Sequent calculus as a compiler intermediate language

DOI10.1145/2951913.2951931MaRDI QIDQ2982003zbMATHOpenAlexWikidataFDO

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

natural deductionsequent calculuscontinuationsHaskellcompiler optimizationsintermediate representations

Mathematics Subject Classification ID

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

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 Church-style intermediate language for ML\(^{\text F}\)
• A classical sequent calculus with dependent types
• scientific article; zbMATH DE number 7243675 (Why is no real title available?)

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)