Sciweavers

TLCA
2009
Springer
14 years 6 months ago
Lexicographic Path Induction
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...
Jeffrey Sarnat, Carsten Schürmann
TLCA
2009
Springer
14 years 6 months ago
Initial Algebra Semantics for Cyclic Sharing Structures
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...
Makoto Hamana
TLCA
2009
Springer
14 years 6 months ago
Parametricity for Haskell with Imprecise Error Semantics
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...
Florian Stenger, Janis Voigtländer
TLCA
2009
Springer
14 years 6 months ago
Relating Classical Realizability and Negative Translation for Existential Witness Extraction
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...
Alexandre Miquel
TLCA
2009
Springer
14 years 6 months ago
Syntax for Free: Representing Syntax with Binding Using Parametricity
We show that, in a parametric model of polymorphism, the type ∀α.((α → α) → α) → (α → α → α) → α is isomorphic to closed n terms. That is, the type of closed ...
Robert Atkey
TLCA
2009
Springer
14 years 6 months ago
A Logical Foundation for Environment Classifiers
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...
Takeshi Tsukada, Atsushi Igarashi