Proof Refinement Logic — Computational Type Theory


Function Extensionality

JonPRL is based off of Nuprl’s Computational Type Theory, where each type is individually assigned its correct judgemental equality.

Intersection & Subset Types

Computationally irrelevant code may be stripped off of realizers by using family intersection types \(\bigcap_{x:A} B[x]\) and set types \(\{x:A\mid B[x]\}\).

Computational Equality

JonPRL comes with Howe's Computational Equality from the start, enabling domain-theory-style reasoning about untyped terms.

Totality and General Recursion

CTT is based on an untyped, open-ended computation system where totality is a semantic property that can be proved by induction.


JonPRL is an homage to the venerable Nuprl system, which is a proof assistant based on Constable et al’s Computational Type Theory, a variant of Martin-Löf's extensional type theory as first introduced in 1979. CTT is to be distinguished from formal type theory, which is the basis of Agda, Idris, Epigram and Coq.

The types of CTT are defined by imposing computation-respecting partial equivalence relations on the terms of a lazy computation system, which includes the untyped lambda calculus but which may be extended to support computational effects such as exceptions.