Programming and Specification Logics
Code
11168
Academic unit
Faculdade de Ciências e Tecnologia
Department
Departamento de Informática
Credits
6.0
Teacher in charge
Carla Maria Gonçalves Ferreira, Luís Manuel Marques da Costa Caires
Weekly hours
4
Total hours
56
Teaching language
Português
Objectives
Knowledge
This course teaches advanced concepts and techniques, based on constructive logic, which underpin the production of certified software and support reasoning about programs and programming languages. The close connection between programs and proofs, called the Curry-Howard correspondence, will be revealed and explored in the course. Students learn the modern type-theoretical foundations of functional and imperative programming, including programming with dependent types, and to develop program proofs.
Application
Students also how to develop certified programs and data types using Coq, an industrial strenght proof assistant, developed at INRIA, being used worldwide in industry and academia. Students use a modern interactive theorem proof assistant. Examples of covered software include ADT based functional and imperative programs, programming language interpreters, and processors, including type checkers and compilers.
Prerequisites
Basic logic and set theory.
Functional and imperative programming.
Algorithms and data structures.
Subject matter
1. Constructive Logic Propositions as Types / Programs as Proofs; The Curry-Howard Interpretation; Logic in Coq. 2. Reasoning about Functional Programs with Dependent Types Basic Functional Programming: numbers, lists, basic proofs; Dependent types; Inductive types; Inductive propositions; Polymorphism and Higher-order functions. Program extraction. Tactics in Coq. 3. Reasoning about Program Interpreters Representing Expressions and Commands; Specification of Evaluation: Hoare Triples, weakest preconditions, verification conditions; Reasoning about imperative programs that manipulate data-structures. 4. Reasoning about Programming Languages A Simple Functional Language; Specification of Evaluation; Type Systems; Type Preservation and Type Safety; A Simple Machine Language; Specification of Execution; Compiler correctness. Program Equivalence; Bisimulation. NB: All chapters will also cover relevant Coq notions, such as proof manipulation, tactics, and proof automation.
Bibliography
Software Foundations, Benjamin C. Pierce, Chris Casinghino, Michael Greenberg, Vilhelm Sjöberg, BrenYorgey, 2012.
The Coq Proof Assistant (http://coq.inria.fr/).
Teaching method
The course is organized in recitation lectures (2T) and laboratory classes (2P). In the laboratory classes students discuss and solve problems proposed by the instructor from a predefined list, and using intensively the Coq proof assistant. In the recitation lectures the instructor presents and motivates concepts and applications are discussed and exemplified. Typically, some “knowledge application” learning outcomes are also exercised in the recitation, so to promote a close connection between the theoretical concepts and their application. Evaluation consists in midterm and final tests and one software development project, to be done by the students as a team. Any student that fails in the basic evaluation scheme with a grade equal of higher than 8/20 is admitted to the final exam, which combines with the grading of the project to produce the final grade.