JonPRL
Proof Refinement Logic — Computational Type Theory

Features

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.