| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 422231 | Electronic Notes in Theoretical Computer Science | 2008 | 14 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
