Date: Wed 26 Feb
Time: 15.00
Place: room 214

Speaker: J. Courant (ENS Lyon)
Title: A module system for proofs and programs
Reference: Elena Zucca

Abstract. The development of large programs or of large formal proofs in a proof checker raise modularity issues. During past years, more and more satisfaying solutions were given in order to modularize programs. One of the most powerful module system is the one of SML. I will show how a similar module system can be adapted to a class of programming and logical languages (called Pure Type Systems). In this aim, I will first try to explain connections between programmation and logic, known as the Curry-Howard isomorphism and I will explain the main concepts underlying the SML module system. Then I will present a module system whose addition to logical languages is logically consistent, and has several desirable properties (subject-reduction, normalization, type inference decidability).