Call-by-Value solvability, revisited

Beniamino Accattoli 1, 2 Luca Paolini 3
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman's call-by-value lambda-CBV calculus and from Accattoli and Kesner's substitution calculus lambda-sub. In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.
Type de document :
Communication dans un congrès
11th International Symposium on Functional and Logic Programming - FLOPS 2012, May 2012, Kobe, Japan. 2012
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00780358
Contributeur : Beniamino Accattoli <>
Soumis le : mercredi 23 janvier 2013 - 17:39:29
Dernière modification le : jeudi 10 mai 2018 - 02:06:35
Document(s) archivé(s) le : mercredi 24 avril 2013 - 04:00:12

Fichier

FLOPS2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00780358, version 1

Collections

Citation

Beniamino Accattoli, Luca Paolini. Call-by-Value solvability, revisited. 11th International Symposium on Functional and Logic Programming - FLOPS 2012, May 2012, Kobe, Japan. 2012. 〈hal-00780358〉

Partager

Métriques

Consultations de la notice

216

Téléchargements de fichiers

150