Software foundations

This course introduces basic concepts and techniques in the foundational study of programming languages, as well as their formal logical underpinnings. The central theme is the view of individual programs and whole languages as mathematical objects about which precise claims may be made and proved. Particular topics include operational techniques for formal definition of language features, polymorphism, type systems and type safety properties.

• Functional programming in Coq
• Constructive logic
• Inductive types and proof techniques for informal and formal proof
• Proof tactics, the Coq proof assistant
• Operational semantics
• Type systems, type safety
• Application to imperative languages
• Correctness of program transformations
• Application to simply types lambda-calculus

Semantics of programming languages, program proof, reasoning techniques.

Basics of functional programming, basics of logic.

• Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, by Yves Bertot and Pierre Castéran, 2004
• The Coq proof assistant, by Institut national de recherche en sciences et technologies du numérique (Inria)
• Types and Programming Languages, by Benjamin C. Pierce, 2002

Sandrine Blazy is professor at the University of Rennes 1 and deputy director of IRISA. Her research interests include semantics of programming languages, theorem proving, static analysis, verified compilation with several applications to software security.