Academic Journal
The λΠ-calculus Modulo as a Universal Proof Language
| العنوان: | The λΠ-calculus Modulo as a Universal Proof Language |
|---|---|
| المؤلفون: | Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.cri.ensmp.fr/people/hermant/docs/2012/PxTP.pdf. |
| سنة النشر: | 2012 |
| المجموعة: | CiteSeerX |
| الوصف: | The λΠ-calculus forms one of the vertices in Barendregt’s λ-cube and has been used as the core language for a number of logical frameworks. Following earlier extensions of natural deduction [14], Cousineau and Dowek [11] generalize the definitional equality of this well studied calculus to an arbitrary congruence generated by rewrite rules, which allows for more faithful encodings of foreign logics. This paper motivates the resulting language, the λΠ-calculus modulo, as a universal proof language, capable of expressing proofs from many other systems without losing their computational properties. We further show how to very simply and efficiently check proofs from this language. We have implemented this scheme in a proof checker called Dedukti. |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.706.3363; http://www.cri.ensmp.fr/people/hermant/docs/2012/PxTP.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.706.3363 http://www.cri.ensmp.fr/people/hermant/docs/2012/PxTP.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.AC78E569 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |