MAP/i - Foundations of Computing

Chapter I: Overview of Foundations

1. Intuitionistic logic
2. Natural deduction
3. lambda-calculus (terms, reduction, the Church-Rosser Theorem)
4. Simple Types (Church versus Curry typing, normalization, extensions)
5. The Curry-Howard isomorphism
6. Introduction to operational semantics
7. Domain theory (complete partial orders, continuous functions)
8. Denotational semantics

Chapter II: Program Verification

1. Dependent Types:
   • First-order dependent types
   • Type equivalence
   • Sum types
   • The calculus of inductive constructions
   • Programming with dependent types
2. Type-based proof assistants
   • Interactive proof development
   • Tactics and tacticals
   • Inductive data types and predicates
3. Program correctness: specification; partial and total correctness
4. Verification of the correctness of functional programs:
   • Extraction of the computational contents of a correctness proof
   • Using programs for structuring correction proofs
5. Axiomatic semantics of imperative programs:
   • Assertions; semantics of assertions
   • Hoare proof rules for correctness
6. Tool support for the specification, verification, and certification of programs:
   • Proof assistants
   • Verification condition generators
7. Alternative approaches to program verification
   • Certifying compilation and proof-carrying code

Chapter III: Program Construction

1. Introduction to the mathematics of program construction
   • The specification / implementation dichotomy. Abstract modeling.
   • Correct by verification versus correct by construction.
2. Description versus calculation
3. The Point-free (PF) transform
   • Taxonomy of binary relations; simple relations and their role in abstract modeling
   • Point-free notation and reasoning
   • Rules of the PF-transform
   • Categorical and allegorical foundations
4. Universal properties and Galois connections
   • Universal constructions and properties; natural properties
   • Reynolds? relation and the free-theorem of polymorphism
   • Galois connections and their corollaries
5. Reasoning by PF-calculation
   • PF-calculation of the consistency of a formal model: satisfiability and invariance
   • Data-level calculation: representing and abstracting data models.
6. Inductive program calculation
   • Relational hylomorphisms
   • Fixpoint calculus and Galois connections: the fixpoint fusion theorem
   • Calculating recursive solutions for hylo-equations
7. Open issues and hot topics in the mathematics of program construction