Skip to main content

1991 | OriginalPaper | Buchkapitel

Reflecting the Open-Ended Computation System of Constructive Type Theory

verfasst von : Robert L. Constable, Stuart F. Allen, Douglas J. Howe

Erschienen in: Logic, Algebra, and Computation

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.

search-config
loading …

The computation system of constructive type theory is open-ended so that theorems about computation will hold for a broad class of extensions to the system. We show that despite this openness it is possible to completely reflect the computation system into the language in a clear way by adding simple primitive concepts that anticipate the reflection. This work provides a hook for developing methods to modify the built-in evaluator and to treat the issues of intensionality and computational complexity in programming logics and provides a basis for reflecting the deductive apparatus of type theory.

Metadaten
Titel
Reflecting the Open-Ended Computation System of Constructive Type Theory
verfasst von
Robert L. Constable
Stuart F. Allen
Douglas J. Howe
Copyright-Jahr
1991
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-642-76799-9_7