Foundations for Rigorous Software Development
Professor: Álvaro Freitas Moreira
Hours: 60 hs
Undergraduate Enrollment: INF05013
Page Link: –
Lambda Calculus, Simply Typed Lambda Calculus, Polymorphic Types, Dependent Types, Calculus of Constructions, Constructive Interpretation of Propositional and Predicate Logic.
Programming languages defined on top of formally defined cores together with proof assistants are fundamental tools for rigorous software development. The goals of this course are: (i) to present to the students variations of the lambda calculus, both in the untyped version and in typed versions with simple types and their extensions such as polymorphic and dependent types, (ii) understand the foundations of modern proof assistants like Coq and Agda, as well as (iii) the foundations of modern programming languages such as Haskell, Ocaml, and F#.
– Lambda Calculus – semantics and properties
– Simply Typed Lambda Calculus – semantic and properties
– Constructive Interpretation of Propositional Logic
– Lambda Calculus with Polymorphic Types – semantics and properties
– Lambda Calculus with Dependent Types – semantics and properties
– Calculus of Constructions – semantics, and properties
– Constructive Interpretation of Predicate Logic
The evaluation will consist of a number of lists of exercises to be solved individually by the students. The final score M will be given by the arithmetic mean of the scores on the exercises. The final grade can be improved by also taking into account subjective criteria such as class participation and attendance.
The possible grades are A (score >= 9.0), B (score >= 7.5 and < 9.0), C (score >= 6.0 and < 7.5), D (failed, score< 6.0) or FF (failed, the student attended less than 75% of the classes).