Academic Journal
The tail-recursive SECD machine
| العنوان: | The tail-recursive SECD machine |
|---|---|
| المؤلفون: | John D. Ramsdell |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://www.ccs.neu.edu/home/ramsdell/papers/trsecd.pdf. |
| سنة النشر: | 1999 |
| المجموعة: | CiteSeerX |
| مصطلحات موضوعية: | tail recursion, tail call, SECD machine, CEK machine, verified implementation, Boyer-Moore theorem prover |
| الوصف: | One method for producing verified implementations of programming languages is to formally derive them from abstract machines. Tail-recursive abstract machines provide efficient support for iterative processes via the ordinary procedure call mechanism. This document argues that the use of tail-recursive abstract machines incurs only a small increase in theorem-proving burden when compared with what is required when using ordinary abstract machines. The position is supported by comparing correctness proofs performed using the Boyer-Moore theorem prover. A by-product of this effort is a syntactic criterion based on tail contexts for identifying which procedure calls must be implemented as tail calls. The concept of tail contexts was used in the latest Scheme Report, the only language specification known to the author that defines the requirement that its implementations must be tail recursive. |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.8133; http://www.ccs.neu.edu/home/ramsdell/papers/trsecd.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.8133 http://www.ccs.neu.edu/home/ramsdell/papers/trsecd.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.D0B20CD4 |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |