The RedPRL Proof Assistant (Invited Paper)
Logic in Computer Science
2018-07-06 v1 Programming Languages
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.
Cite
@article{arxiv.1807.01869,
title = {The RedPRL Proof Assistant (Invited Paper)},
author = {Carlo Angiuli and Evan Cavallo and Kuen-Bang Hou and Robert Harper and Jonathan Sterling},
journal= {arXiv preprint arXiv:1807.01869},
year = {2018}
}
Comments
In Proceedings LFMTP 2018, arXiv:1807.01352