contribution: C (integration of functional languages and proof assistants)

I shall talk about a module system for proof assistants such as
Coq. The proposed module system can be quickly described as
an SML-like module system in which the notion of type abstraction
had to be (and has been) revisited in order to gain some
meta-theoretical properties. I shall try to explain why such
properties were desirable in the framework of proof assistants,
and also, how my proposal could bring these properties to module
systems for programming languages -- as such, my talk have strong
connections with theme B (program structuring).

---------------------------------------------------------------------------
Result of feedback form submitted by
Courant (Judicael.Courant@ens-lyon.fr) on Tuesday, August 11, 1998 at 09:21:07