The RedPRL Proof Assistant

RedPRL is an experimental proof assistant based on cubical computational type theory, which extends the Nuprl semantics by higher-dimensional features inspired by homotopy type theory. RedPRL is created and maintained by the RedPRL Development Team.

RedPRL is written in Standard ML, and is available for download on GitHub.

Features

• computational canonicity and extraction
• univalence as a theorem
• strict (exact) equality types
• coequalizer and pushout types
• functional extensionality
• equality reflection
• proof tactics

Papers & Talks

• Angiuli, Favonia, Harper. Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. CSL 2018.
• Angiuli, Cavallo, Favonia, Harper, Sterling. The RedPRL Proof Assistant. LFMTP 2018 (Invited Paper).
• Favonia. Cubical Computational Type Theory & RedPRL. 2018.
• Harper, Angiuli. Computational (Higher) Type Theory. ACM POPL Tutorial Session 2018.
• Sterling, Harper. Algebraic Foundations of Proof Refinement. Draft, 2016.

RedPRL User Guide

• Tutorial
  • Getting started
  • Cubical reasoning
• Language reference
  • Top-level vernacular
  • Object language
  • Tactic language
• Atomic judgments
  • Truth
  • Type equality
  • Subtyping
  • Subkinding
  • Term
• Multiverses
• Refinement rules
  • Booleans
  • Natural numbers and integers
  • Void
  • Circle
  • Dependent functions
  • Records
  • Paths
  • Lines
  • Pushouts
  • Coequalizers
  • Exact equalities
  • Composite types
  • V types
  • Kan operations
  • Universes

Indices

• Index
• Search Page

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 Isaac Newton Institute for Mathematical Sciences for its support and hospitality during the program “Big Proof” when part of this work was undertaken; the program was supported by the Engineering and Physical Sciences Research Council under grant number EP/K032208/1. 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.