- Transition to Processing
- Primitive Operations
- Algorithms
- Variables
- Debugging in Processing
- Conditions
- Loops
- Functions
- Scope
- Compound Data
- Reference Semantics
- Refactoring
- Transition to Java
- Debugging in Java
- Unit Testing
- Classes - Writing your own Types
- Classes - Functions inside objects
- Recursion
- Lists
- Iteration
- Recursive Lists
- Searching

- Logic and Proofs
- Relations
- Mathematical Functions
- Matrices
- Binary Numbers
- Trigonomtry
- Finite State Machines
- Turing Machines
- Counting - Inclusion/Exclusion
- Graph Algorithms

- Algorithm Efficiency
- Algorithm Correctness
- Trees
- Heaps, Stack, and Queues
- Maps and Hashtables
- Graphs and Graph Algorithms
- Advanced Trees and Computability

- Command line control
- Transition to C
- Pointers
- Memory Allocation
- IO
- Number representations
- Assembly Programming
- Structs and Unions
- How memory works
- Virtual Memory

- Version Control with Git
- Inheritance and Overloading
- Generics
- Exceptions
- Lambda Expressions
- Design Patterns
- Concepts of Concurrency
- Concurrency: Object Locks
- Modern Concurrency

- System Models
- Naming and Distributed File Systems
- Synchronisation and Concurrency
- Fault Tolerance and Security
- Clusters and Grids
- Virtualisation
- Data Centers
- Mobile Computing

- Transition to Scala
- Functional Programming
- Syntax Analysis
- Name Analysis
- Type Analysis
- Transformation and Compilation
- Control Abstraction
- Implementing Data Abstraction
- Language Runtimes

- Transition to Coq
- Proof by Induction, Structured Data
- Polymorphism and Higher-Order Functions
- More Basic Tactics
- Logical Reasoning in Proof Assistants
- Inductive Propositions
- Maps
- An Imperative Programming Language
- Program Equivalence
- Hoare Logic
- Small-Step Operational Semantics
- Simply-typed Lambda Calculus

- Have a broader range of Coq tactics in your proof-toolbox.

All the material for this topic is contained in the Tactics chapter of Software Foundations.