Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Multi-Level Meta-Reasoning with Higher Order Abstract Syntax
Authors: Alberto Momigliano ; Simon Ambler
Date:Apr 2003
Publication Type:Conference Paper Publication Status:Published
Page Nos:375-391
Combining Higher Order Abstract Syntax (HOAS) and (co)-induction is well known to be problematic. In previous work [1] we have described the implementation of a tool called Hybrid, within Isabelle HOL, which allows object logics to be represented using HOAS, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such and Twelf. By explicitly referencing provability, we solve the problem of reasoning by (co)induction in presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications. We demonstrate the method by formally verifying the correctness of a compiler for (a fragment) of Mini-ML, following [10]. To further exhibit the flexibility of our system, we modify the target language with a notion of non-well-founded closure, inspired by Milner & Tofte [16] and formally verify via co-induction a subject reduction theorem for this modified language.
Links To Paper
1st Link
Bibtex format
author = { Alberto Momigliano and Simon Ambler },
title = {Multi-Level Meta-Reasoning with Higher Order Abstract Syntax},
book title = {},
publisher = {Springer},
year = 2003,
month = {Apr},
pages = {375-391},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh