RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link
cubical-type-theory ocaml proof-assistant type-theory

redtt is a core language for cartesian cubical type theory with extension types. We plan to build an extensible interactive proof assistant around it, using ideas from proof assistants like RedPRL, Epigram, and Idris.

Related work: yacctt, RedPRL and cubicaltt.

Feature Summary

redtt is not yet documented; we have the following interesting features:

Features we intend to add in the near future:

The redtt mathematical library

See library/README.md.

Contributing Guidelines

Help is welcome and desired! Please see the open tickets and especially our Roadmap. Currently, we are trying to limit the dependencies of this code; when something is available as a package, but can easily be coded locally, we prefer the latter.

We also want to avoid using things like syntax extensions/ppxs, though we may end up using one of these for the lexer at one point.

Installing

Prerequisites

prerequisite version how to install
OPAM >= 2.0.5 manually or via package manager

If this is your first time configuring OPAM, please run opam init; this will automatically install OCaml. If you are using a version of OCaml other than 4.09.0, you must run opam switch 4.09.0.

Other recommended packages

We recommend installing merlin and ocp-indent using opam; the easiest way to edit OCaml code out of the box is to install Visual Studio Code along with the OCaml and Reason IDE package by Darin Morrison.

Installing Dependencies

$ git clone https://github.com/RedPRL/redtt
$ cd redtt
$ opam update
$ opam pin add -y redtt . # the first time you build
$ opam upgrade            # after packages change

If you have previously built redtt but some of our dependencies have changed in the meanwhile, opam upgrade might fail. In this case, please first run opam uninstall redtt and then run opam upgrade.

Building

$ make

Toplevel

Requires utop (see prerequisites).

$ make top

Library

$ make library

What's the relationship to RedPRL?

The goal of the RedPRL Development Team is to study implementation techniques for higher dimensional type theory, and determine which ideas lead to the most convenient and ergonomic system for developing both higher dimensional mathematics and higher dimensional programming. To this end, our first experiment was the RedPRL Proof Assistant; our second experiment is the redtt proof assistant, which synthesizes what we learned from the experience of building RedPRL and using it to formalize mathematics.

Acknowledgments

This research was sponsored by the Air Force Office of Scientific Research under grant number FA9550-15-1-0053 and the National Science Foundation under grant number DMS-1638352. We also thank the Logic and Semantics Group at Aarhus University for their hospitality in during the summer of 2018, during which part of this work was undertaken. The views and conclusions contained here are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any sponsoring institution, government or any other entity.