[[!redirects Elf]] +-- {: .rightHandSide} +-- {: .toc .clickDown tabindex="0"} ### Context #### Type theory +-- {: .hide} [[!include type theory - contents]] =-- #### Deduction and Induction +-- {: .hide} [[!include deduction and induction - contents]] =-- #### Constructivism, Realizability, Computability +-- {: .hide} [[!include constructivism - contents]] =-- #### Foundations +-- {: .hide} [[!include foundations - contents]] =-- =-- =-- #Contents# * table of contents {:toc} ## Idea **LF** ([Pfenning 91](#Pfenning91), [Harper-Honsell-Plotkin 93](#HarperHonsellPlotkin93)) is a certain [[logical framework]] based on [[dependent type theory|dependent]] [[intuitionistic type theory]]. Variants include the _Edinburgh logical framework_, abbreviated "Elf", and _linear LF_, abbreviated LLF ([Pfenning 96](Pfenning96)), the latter capturing also [[dependent linear type theory]]. ## Related concepts * [[Automath]] * [[Twelf]] ## References The logical framework LF originates around * {#Pfenning91} [[Frank Pfenning]], _Logic Programming in the LF Logical Framework_ (1991) ([web](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.3910)) * {#HarperHonsellPlotkin93} [[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 * _[Elf Homepage](http://www.cs.cmu.edu/~fp/elf.html)_ Extension to a framework for [[dependent linear type theory]] called LLF is discussed in * {#Pfenning96} Iliano Cervesato, [[Frank Pfenning]], _A Linear Logical Framework_, 1996, ([web](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.21.1152)) * {#WCFW03} 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](http://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf)) category: software [[!redirects Edinburgh Logical Framework]] [[!redirects Edinburgh logical framework]] [[!redirects ELF]] [[!redirects LF]]