Proof assistants like Coq, HOL, Agda, ... cannot be used practically as programming languages. A lot of research today consists to start with a given programming language, usually of the ML family, and to add dependent types, thus turning it into a proof assistant. The logic behind such an enriched programming language is a type theory whose terms (the objects we are proving properties of) live in various (distinct) types, stratifying the objects by the type system.
PML arises from a classical realizability model whose basis is the set of all pure (i.e. untyped) programs. Thanks to realizability techniques, the semantics of types and formulas can be reconstructed as particular sets of programs. In this approach, types are just external information you may give (or not) to objects and the same term may have many distinct types (subtyping). In some sense, PML's logic is closer to set theory than type theory.
The key features which arise from this model are:
- Singleton types (not exactly in the sens of Haskell's singleton types)
- Equational reasoning on programs
- Classical logic (if one wishes)
- Subtyping (without coercions)
- Extensible records and polymorphic variants
- Inductive and Co-inductive types.
Moreover, PML does not follow the "proofs as programs" paradigm of system such as Coq, but a "programs as proofs" paradigm (similar to Agda). In particular, the language provides no primitive construct dedicated to proofs, which makes it easier to learn.
In this talk, we will essentially present the language from examples. And then, we shall briefly discuss some ideas of the underlying model.
Prof. Christophe Raffalli
Université Savoie Mont Blanc