MAP/i - Foundations of Computing

Option I: Program Semantics, Verification, and Construction

Chapter I: Overview of Foundations (5*3 hours)

  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 (6*3 hours)

  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 (4*3 hours)

  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

r3 - 27 Sep 2008 - 11:45:31 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM