Re: [isabelle] antiquotations



On Mon, 11 Feb 2008, Jeremy Dawson wrote:

> Finally, is all this stuff documented anywhere?

Here are some references that might help:

 * Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the 
   Isabelle/Isar Framework. In Theorem Proving in Higher Order Logics, 
   TPHOLs 2007.
   http://www4.in.tum.de/~wenzelm/papers/isar-tool-framework.pdf

 * Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into 
   Isabelle/Isar. In J. Carette and F. Wiedijk, editors. Programming 
   Languages for Mechanized Mathematics Workshop (CALCULEMUS 2007). 
   http://www4.in.tum.de/~wenzelm/papers/Isar-SML.pdf

 * Amine Chaieb and Makarius Wenzel. Context aware Calculation and 
   Deduction --- Ring Equalities via Gröbner Bases in Isabelle. In M. 
   Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors. Towards 
   Mechanized Mathematical Assistants (CALCULEMUS 2007 and MKM 2007).
   http://www4.in.tum.de/~wenzelm/papers/context-methods.pdf

 * Makarius Wenzel.  The Isabelle/Isar Implementation Manual.  Distributed 
   with Isabelle2007 (incomplete).
   http://isabelle.in.tum.de/dist/Isabelle/doc/implementation.pdf

These things did not appear overnight out of the blue, but emerged from 
principles that have been present in Isabelle for many years already.

The following talk provides an overview of the general state of affairs of 
integrating everything into some kind of ``logical operating system'':

 * Makarius Wenzel.
   Aspects of locality in Isabelle --- local proofs, local theories, and 
   local everything.
   http://www.matf.bg.ac.yu/~janicic/locality.pdf

When using the system you do not have to understand all the details, but 
merely sit back comfortably and let the framework do most of the job. 
Complications mostly arise from trying to challange things by interfering 
with the low-level implementation layer.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.