Skip to content


Subversion checkout URL

You can clone with
Download ZIP
A minimalist implementation of type theory, suitable for experimentation
OCaml TeX Emacs Lisp Shell Makefile Standard ML JavaScript
Fetching latest commit...
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.


A minimalist implementation of type theory with universes indexed by numerals and dependent products. The concrete syntax is as follows:

  • The universes are Type 0, Type 1, Type 2, ...
  • A dependent product is written as forall x : T1, T2
  • A function is written as fun x : T => e
  • Application is written as e1 e2


Type Help. in the interactive shell to see what the type system can do. Here is a sample session:

Type Ctrl-D to exit or "Help." for help.]
# Parameter nat : Type 0.
nat is assumed
# Parameter z : nat.
z is assumed
# Parameter s : nat -> nat.
s is assumed
# Eval (fun f : nat -> nat => fun n : nat => f (f (f (f n)))) (fun n : nat => s (s (s n))) (s (s (s (s z)))).
    = s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))))
    : nat
# Check (fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f A).
Typing error: type mismatch
# Check (fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f a).
fun A : Type 0 => fun f : A -> Type 1 => fun a : A => f a
    : forall A : Type 0, (A -> Type 1) -> A -> Type 1

Source code

The purpose of the implementation is to keep the source uncomplicated and short. The essential bits of source code can be found in the following files:

  • the abstract syntax
  • compiled form of abstract syntax, where abstractions are Ocaml functions, normalization
  • type checking

The rest of the files are just logistics:

  • lexer.mll lexical analysis of concrete syntax
  • parser.mly parser which converts concrete syntax to abstract syntax
  • pretty-printing of expressions
  • commonly used functions
  • printing of errors
  • toplevel interactive shell
Something went wrong with that request. Please try again.