HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-01160579
Contributor : Guillaume Munch-Maccagnoni Connect in order to contact the contributor
Submitted on : Thursday, December 3, 2015 - 6:56:00 PM
Last modification on : Friday, February 4, 2022 - 3:10:24 AM
Long-term archiving on: : Saturday, April 29, 2017 - 5:23:56 AM

File

principles.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

966

Files downloads

893