306a7fd82e790b3c00ba5cf806ccd6c0108061b5Lennart PoetteringAs a prerequisite for change management, a dependency tracking

335aa753fa60ba0bb3c9fe679c761d5f1f3b1588Lennart Poetteringrelation is needed. Each theory morphism and each (theoroidal)

335aa753fa60ba0bb3c9fe679c761d5f1f3b1588Lennart Poettering(co)morphism (see also ticket #172) leads to a tracking relation

335aa753fa60ba0bb3c9fe679c761d5f1f3b1588Lennart Poetteringbetween the symbols and axioms of the source and the target

3b63d2d31d0850bd7a81ab9b468218d2c4c461e8Lennart Poetteringsignature/theory. The intended semantics is that tr(sy1,sy2) means

3b63d2d31d0850bd7a81ab9b468218d2c4c461e8Lennart Poetteringthat sy2 is contained in the entity that is the image of symbol

46574a5b4afeac0c3f69f15ce47c460309cb9becLennart Poetteringsy1. For example, a function symbol may be mapped (by a comorphism) to

46574a5b4afeac0c3f69f15ce47c460309cb9becLennart Poetteringtwo function symbols, or to one function symbol and an axiom.

46574a5b4afeac0c3f69f15ce47c460309cb9becLennart Poettering

85ed27f699939f75b8422ae67e016bdf9f439da9Lennart PoetteringImportant properties:

447be1550523114f96c7f9eacb9d6a1ff6ca4197Lennart PoetteringChange management tracks which symbols and axioms are needed to

c7b508592b28ee1e62350f0d249856811371f631Lennart Poetteringprove a specific theorem. These symbols and axioms then can,

afbf835326b0cc05c282b43f14ed501977de2004Lennart Poetteringvia the tracking relation, also be traced back to their origin.

4bb2357f77c875976de5e238a5783e4e136b37b5Lennart PoetteringIf in the changed development graph, they are still there, then

4bb2357f77c875976de5e238a5783e4e136b37b5Lennart Poetteringthen the proof is still valid.

93a45c562a1989dfbb2dd08c65f8a21b02959934Lennart Poettering

addab137cd8d318e4f543ca56018ee23d51aaca9Lennart PoetteringEntities on the abstract level

b2423f1f436f847d9fc96a63679be2b5552b6bafLennart Poettering------------------------------

449ddb2d23a63ca4c8cd70d13a070fba87c1fb30Lennart Poettering- Objects = symbols? what are objects? all subterms? symbols are those entities that can be mapped in a signature morphism

97c4a07df982ee967705022feaba9be33947abf0Lennart Poettering- Statments

b574fa098d2827359c31a2d922b729725a8c6c8cLennart Poettering- Theories / signatures

f61448083198dc0e4e0d19a916bcd478336cc85dLennart Poettering

6e200d55ae538fc29360cdaa9863f30cdddf58f3Lennart Poettering- object is contained in statement, theory

6e200d55ae538fc29360cdaa9863f30cdddf58f3Lennart Poettering- theory is made of signature and statements

dfac97b21e00cd3617ba817227db7b621841b5ccLennart Poettering- signature is made of symbols??? This would lead to "subsort symbols" etc.

dfac97b21e00cd3617ba817227db7b621841b5ccLennart Poettering- 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

f0b02ca2afa806efb73b43a81204ff21c4c65446Lennart Poetteringtyping. 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.

f92a18f5274ad506aed600b2ed8f4a560c510807Lennart Poettering

5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering

5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering

5e6afdd3d359fc42de7ac432243e98673577e81fLennart Poettering

fb1bd35a5dd1ad5cfd848fdbe0d64ac53a122af0Lennart Poettering

cd6d0a456bc9c45fa79316fc5896e4a3ae75a30bLennart Poettering

cd6d0a456bc9c45fa79316fc5896e4a3ae75a30bLennart PoetteringDFG/DFKI projects

c24eb49e6aecd6de2ad450083e826d4c9d9c75b6Lennart Poettering=================

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},

doi = {http://doi.acm.org/10.1145/197320.197336},

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