تقرير
Grokking the Sequent Calculus (Functional Pearl)
| العنوان: | Grokking the Sequent Calculus (Functional Pearl) |
|---|---|
| المؤلفون: | Binder, David, Tzschentke, Marco, Müller, Marius, Ostermann, Klaus |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Programming Languages |
| الوصف: | 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. Comment: Preprint of the paper accepted at ICFP '24 |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2406.14719 |
| رقم الأكسشن: | edsarx.2406.14719 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |