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

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

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.

# 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",