Skip to content


Switch branches/tags

Latest commit

* Improved record syntax and pretty printer

* remove #quit from test

* minor improvement

* remove use of %s

* cleanup pp_fields in terms of pp_print_list

* refactor pp_sign

* tweak precedence of =>

* improve v type printing

* 🌻 Improve pretty printing

* πŸ“Έ Update snapshots

* 🌻 Don't omit dimensions or cofibrations for anon vars in printing

* πŸ“Έ Update snapshots

* 🚫 Revert change to anonymous variables + lambdas

* πŸ“Έ Update snapshots

* πŸ› Worship the immortal pretty printing rules

* πŸ“Έ Update snapshot

* Update src/core/

Co-authored-by: favonia <>

* fix bug in pretty printer for Pi

Co-authored-by: Reed Mullanix <>
Co-authored-by: favonia <>

Git stats


Failed to load latest commit information.


A cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory.

For examples, see the test/ directory.

This implementation is forked from blott, the implementation artifact of Implementing a Modal Dependent Type Theory by Gratzer, Sterling, and Birkedal. Code has been incorporated from redtt, implemented by Sterling and Favonia.


cooltt has been built with OCaml 4.13.0 with opam 2.0.8. If you are running an older version of OCaml, try executing the following command:

$ opam switch create 4.13.0

Once these dependencies are installed cooltt can be built with the following set of commands.

$ opam update
$ opam pin add -y cooltt .              # first time
$ opam upgrade                          # after packages change

After this, the executable cooltt should be available. The makefile can be used to rebuild the package for small tests. Locally, cooltt is built with dune; running the above commands will also install dune. Once dune is available the executable can be locally changed and run with the following:

$ make upgrade-pins                     # update and upgrade dependencies in active development
$ dune exec cooltt                      # from the `cooltt` top-level directory

A small collection of example programs is contained in the test/ directory. See test/ for a brief description of each program's purpose.


This research was supported by the Air Force Office of Scientific Research under MURI grants FA9550-15-1-0053, FA9550-19-1-0216, and FA9550-21-0009. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of any sponsoring institution, government or any other entity.