**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

The *Archive of Formal Proofs* (*AFP*) is an online library of formal proofs, examples, and projects formalized in the proof assistant Isabelle.

In contrast to other current projects, AFP and Isabelle are based on classical set theoretic foundations. It already comprises a large amount of concepts like smooth manifolds, Markov models, Monoidal Categories, or ordinals and cardinals to mention a few.

Last revised on May 20, 2019 at 08:00:41. See the history of this page for a list of all contributions to it.