wiki:WikiStart
Last modified 4 years ago Last modified on 04/26/13 15:12:39

Overview

PML is a variant of the ML language (like Standard ML or OCaml) which focuses both on being able to prove programs and be really usable. The current version starts to fulfill both goals even if several major features are still under development (like a compiler or input-output). PML should also be usable to develop certified mathematics.

Current status: the core language has now stabilized and one can start writing proofs. Many examples are available in the examples and lib folders.

PML is not yet usable as a production programming language. It is still a research platform. Nevertheless, we will be grateful if you try it and report about your experience and problems.

Installation

To install PML, you need

  • darcs,
  • OCaml (>= 3.11),
  • findlib (can also do without ... with a little makefile editing),
  • dypgen (a very nice parser generator for OCaml) and
  • bindlib (the darcs version only).
  • Boehm's GC (it is possible to compile PML without its compiler and drop this dependency, see below) For best performance, use libgc 7.1 or more recent with the following compilation option:

CFLAGS="-O2" ./configure --enable-threads=posix --enable-thread-local-alloc --disable-gc-debug

Then, get the latest development version of PML, using darcs:

darcs get http://lama.univ-savoie.fr/~raffalli/repos/pml

A tar archive is also available (version 26/04/2013)

The above repository is a copy of PML which is manually updated from the working repository when this seems a good idea ;-). If you want to participate to PML's development, you may have a read write access to the working repository. Send an email to raffalli at univ-savoie.fr.

Then, follow the instructions in INSTALLDOC file at the root of the pml repository you just downloaded.

Using PML

  • Programming in PML (in progress): explains how to program in PML. These pages should converge toward a programming course based on PML, adapted even for beginners.
  • Proving in PML (planned): explains how to write properties and proof in PML. These pages should converge toward a course on certified programming (and may be later, certified mathematics).

More details (page are signaled as "in progress" = readable or "planned" = not ready for reading)