- 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

- Some experience with Functional Programming

- Become familiar with the basic constructs of proofs in Coq

All the material for this topic is contained in chapters Preface and Basics of the Software Foundations text.

Some interesting points to come out of this:

`Inductive`

defines new data`Definition`

defines new computation and`Compute`

is how we invoke that computation.- Functions are defined in pattern matching style.
`Example`

defines new goal/assertion- It seems like all computation over inductive data types is done with
`match`

expressions. That sounds about-right. - It looks like
`simpl`

might compute for us and`reflexivity`

dispatches things that are the same on the left as they are on the right. `Check`

will tell us the type of a value.- Types are given in the Haskell.
- We have enumerated types and so-called “inductive” types.
- Constructors seem a lot like functions - they even have the same type!