Termination in impure lambda-calculus

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.
Type de document :
Communication dans un congrès
Fundamentals of Software Engineering, 2012, Unknown, Springer, 7141, pp.128--142, 2012, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/hal-00909392
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 11:08:40
Dernière modification le : vendredi 20 avril 2018 - 15:44:24

Identifiants

  • HAL Id : hal-00909392, version 1

Collections

Citation

Romain Demangeon, Daniel Hirschkoff, Davide Sangiorgi. Termination in impure lambda-calculus. Fundamentals of Software Engineering, 2012, Unknown, Springer, 7141, pp.128--142, 2012, Lecture Notes in Computer Science. 〈hal-00909392〉

Partager

Métriques

Consultations de la notice

162