| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
A Meta-Model for the Isabelle API
| Title: | A Meta-Model for the Isabelle API |
| Authors: | Frédéric Tuong and Burkhart Wolff |
| Submission date: | 2015-09-16 |
| Abstract: |
We represent a theory of (a fragment of) Isabelle/HOL in
Isabelle/HOL. The purpose of this exercise is to write packages for
domain-specific specifications such as class models, B-machines, ...,
and generally speaking, any domain-specific languages whose
abstract syntax can be defined by a HOL "datatype". On this basis, the
Isabelle code-generator can then be used to generate code for global
context transformations as well as tactic code.
Consequently the package is geared towards parsing, printing and code-generation to the Isabelle API. It is at the moment not sufficiently rich for doing meta theory on Isabelle itself. Extensions in this direction are possible though. Moreover, the chosen fragment is fairly rudimentary. However it should be easily adapted to one's needs if a package is written on top of it. The supported API contains types, terms, transformation of global context like definitions and data-type declarations as well as infrastructure for Isar-setups. This theory is drawn from the Featherweight OCL project where it is used to construct a package for object-oriented data-type theories generated from UML class diagrams. The Featherweight OCL, for example, allows for both the direct execution of compiled tactic code by the Isabelle API as well as the generation of ".thy"-files for debugging purposes. Gained experience from this project shows that the compiled code is sufficiently efficient for practical purposes while being based on a formal model on which properties of the package can be proven such as termination of certain transformations, correctness, etc. |
| BibTeX: |
@article{Isabelle_Meta_Model-AFP,
author = {Frédéric Tuong and Burkhart Wolff},
title = {A Meta-Model for the Isabelle API},
journal = {Archive of Formal Proofs},
month = sep,
year = 2015,
note = {\url{http://isa-afp.org/entries/Isabelle_Meta_Model.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |