Normalization for the Simply-Typed Lambda-Calculus in Twelf

Normalization for the simply-typed -calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait's computability method does not seem to be directly usable, a syntactical proof is adapted and formalized instead. In this case study, some boundaries of Twelf current capabilities are touched and discussed.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Andreas Abel
• Keywords: Computability Method, Edinburgh Logical Framework, ENTCS 2008, Proof-theoretical Restrictions