Wed 26 Feb
J. Courant (ENS Lyon)
A module system for proofs and programs
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).