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
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
basic constructions:
strong axioms
LF (Pfenning 91, Harper-Honsell-Plotkin 93) is a certain logical framework based on dependent intuitionistic type theory. Variants include the Edinburgh logical framework, abbreviated “Elf”, and linear LF, abbreviated LLF (Pfenning 96), the latter capturing also dependent linear type theory.
The logical framework LF originates around
Frank Pfenning, Logic Programming in the LF Logical Framework (1991) (web)
Robert Harper, F. Honsell, G. Plotkin, A framework for defining logics, Journal for the association for computing machinery 40(1):143-184 (1993)
For Elf see
Extension to a framework for dependent linear type theory called LLF is discussed in
Iliano Cervesato, Frank Pfenning, A Linear Logical Framework, 1996, (web)
Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker, A concurrent logical framework I: Judgments and properties, CMU technical report CMU-CS-02-101, revised May 2003 (web)