Sciweavers

ENTCS
2008

Normalization for the Simply-Typed Lambda-Calculus in Twelf

13 years 10 months ago
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.
Andreas Abel
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Andreas Abel
Comments (0)