McLTT: A Bottom-up Approach to Implementing A Proof Assistant

In McLTT, we build a verified, runnable typechecker for Martin-Löf type theory. After the accomplishment of this project, we will obtain an executable, to which we can feed a program in Martin-Löf type theory, and this executable will check whether this program has the specified type. McLTT is novel in that it is implemented in Coq. Moreover, we will prove that the typechecking algorithm extracted from Coq is sound and complete: a program passes typechecking if and only if it is a well-typed program in MLTT. This will be the first verified proof assistant (despite being elementary) and serves as a basis for future extensions.

Online Documentation

We have generated a Coqdoc for browsing our Coq proof.

Architecture

McLTT has the following architecture:

    | source code of McLTT
    v
+-------+
| lexer |          OCaml code generated by ocamllex
+-------+
    | stream of tokens
    v
+--------+
| parser |         Coq code generated by Menhir
+--------+
    | concrete syntax tree
    v
+------------+
| elaborator |     Coq code
+------------+
    | abstract syntax tree
    v
+-------------+
| typechecker |    Coq code
| (normalizer |
|   included) |
+-------------+
    | yes or no    Driver in OCaml
    v

In this architecture, most code is in Coq, with accompanying theorems to justify the implementation.

Dependencies

• OCaml 4.14.2
• Menhir
• Coq-Menhirlib
• Coq 8.20.0
• Coq-Equations 1.3

We recommend to install dependencies in the following way:

opam switch create coq-8.20.0 4.14.2
opam install menhir
opam pin add coq 8.20.0
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-equations
opam install coq-menhirlib
opam install ppx_inline_test

Development

Use the toplevel make to build the whole project:

make

Makefile will try to find out the number of your CPU cores and parallel as much as possible.

Once make finishes, you can run the binary:

dune exec mcltt examples/nary.mcl # or your own example

or more directly

_build/default/driver/mcltt.exe examples/nary.mcl # or your own example

To build Coq proof only, you can go into and only build the Coq folder:

cd theories
make

Branches

The Github repo includes the following special branches:

1. main: the main branch that is used to generate this homepage and Coqdoc;
2. ext/*: branches in this pattern are variations of main that implements various extensions. They are often used to implement extensions that require non-trivial workload and are aimed to be merged to main eventually;
3. gh-pages: the branch to host the homepage.