#
Computational Reflection
in the Calculus of Constructions
and its Application to Theorem Proving

Presented at TLCA'97, Nancy, France, April 1997. © Springer-Verlag.

# Authors

Harald Rueß

# Abstract

This paper describes a computational reflection mechanism
for the {\em calculus of constructions}.
In this framework it is possible to encode functions that
operate on {\em syntactic} representations on the meta-level
and to verify {\em semantic} relations between the object-level
denotations of the source and the target of meta-functions.
Moreover, it is shown how computational reflection can
easily be integrated with existing proof development systems
based on refinement methods in order to extend theorem proving
capabilities in a sound way.

gzipped postscript
or
postscript

# BibTeX Entry

@InProceedings{Ruess97,
author = "Harald Rue{\ss}",
title = "Computational Reflection in the Calculus of Constructions and Its Application to Theorem Proving",
editor = "R. Hindley",
booktitle = "Proceedings fo the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97)",
year = "1997",
publisher = "Springer-Verlag",
series = "Lecture Notes in Computer Science",
address = "Nancy, France",
month = apr
}

Harald Ruess:
ruess@csl.sri.com