Academic Journal
Beluga: A framework for programming and reasoning with deductive systems (system description
| العنوان: | Beluga: A framework for programming and reasoning with deductive systems (system description |
|---|---|
| المؤلفون: | Brigitte Pientka, Joshua Dunfield |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.cs.cmu.edu/%7Ejoshuad/papers/beluga-system/Pientka10_Beluga.pdf. |
| بيانات النشر: | SpringerVerlag |
| سنة النشر: | 2010 |
| المجموعة: | CiteSeerX |
| الوصف: | Beluga is an environment for programming and reasoning about formal systems given by axioms and inference rules. It implements the logical framework LF for specifying and prototyping formal systems via higher-order abstract syntax. It also supports reasoning: the user implements inductive proofs about formal systems as dependently typed recursive functions. A distinctive feature of Beluga is that it not only represents binders using higher-order abstract syntax, but directly supports reasoning with contexts. Contextual objects represent hypothetical and parametric derivations, leading to compact and elegant proofs. Our test suite includes standard examples such as the Church-Rosser theorem, type uniqueness, proofs about compiler transformations, and preservation and progress for various ML-like languages. We also implemented proofs of structural properties of expressions and paths in expressions. Stating these properties requires nesting of quantifiers and implications, demonstrating the expressive power of Beluga. 1 |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.3950; http://www.cs.cmu.edu/%7Ejoshuad/papers/beluga-system/Pientka10_Beluga.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.188.3950 http://www.cs.cmu.edu/%7Ejoshuad/papers/beluga-system/Pientka10_Beluga.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.DC414456 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |