Blog|Meta Topics|Advanced Topics

Software Technology: Proof by Induction, Structured Data

Programming
  1. Transition to Processing
  2. Primitive Operations
  3. Algorithms
  4. Variables
  5. Debugging in Processing
  6. Conditions
  7. Loops
  8. Functions
  9. Scope
  10. Compound Data
  11. Reference Semantics
  12. Refactoring
  13. Transition to Java
  14. Debugging in Java
  15. Unit Testing
  16. Classes - Writing your own Types
  17. Classes - Functions inside objects
  18. Recursion
  19. Lists
  20. Iteration
  21. Recursive Lists
  22. Searching
Mathematics for Programmers
  1. Logic and Proofs
  2. Relations
  3. Mathematical Functions
  4. Matrices
  5. Binary Numbers
  6. Trigonomtry
  7. Finite State Machines
  8. Turing Machines
  9. Counting - Inclusion/Exclusion
  10. Graph Algorithms
Data Structures and Algorithms
  1. Algorithm Efficiency
  2. Algorithm Correctness
  3. Trees
  4. Heaps, Stack, and Queues
  5. Maps and Hashtables
  6. Graphs and Graph Algorithms
  7. Advanced Trees and Computability
Systems Programming
  1. Command line control
  2. Transition to C
  3. Pointers
  4. Memory Allocation
  5. IO
  6. Number representations
  7. Assembly Programming
  8. Structs and Unions
  9. How memory works
  10. Virtual Memory
The Practice of Programming
  1. Version Control with Git
  2. Inheritance and Overloading
  3. Generics
  4. Exceptions
  5. Lambda Expressions
  6. Design Patterns
  7. Concepts of Concurrency
  8. Concurrency: Object Locks
  9. Modern Concurrency
Distributed Systems
  1. System Models
  2. Naming and Distributed File Systems
  3. Synchronisation and Concurrency
  4. Fault Tolerance and Security
  5. Clusters and Grids
  6. Virtualisation
  7. Data Centers
  8. Mobile Computing
Programming Languages
  1. Transition to Scala
  2. Functional Programming
  3. Syntax Analysis
  4. Name Analysis
  5. Type Analysis
  6. Transformation and Compilation
  7. Control Abstraction
  8. Implementing Data Abstraction
  9. Language Runtimes
Provably Correct Programs
  1. Transition to Coq
  2. Proof by Induction, Structured Data
  3. Polymorphism and Higher-Order Functions
  4. More Basic Tactics
  5. Logical Reasoning in Proof Assistants
  6. Inductive Propositions
  7. Maps
  8. An Imperative Programming Language
  9. Program Equivalence
  10. Hoare Logic
  11. Small-Step Operational Semantics
  12. Simply-typed Lambda Calculus
Assumed Knowledge:
Learning Outcomes:
  • Write your first proofs by induction, rewriting, and case analysis in Coq.

All the material for this topic is contained in the Induction and Lists chapters of Software Foundations.