Abstract
Higher-order abstract syntax (HOAS), an elegant and declarative treatment of object-level abstraction and substitution, is difficult to treat in proofs involving induction. A meta-logic that can be used to reason about judgements coded using HOAS is presented. This meta-logic is an extension of a simple intuitionistic logic that admits higher-order quantification over simply typed -terms as well as induction and a notion of definition. The meta-logic results can specify various logical frameworks and a large range of judgements regarding programming languages and inference systems. These points are illustrated through examples.
| Original language | English |
|---|---|
| Pages (from-to) | 434-445 |
| Number of pages | 12 |
| Journal | Proceedings - Symposium on Logic in Computer Science |
| Publication status | Published - 1 Jan 1997 |
| Externally published | Yes |
| Event | Proceedings of the 1997 12th Annual IEEE Symposium on Logic in Computer Science, LICS - Warsaw, Pol Duration: 29 Jun 1997 → 2 Jul 1997 |