View PDF

The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The {\lambda}{\mu}{\mu}-calculus is a term assignment system for the sequent calculus and a great foundation for compiler intermediate languages due to its first-class representation of evaluation contexts. Unfortunately, only experts of the sequent calculus can appreciate its beauty. To remedy this, we present the first introduction to the {\lambda}{\mu}{\mu}-calculus which is not directed at type theorists or logicians but at compiler hackers and programming-language enthusiasts. We do this by writing a compiler from a small but interesting surface language to the {\lambda}{\mu}{\mu}-calculus as a compiler intermediate language.

Submission history

From: David Binder [view email]
[v1] Thu, 20 Jun 2024 20:30:37 UTC (270 KB)

||||I|||| Skip to main content We gratefully acknowledge support from the Simons Foundation, member institutions , and all contributors. Donate > cs > arXiv:2406.14719 Help | Advanced Search All fields Title Author Abstract Comments Journal reference ACM classification MSC classification Report number arXiv identifier DOI ORCID arXiv author ID Help pages Full text Search GO quick links * Login * Help Pages * About Computer Science > Programming Languages arXiv:2406.14719 (cs) [Submitted on 20 Jun 2024] Title: Grokking the Sequent Calculus (Functional Pearl) Authors: David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann View a PDF of the paper titled Grokking the Sequent Calculus (Functional Pearl), by David Binder and 3 other authors View PDF Abstract: The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The {\lambda}{\mu}{\mu}-calculus is a term assignment system for the sequent calculus and a great foundation for compiler intermediate languages due to its first-class representation of evaluation contexts. Unfortunately, only experts of the sequent calculus can appreciate its beauty. To remedy this, we present the first introduction to the {\lambda}{\mu}{\mu}-calculus which is not directed at type theorists or logicians but at compiler hackers and programming-language enthusiasts. We do this by writing a compiler from a small but interesting surface language to the {\lambda}{\mu}{\mu}-calculus as a compiler intermediate language. Comments: Preprint of the paper accepted at ICFP '24 Subjects: Programming Languages (cs.PL) Cite as: arXiv:2406.14719 [cs.PL] (or arXiv:2406.14719v1 [cs.PL] for this version) Submission history From: David Binder [view email] [v1] Thu, 20 Jun 2024 20:30:37 UTC (270 KB) Full-text links: Access Paper: View a PDF of the paper titled Grokking the Sequent Calculus (Functional Pearl), by David Binder and 3 other authors * View PDF * TeX Source * Other Formats view license Current browse context: cs.PL < prev | next > new | recent | 2024-06 Change to browse by: cs References & Citations * NASA ADS * Google Scholar * Semantic Scholar a export BibTeX citation Loading... BibTeX formatted citation × loading... Data provided by: Bookmark Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Code, Data and Media Associated with this Article Links to Code Toggle CatalyzeX Code Finder for Papers (What is CatalyzeX?) DagsHub Toggle DagsHub (What is DagsHub?) GotitPub Toggle Gotit.pub (What is GotitPub?) Links to Code Toggle Papers with Code (What is Papers with Code?) ScienceCast Toggle ScienceCast (What is ScienceCast?) Demos Demos Replicate Toggle Replicate (What is Replicate?) Spaces Toggle Hugging Face Spaces (What is Spaces?) Spaces Toggle TXYZ.AI (What is TXYZ.AI?) Related Papers Recommenders and Search Tools Link to Influence Flower Influence Flower (What are Influence Flowers?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Core recommender toggle CORE Recommender (What is CORE?) About arXivLabs arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs. Which authors of this paper are endorsers? | Disable MathJax (What is MathJax?) * About * Help * Click here to contact arXiv Contact * Click here to subscribe Subscribe * Copyright * Privacy Policy * Web Accessibility Assistance * arXiv Operational Status Get status notifications via email or slack

Search across your past Websets

Articles: compiler design, beginner-friendly, published in 2025

Search Criteria

Enrichments

Find more results