Polarised intermediate representation of lambda calculus with sums

DOI10.1109/LICS.2015.22zbMATH Open1394.68068MaRDI QIDQ4635798FDOQ4635798

Gabriel Scherer, Guillaume Munch-Maccagnoni

Publication date: 23 April 2018

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

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

zbMATH Keywords

\(\lambda\)-calculus

Mathematics Subject Classification ID

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

Cited In (4)

• The polarized \(\lambda\)-calculus
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Call-by-name extensionality and confluence
• Title not available (Why is that?)

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)