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ß


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

  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: