McTT: Building A Correct-By-Construction Proof Checkers For Type Theories

McTT is a verified, runnable typechecker for Martin-Löf type theory. This project provides an executable, to which we can feed a program in Martin-Löf type theory to check whether this program has the specified type. McTT is novel in that it is implemented and verified in Coq. More specifically, we proved that the typechecking algorithm extracted from Coq is sound and complete: a program passes typechecker if and only if it is a well-typed program in MLTT. This is 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

McTT has the following architecture:

    | source code of McTT
    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 update
opam switch create coq-8.20.0 4.14.2
opam pin add coq 8.20.0
opam repo add coq-released https://coq.inria.fr/opam/released
opam install -y menhir coq-equations coq-menhirlib 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 mctt examples/nary.mctt # or your own example

or more directly

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

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

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.