Meta Topics
Software Technology
: Polymorphism and Higher Order Data
Programming
Transition to Processing
Primitive Operations
Algorithms
Variables
Debugging in Processing
Conditions
Loops
Functions
Scope
Compound Data
Reference Semantics
Refactoring
Program Design
Transition to Java
Debugging in Java
Unit Testing
Classes - Writing your own Types
Classes - Copying objects
Classes - Functions inside objects
Classes - Composition
Classes - Array of objects
Classes - Class holding array(s)
Recursion - What goes on during a function call
Recursion
Recursion with String data
Tail-optimized recursion
Recursion with arrays
Lists
Iteration
Custom-built ArrayList
Recursive data structures - 1
Recursive data structures - 2
Searching
Mathematics for Programmers
Logic and Proofs
Relations
Mathematical Functions
Matrices
Binary Numbers
Trigonomtry
Finite State Machines
Turing Machines
Counting - Inclusion/Exclusion
Graph Algorithms
Data Structures and Algorithms
Algorithm Efficiency
Algorithm Correctness
Trees
Heaps, Stack, and Queues
Maps and Hashtables
Graphs and Graph Algorithms
Advanced Trees and Computability
Systems Programming
Command line control
Transition to C
Pointers
Memory Allocation
IO
Number representations
Assembly Programming
Structs and Unions
How memory works
Virtual Memory
The Practice of Programming
Version Control with Git
Inheritance and Overloading
Generics
Exceptions
Lambda Expressions
Design Patterns
Concepts of Concurrency
Concurrency: Object Locks
Modern Concurrency
Distributed Systems
System Models
Naming and Distributed File Systems
Synchronisation and Concurrency
Fault Tolerance and Security
Clusters and Grids
Virtualisation
Data Centers
Mobile Computing
Programming Languages
Transition to Scala
Functional Programming
Syntax Analysis
Name Analysis
Type Analysis
Transformation and Compilation
Control Abstraction
Implementing Data Abstraction
Language Runtimes
Provably Correct Programs
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
Assumed Knowledge:
Can do basic proofs by induction and work with inductive data types as well as polymorphism.
Learning Outcomes:
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.