Repository files navigation

redtt is a core language for cartesian cubical type theory with extensiontypes. We plan to build an extensible interactive proof assistant around it,using ideas from proof assistants likeRedPRL,Epigram, andIdris.

Related work:yacctt,RedPRLandcubicaltt.

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

• path types definable in terms of more general extension types, which specifythe boundary of ann-cube all at once

• source language with implicit arguments based on a cubical version ofhigher-order unification

• predicative hierarchy of cumulative, univalent universes

• level "polymorphic" definitions achieved using McBride's "Crude But EffectiveStratification" (in which each thing is defined at the lowest level possible,and then hoisted upward when needed)

• two-level type theory in the style of RedPRL: currently we have only pretypesand (kan) types. Once we design a suitable account of exact equality types inthe cubical setting, we will add these, and they will live side-by-side withpath types as they did in RedPRL.

• user-defined (parametric) higher inductive types (indexed HITs not yet supported)based on thework of Evan Cavallo and Bob Harper.

• RedML, a (very) rudimentary tactic language

Features we intend to add in the near future:

• namespacing

• indexed higher inductive types

• a type system for RedML

• algebraic effects and handlers for RedML

Seelibrary/README.md.

Help is welcome and desired! Please see theopentickets andespecially ourRoadmap.Currently, we are trying to limit the dependencies of this code; when somethingis available as a package, but can easily be coded locally, we prefer thelatter.

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

If this is your first time configuring OPAM, please runopam init; this willautomatically install OCaml. If you are using a version of OCaml other than4.09.0, you must runopam switch 4.09.0.

We recommend installingmerlin andocp-indent usingopam; the easiest way to editOCaml code out of the box is to installVisual StudioCodealong with theOCaml and ReasonIDEpackage by Darin Morrison.

$ 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 builtredtt but some of our dependencies have changedin the meanwhile,opam upgrade might fail. In this case, please first runopam uninstall redtt and then runopam upgrade.

$ make

Requiresutop (see prerequisites).

$ make top

$ make library

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 theredtt proof assistant, which synthesizes what we learned from the experience of building RedPRL and using it to formalize mathematics.

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.