The intuitionistic fragment of the call-by-name version of Curien andHerbelin's λ--μ-μ~-calculus is isolated and proved stronglynormalising by means of an embedding into the simply-typed lambda-calculus. Ourembedding is a continuation-and-garbage-passing style translation, theinspiring idea coming from Ikeda and Nakazawa's translation of Parigot'sλ-μ-calculus. The embedding strictly simulates reductions while usualcontinuation-passing-style transformations erase permutative reduction steps.For our intuitionistic sequent calculus, we even only need "units of garbage"to be passed. We apply the same method to other calculi, namely successiveextensions of the simply-typed λ-calculus leading to our intuitionisticsystem, and already for the simplest extension we consider (λ-calculuswith generalised application), this yields the first proof of strongnormalisation through a reduction-preserving embedding. The results obtainedextend to second and higher-order calculi.
展开▼
