MAP/i  Foundations of Computing
Option I: Program Semantics, Verification, and Construction
Login

Register

Print
MAP/i
Overview
Recommended Books
Syllabus and Course Material
Assessment
Education
»
MapiFc
»
WebHome
»
Syllabus0708
Chapter I: Overview of Foundations (5*3 hours)
Intuitionistic logic
Natural deduction
lambdacalculus (terms, reduction, the ChurchRosser Theorem)
Simple Types (Church versus Curry typing, normalization, extensions)
The CurryHoward isomorphism
Introduction to operational semantics
Domain theory (complete partial orders, continuous functions)
Denotational semantics
Chapter II: Program Verification (6*3 hours)
Dependent Types:
Firstorder dependent types
Type equivalence
Sum types
The calculus of inductive constructions
Programming with dependent types
Typebased proof assistants
Interactive proof development
Tactics and tacticals
Inductive data types and predicates
Program correctness: specification; partial and total correctness
Verification of the correctness of functional programs:
Extraction of the computational contents of a correctness proof
Using programs for structuring correction proofs
Axiomatic semantics of imperative programs:
Assertions; semantics of assertions
Hoare proof rules for correctness
Tool support for the specification, verification, and certification of programs:
Proof assistants
Verification condition generators
Alternative approaches to program verification
Certifying compilation and proofcarrying code
Chapter III: Program Construction (4*3 hours)
Introduction to the mathematics of program construction
The specification / implementation dichotomy. Abstract modeling.
Correct by verification versus correct by construction.
Description versus calculation
The Pointfree (PF) transform
Taxonomy of binary relations; simple relations and their role in abstract modeling
Pointfree
notation and reasoning
Rules of the PFtransform
Categorical and allegorical foundations
Universal properties and Galois connections
Universal constructions and properties; natural properties
Reynolds? relation and the freetheorem of polymorphism
Galois connections and their corollaries
Reasoning by PFcalculation
PFcalculation of the consistency of a formal model: satisfiability and invariance
Datalevel calculation: representing and abstracting data models.
Inductive program calculation
Relational hylomorphisms
Fixpoint calculus and Galois connections: the fixpoint fusion theorem
Calculating recursive solutions for hyloequations
Open issues and hot topics in the mathematics of program construction
r3  27 Sep 2008  11:45:31 
JoseBacelarAlmeida
Copyright © by the contributing authors. Ideas, requests, problems?
Send feedback
.
Syndicate this site
RSS
ATOM