Polarised Intermediate Representation of Lambda Calculus with Sums

Abstract : The theory of the λ-calculus with extensional sums is more complex than with only pairs and functions. We propose an untyped representation—an intermediate calculus—for the λ-calculus with sums, based on the following principles: 1) Computation is described as the reduction of pairs of an expression and a context; the context must be represented inside-out, 2) Operations are represented abstractly by their transition rule, 3) Positive and negative expressions are respectively eager and lazy; this polarity is an approximation of the type. We offer an introduction from the ground up to our approach, and we review the benefits. A structure of alternating phases naturally emerges through the study of normal forms, offering a reconstruction of focusing. Considering further purity assumption, we obtain maximal multi-focusing. As an application, we can deduce a syntax-directed algorithm to decide the equivalence of normal forms in the simply-typed λ-calculus with sums, and justify it with our intermediate calculus.
Type de document :
Communication dans un congrès
Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015), Jul 2015, Kyoto, Japan. 〈10.1109/LICS.2015.22〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01160579
Contributeur : Guillaume Munch-Maccagnoni <>
Soumis le : jeudi 3 décembre 2015 - 18:56:00
Dernière modification le : mercredi 14 décembre 2016 - 01:07:26
Document(s) archivé(s) le : samedi 29 avril 2017 - 05:23:56

Fichier

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

Identifiants

Collections

Citation

Guillaume Munch-Maccagnoni, Gabriel Scherer. Polarised Intermediate Representation of Lambda Calculus with Sums. Thirtieth Annual ACM/IEEE Symposium on Logic In Computer Science (LICS 2015), Jul 2015, Kyoto, Japan. 〈10.1109/LICS.2015.22〉. 〈hal-01160579v2〉

Partager

Métriques

Consultations de
la notice

435

Téléchargements du document

277