The RedPRL proof assistant (invited paper)

DOI10.4204/EPTCS.274.1MaRDI QIDQ6940464zbMATH OpenFDO

Authors Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.274.1

Mathematics Subject Classification ID

Type theory (03B38) Functional programming and lambda calculus (68N18) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• Advanced Functional Programming
• Computational higher-dimensional type theory
• Constructive mathematics and computer programming
• Cubical type theory: a constructive interpretation of the univalence axiom
• Edinburgh LCF. A mechanized logic of computation
• Homotopy type theory in Lean
• Homotopy type theory. Univalent foundations of mathematics
• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• Idris, a general-purpose dependently typed programming language: Design and implementation
• The Matita interactive theorem prover

This page was built for publication: The RedPRL proof assistant (invited paper)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940464)