This paper is concerned with developing a reflective architecture for formalizing and reasoning about entities that occur in the process of software development, such as specifications, theorems, programs, and proofs. The starting point is a syntactic extension of the type theory ECC. An encoding of this object calculus within itself comprises the meta-level, and reflection principles are provided for switching between different levels. These reflection principles are used to mix object- and meta-level reasoning, to generate "standard" units by executing meta-operators, and to apply formal tactics that allow for abstraction from the base logic.

Online Copy

Avalaible as Postscript (122 KB) or gzip'ed Postscript (37 KB)

BibTeX Entry

@InProceedings{RPvH95, author = "Harald Rueß, Holger Pfeifer, Friedrich W. von Henke", title = "Formalization and Reasoning in a Reflective Architecture", editor = "M. Ibrahim, P. Cointe, F. Cummins, F. Giunchiglia, and J. Malenfant", year = 1995, booktitle = "IJCAI 1995 Workshop on Reflection and Meta Level Architecture and their Application in AI", address = "Montreal, Canada", month = "August" }