The RedPRL Proof Assistant (Invited Paper)

TL;DR

RedPRL is an experimental proof assistant based on Cartesian cubical type theory, enabling higher-dimensional constructions and combining extensional and proof-relevant equality notions for advanced formal reasoning.

Contribution

It introduces a novel proof assistant implementing a two-level type theory with both extensional and higher-dimensional path equality, inspired by homotopy type theory.

Findings

Supports higher-dimensional constructions in proof development

Combines extensional and proof-relevant equality notions

Demonstrates practical use of cubical type theory in proof assistant

Abstract

RedPRL is an experimental proof assistant based on Cartesian cubical computational type theory, a new type theory for higher-dimensional constructions inspired by homotopy type theory. In the style of Nuprl, RedPRL users employ tactics to establish behavioral properties of cubical functional programs embodying the constructive content of proofs. Notably, RedPRL implements a two-level type theory, allowing an extensional, proof-irrelevant notion of exact equality to coexist with a higher-dimensional proof-relevant notion of paths.