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

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 ppx_expect

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

External Syntax

Our interpreter accepts a prog, defined in the following grammar (written in EBNF):

prog = term , ':' , type;

type = term;
     (* function type *)
term = 'forall' , {parameter} , '->' , term
     (* function *)
     | 'fun' , {parameter} , '->' , term
     (* application *)
     | {atomic term}
     (* let expression *)
     | 'let' , {let definition} , 'in' , term
     (* successor of a natural number *)
     | 'succ' , term
     (* natural number eliminator *)
     | 'rec' , term , 'return' , nat motive , zero branch , succ branch , 'end';

            (* universe of level n *)
atomic term = 'Type', '@' , nat
            (* natural number type *)
            | 'Nat'
            (* natural number zero *)
            | 'zero'
            (* a shorthand for succ (succ (... (succ zero))) *)
            | nat
            (* variable *)
            | id
            (* parenthesized term *)
            | '(' , term , ')';

parameter = '(' , id , ':' , type , ')';

let definition = '(' , parameter , ':=' , term , ')';

(* This describes the return type of the eliminator
   when id is bound to the scrutinee *)
nat motive = id , '.' , type;

zero branch = '|', 'zero' , '=>' , term;

(* the first id is predecessor
   and the second id is the result of the recursive call *)
succ branch = '|', 'succ' , id , id , '=>' , term;

id = ? sequence of upper- or lower-case ASCII alphabet characters ?;
nat = ? natural number ?;

Here, we omit spaces between tokens. Note that the current let expression does not support delta reduction.

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.