As a prerequisite for change management, a dependency tracking
relation is needed. Each theory morphism and each (theoroidal)
(co)morphism (see also ticket #172) leads to a tracking relation
between the symbols and axioms of the source and the target
signature/theory. The intended semantics is that tr(sy1,sy2) means
that sy2 is contained in the entity that is the image of symbol
sy1. For example, a function symbol may be mapped (by a comorphism) to
two function symbols, or to one function symbol and an axiom.
Important properties:
Change management tracks which symbols and axioms are needed to
prove a specific theorem. These symbols and axioms then can,
via the tracking relation, also be traced back to their origin.
If in the changed development graph, they are still there, then
then the proof is still valid.
Entities on the abstract level
------------------------------
- Objects = symbols? what are objects? all subterms? symbols are those entities that can be mapped in a signature morphism
- Statments
- Theories / signatures
- object is contained in statement, theory
- theory is made of signature and statements
- signature is made of symbols??? This would lead to "subsort symbols" etc.
- Statement is made of objects??? This would lead to parchments. Logics have to specify something like an XML schema, such that we can look into the abstract syntax tree of all entities. However, this has no logical meaning. Then, we can also OMDocify things and use variables, constants, application, binders, with
typing. Again, the logical important thing is the tracking relation. Provide this feature only for OmDoc-based formalisms? Or make it into a general design principle (hard migration!). Structured presentation of statements does not lead to logical decomposition. Rather, the statement is computed and then treated as if it were an atomic object in the target theory.
DFG/DFKI projects
=================
CASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
CoCASL/Concurrent Haskell (George's events)/SPIN/CspCASL (Till, Shi, Lutz)
Modal-CASL als Anforderungssprache
div. Prozessalgebren (wir stellen den allg. Rahmen)
HetCASL/Hets (Till)
Abstract robotics (cxl, paolo)
AWE II / General FM (cxl, bkb)
Tool chains
===========
(2) Expose commutativity in tool chains. It is certainly usefull to get
overviews of tool compositions. However, what happened with proven techniques
to do this like T-diagrams? They were first described in
Jay Earley , Howard Sturgis, A formalism for translator interactions,
Communications of the ACM, v.13 n.10, p.607-617, Oct. 1970
[doi>10.1145/355598.362740]
Popular accounts are:
A modified version can be found in:
@article{197336,
author = {Andrew W. Appel},
title = {Axiomatic bootstrapping: a guide for compiler hackers},
journal = {ACM Trans. Program. Lang. Syst.},
volume = {16},
number = {6},
year = {1994},
issn = {0164-0925},
pages = {1699--1718},
publisher = {ACM},
address = {New York, NY, USA},
}
Isabelle
========
- theory morphisms (cxl)
- Latin2: Mizar->Isabelle, PVS->Isabelle
Joe Hurd (binary format for HOL) PLMMS 09
Cezary Kaliszyk (HOL import)
Klaus Grue LogiWeb
- Isabelle parser
terms of basic logic, annotated with datatypes etc.
4 levels:
- source+markup (locales, non-logical stuff, ...)
- code_gen (Haftmann) intermediate language, Haskell-like
datatype, function, etc., useful for translation to Haskell etc.
- in parallel: find_theorems (leave alone concealed theorems)
-> additional theorems
- Typedef.get_info, Cpodef
- spec_rules: src/Pure/Isar/spec_rules.ML
how is HOL.plus specified?
unknown (axiomatic)
equiontional (fun, primrec)
inductive (relational)
coinductive
- logical foundation: types, consts (typeclasses, sorts), thms
- LF coding? Isabelle as a LF for Hets
Cube, CTT
- nice view on tool-generated Isabelle theories
- either fancy syntax rules
- or (better) annotated source
- using PIDE for Hets (asynchronous editing - checking - proving)
- Ubuntu package
- isomorphism theorems
- HOL-light to Isabelle. Descision procedures?
- model finders (e.g. nitpick, quickcheck) Lukas Bulwahn, Jasmin Blanchette (Vortrag CADE)
- IsaPlanner
- default simpset and claset setup