Skip to Main content Skip to Navigation
Conference papers

Termination in impure lambda-calculus

Romain Demangeon 1, 2 Daniel Hirschkoff 1, 2 Davide Sangiorgi 3, 4
2 PLUME - Preuves et Langages
LIP - Laboratoire de l'Informatique du Parallélisme
3 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
Abstract : We present a method for ensuring termination of lambda- calculi with references. This method makes it possible to combine measure- based techniques for termination of imperative languages with traditional approaches to termination in purely functional languages, such as logical relations. More precisely, the method lifts any termination proof for the purely functional simply-typed lambda-calculus to a termination proof for the lambda-calculus with references. The method can be made para- metric on the termination technique employed for the functional core.
Document type :
Conference papers
Complete list of metadatas
Contributor : Davide Sangiogi <>
Submitted on : Tuesday, November 26, 2013 - 11:08:40 AM
Last modification on : Friday, October 30, 2020 - 12:04:04 PM


  • HAL Id : hal-00909392, version 1



Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi. Termination in impure lambda-calculus. Fundamentals of Software Engineering, 2012, Unknown, Afghanistan. pp.128--142. ⟨hal-00909392⟩



Record views