Termination in impure lambda-calculus - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Termination in impure lambda-calculus

Résumé

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.

Domaines

Informatique
Fichier non déposé

Dates et versions

hal-00909392 , version 1 (26-11-2013)

Identifiants

  • HAL Id : hal-00909392 , version 1

Citer

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

Partager

Gmail Facebook X LinkedIn More