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