Sequent calculus as a compiler intermediate language

DOI10.1145/2951913.2951931MaRDI QIDQ2982003zbMATH OpenOpenAlexWikidataFDO

Authors Paul Downen, Luke Maurer, Zena M. Ariola, Simon Peyton-Jones

Publication date 10 May 2017

Published in Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2951913.2951931

zbMATH Keywords

compiler optimizationscontinuationsHaskellintermediate representationsnatural deductionsequent calculus

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Functional runtime systems within the lambda-sigma calculus
• Functional back-ends within the lambda-sigma calculus
• On the concurrent computational content of intermediate logics
• Computation with classical sequents
• Term sequent logic

Cited in

(3)

• A classical sequent calculus with dependent types
• A Church-style intermediate language for ML\(^{\text F}\)
• Compiling with classical connectives

Describes a project that uses

Uses Software

• Haskell
• GHC

This page was built for publication: Sequent calculus as a compiler intermediate language

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