Grokking the Sequent Calculus (Functional Pearl)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866908338666602496 |
|---|---|
| author | Binder, David Tzschentke, Marco Müller, Marius Ostermann, Klaus |
| author_facet | Binder, David Tzschentke, Marco Müller, Marius Ostermann, Klaus |
| contents | The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The λμμ-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 λμμ-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 λμμ-calculus as a compiler intermediate language. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_14719 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Grokking the Sequent Calculus (Functional Pearl) Binder, David Tzschentke, Marco Müller, Marius Ostermann, Klaus Programming Languages The sequent calculus is a proof system which was designed as a more symmetric alternative to natural deduction. The λμμ-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 λμμ-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 λμμ-calculus as a compiler intermediate language. |
| title | Grokking the Sequent Calculus (Functional Pearl) |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2406.14719 |