Skip to main content
PRL Project

Reflecting Higher-Order Abstract Syntax in Nuprl

by Eli Barzilay, Stuart F. Allen

Track B Proceedings of 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '02)

  • unofficial copies PDF, PS

This document describes part of an effort to achieve in Nuprl a practical reflection of its expression syntax. This reflection is done at the granularity of the operators; in particular, each operator of the syntax is denoted by another operator of the same syntax. Further, the syntax has binding operators, and we organize reflection not around the concrete binding syntax, but instead, around the abstract higher-order syntax. We formulate and prove the correctness of a core rule for inferring well-formedness of instances of operator-denoting operator

There is also a list of HOAS Articles and a Citation Graph for them; most are not cited in the above paper.

bibTex ref: BA02

cite link