In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it remains very different from standard programming. To bridge this gap, we aim at designing an ML-style programming language with support for proofs of programs, combining in a single tool the flexibility of ML and the fine specification features of a proof assistant. In other words, the system should be suitable both for programming (in the strongly-typed, functional sense) and for gradually increasing the level of guarantees met by programs, on a by-need basis.
We thus define and study a call-by-value language whose type system extends higher-order logic with an equality type over untyped programs, a dependent function type, classical logic and subtyping. The combination of call-by-value evaluation, dependent functions and classical logic is known to raise consistency issues. To ensure the correctness of the system (logical consistency and runtime safety), we design a theoretical framework based on Krivine's classical realisability. The construction of the model relies on an essential property linking the different levels of interpretation of types in a novel way.
We finally demonstrate the expressive power of our system using our prototype implementation, by proving properties of standard programs like the map function on lists or the insertion sort.
The source code of the implementation is available online as a Darcs repository. It can be accessed through the HTTPS protocol using the following command.
darcs get https://lama.univ-smb.fr/~lepigre/these/pml2
It can be compiled using OCaml (it has been tested with version 4.03.0) with ocamlfind, ocamlbuild and standard tools such as GNU make. There are also several dependencies on libraries developed by Christophe Raffalli and me:
Their latest verion can be obtained and installed with the following commands.
darcs get https://www.lama.univ-savoie.fr/~raffalli/repos/bindlib cd bindlib && make && make install && cd .. darcs get https://www.lama.univ-savoie.fr/~raffalli/repos/earley cd earley && make && make install && cd .. darcs get https://www.lama.univ-savoie.fr/~raffalli/repos/earley_ocaml cd earley_ocaml && make && make && make install && cd ..
Note that make needs to be run twice (for bootstrap) for the compilation of earley-ocaml.