The lambda-se-calculus does not preserve strong normalisation
Abstract
Kamareddine, F., & Ríos (1997) conjecture that the λ s e -calculus preserves the strong normalisation of the λ-calculus. We prove here that this conjecture is false.
Related papers
- lambda-nu, A Calculus of Explicit Substitutions which Preserves Strong Normalisation JFP 1996
- Extending a lambda-Calculus with Explicit Substitution which Preserves Strong Normalisation Into a Confluent Calculus on Open Terms JFP 1997
- Strong Normalisation for the Linear Term Calculus JFP 1995
- Foundations of strong call by need ICFP 2017
- Computational Types from a Logical Perspective JFP 1998
- Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums POPL 2004
- Pure type systems with corecursion on streams: from finite to infinitary normalisation ICFP 2012
- On Polymorphic Sessions and Functions - A Tale of Two (Fully Abstract) Encodings ESOP 2018