Lista de Disciplinas | CMP194

Foundations for Rigorous Software Development

Professor: Álvaro Freitas Moreira
Prerequisites: –
Hours: 60 hs
Credits: 4
Semesters: First
Undergraduate Enrollment: INF05013
Page Link: –

SUMMARY

Lambda Calculus, Simply Typed Lambda Calculus, Polymorphic Types, Dependent Types, Calculus of Constructions, Constructive Interpretation of Propositional and Predicate Logic.

OBJECTIVES

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#.

PROGRAM

– 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

EVALUATION

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).

BIBLIOGRAPHY

1. Rob Nederpelt and Herman Geuvers. Type Theory and Formal Proof: An Introduction. Cambridge University Press, 2014. ISBN 9781316056349
2. Benjamin Pierce. Types and programming languages. Cambridge: MIT Press, 2002. ISBN 0262162091
3. Papers on the specific topics discussed will also be recommended