Polarised intermediate representation of lambda calculus with sums

DOI10.1109/LICS.2015.22MaRDI QIDQ4635798zbMATH OpenFDO

Authors Guillaume Munch-Maccagnoni, Gabriel Scherer

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

zbMATH Keywords

\(\lambda\)-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• The polarized \(\lambda\)-calculus
• Some lambda calculi with categorical sums and products
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Extensional Rewriting with Sums
• Deciding equivalence with sums and the empty type

Cited in

(5)

• Call-by-name extensionality and confluence
• Deciding equivalence with sums and the empty type
• The polarized \(\lambda\)-calculus
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• scientific article; zbMATH DE number 7533346 (Why is no real title available?)

This page was built for publication: Polarised intermediate representation of lambda calculus with sums

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635798)