TLCA
2009
Springer
14 years 7 months ago
2009
Springer
Abstract. Programming languages theory is full of problems that reduce to proving the consistency of a logic, such as the normalization of typed lambda-calculi, the decidability of...
TLCA
2009
Springer
14 years 7 months ago
2009
Springer
Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanis...
TLCA
2009
Springer
14 years 7 months ago
2009
Springer
Types play an important role both in reasoning about Haskell and for its implementation. For example, the Glasgow Haskell Compiler performs certain fusion transformations that are...
TLCA
2009
Springer
14 years 7 months ago
2009
Springer
Friedman showed how to turn a classical proof of a Σ0 1 formula into an intuitionistic proof of the same formula, thus giving an effective method to extract witnesses from classi...
TLCA
2009
Springer
14 years 7 months ago
2009
Springer
We show that, in a parametric model of polymorphism, the type ∀α.((α → α) → α) → (α → α → α) → α is isomorphic to closed n terms. That is, the type of closed ...
TLCA
2009
Springer
14 years 7 months ago
2009
Springer
Taha and Nielsen have developed a multi-stage calculus λα with a sound type system using the notion of environment classifiers. They are special identifiers, with which code fr...