Gallina specification language

**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**

A formal language for specifying logical theories. Gallina is used in the proof-assistent system Coq.

Created on August 25, 2012 21:42:53
by Urs Schreiber
(82.113.106.150)