ENTCS
2007
14 years 16 days ago
2007
We formalize in the logical framework ATS/LF a proof based on Tait’s method that establishes the simply-typed lambda-calculus being strongly normalizing. In malization, we emplo...
APLAS
2007
ACM
14 years 4 months ago
2007
ACM
Abstract. We introduce the concept of guarded saturated sets, saturated sets of strongly normalizing terms closed under folding of corecursive functions. Using this tool, we can mo...
TLCA
2001
Springer
14 years 5 months ago
2001
Springer
We introduce λµ→∧∨⊥ , an extension of Parigot’s λµ-calculus where disjunction is taken as a primitive. The associated reduction relation, which includes the permutati...
RTA
2007
Springer
14 years 6 months ago
2007
Springer
We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The m...
LICS
2007
IEEE
14 years 6 months ago
2007
IEEE
When enriching the λ-calculus with rewriting, union types may be needed to type all strongly normalizing terms. However, with rewriting, the elimination rule (∨ E) of union typ...