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 parametric on the termination technique employed for the functional core

Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi (2012). Strong Normalisation in λ-Calculi with References. Berlino : Springer [10.1007/978-3-642-29320-7_9].

Strong Normalisation in λ-Calculi with References

SANGIORGI, DAVIDE
2012

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 parametric on the termination technique employed for the functional core
2012
Fundamentals of Software Engineering: Revised Selected Papers
128
142
Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi (2012). Strong Normalisation in λ-Calculi with References. Berlino : Springer [10.1007/978-3-642-29320-7_9].
Romain Demangeon;Daniel Hirschkoff;Davide Sangiorgi
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/148927
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact