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. Program Design
  14. Transition to Java
  15. Debugging in Java
  16. Unit Testing
  17. Classes - Writing your own Types
  18. Classes - Copying objects
  19. Classes - Functions inside objects
  20. Classes - Composition
  21. Classes - Array of objects
  22. Classes - Class holding array(s)
  23. Recursion - What goes on during a function call
  24. Recursion
  25. Recursion with String data
  26. Tail-optimized recursion
  27. Recursion with arrays
  28. Lists
  29. Iteration
  30. Custom-built ArrayList
  31. Recursive data structures - 1
  32. Recursive data structures - 2
  33. 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.