The PML₂ language provides a uniform environment for programming, and for proving properties of programs in an ML-like setting. The language is Curry-style and call-by-value, it provides a control operator (interpreted in terms of classical logic), it supports general recursion and a very general form of (implicit, non-coercive) subtyping. In the system, equational properties of programs are expressed using two new type formers, and they are proved by constructing terminating programs. Although proofs rely heavily on equational reasoning, equalities are exclusively managed by the type-checker. This means that the user only has to choose which equality to use, and not where to use it, as is usually done in mathematical proofs. In the system, writing proofs mostly amounts to applying lemmas (possibly recursive function calls), and to perform case analyses (pattern matchings).
Related documents and prototypes:
- https://doi.org/10.4230/LIPIcs.TYPES.2017.4 (introductory paper),
- https://tel.archives-ouvertes.fr/tel-01682908 (R. Lepigre's PhD thesis),
- https://doi.org/10.1007/978-3-662-49498-1_19 (paper related to the model),
- https://doi.org/10.1145/3285955 (paper related to subtyping),
- https://github.com/rlepigre/subml (the SubML language).
PML₂ requiere a Unix-like system. It should work well on Linux as well as on MacOS. It might also be possible to make it work on Windows with Cygwyn or with "bash on Windows").
List of dependencies:
- GNU make,
- OCaml (at least 4.04.0) with Opam,
- dune (at least 1.7.0),
- bindlib 5.0.1 (https://github.com/rlepigre/ocaml-bindlib),
- earley 2.0.0 (https://github.com/rlepigre/ocaml-earley).
Using Opam, a suitable OCaml environment can be setup as follows.
opam switch 4.05.0
eval `opam config env`
opam install dune>=1.7.0 bindlib.5.0.1 earley.2.0.0
To compile PML₂, just run the command make
in the source directory. This
produces the main.native
binary, which can be run on files with the .pml
extension (use ./main.native --help
for more informations).
make
make install # optionally install the program.
make doc # optionally produce the ocamldoc documentation
This folder contains files related to the PML project.
The source files can be found in the following folders:
src/util
contains a set of libraries not directly related to PML,src/parser
contains a low level AST of the language and the parser,src/kernel
contains the core of PML (type checking, equivalence, AST...),src/pml.ml
is the main program.
Other directories:
editors
contains PML modes for editors (vim and emacs only),lib
contains the PML standard library (very small),test
contains most of our examples of PML programs,
The directories tmp
and attic
are not relevant as the contain files used
for debugging the newest features including termination checking and old code
that we want to keep somewhere.
After installing PML (with make install
), you will need to add the
following lines to you .vimrc
file (if they are not already present).
" PML stuff
let g:opamshare = substitute(system('opam config var share'),'\n$','','''')
execute "set rtp+=" . g:opamshare . "/pml/vim"
Note that it may be necessary for these lines to appear before the following line.
filetype plugin indent on
After installing PML (with make install
), you will need to add the
following lines to you .emacs
file.
;; PML stuff
(load "pml-mode")
My advice to start looking at the code would be to take a look at the three different abstract syntax representations.
- The main abstract syntax is implemented as a GADT in
src/kernel/ast.ml
, - The abstract syntax after parsing can be found in
src/parser/raw.ml
, together with the first level of type checking (sorting), - The graph representation of terms for the decision of equivalence can be
found in
src/kernel/equiv.ml
.
The implementation of type checking can be found in src/kernel/typing.ml
,
and the function for comparing expressions (including the unification
functions) are in src/kernel/compare.ml
.