README
author Christian Urban <urbanc@in.tum.de>
Wed, 02 Jan 2019 21:09:05 +0000
changeset 208 a5afc26b1d62
parent 198 65b178574112
permissions -rw-r--r--
final version
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
208
a5afc26b1d62 final version
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
     1
a5afc26b1d62 final version
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
     2
a5afc26b1d62 final version
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
     3
a5afc26b1d62 final version
Christian Urban <urbanc@in.tum.de>
parents: 198
diff changeset
     4
Tested with Isabelle 2017
146
Christian Urban <urbanc@in.tum.de>
parents: 83
diff changeset
     5
Christian Urban <urbanc@in.tum.de>
parents: 83
diff changeset
     6
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     7
Theories:
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     8
=========
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
     9
195
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
    10
 Graphs.thy              A relational graph library 
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
    11
 RTree                   Rooted tree graphs 
35
92f61f6a0fe7 added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 29
diff changeset
    12
 Max.thy                 Some generic facts about Max.
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    13
 Precedence_ord.thy      A theory of precedences.
64
b4bcd1edbb6d renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 52
diff changeset
    14
 PIPDefs.thy             The formal definition of the PIP-model.
b4bcd1edbb6d renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 52
diff changeset
    15
 PIPBasics.thy           Basic properties of the PIP-model.
b4bcd1edbb6d renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 52
diff changeset
    16
 Correctness.thy         The correctness proof of the PIP-model.
b4bcd1edbb6d renamed files
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 52
diff changeset
    17
 Implementation.thy      Properties interesting for an implementation.
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    18
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
198
65b178574112 updated
Christian Urban <urbanc@in.tum.de>
parents: 197
diff changeset
    20
The repository can be checked using Isabelle 2016-1.
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    21
45
fc83f79009bd updated for Isabelle 2015
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 35
diff changeset
    22
  isabelle build -c -v -d . PIP
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    23
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    24
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    25
Othe directories are:
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    26
=====================
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    28
  Slides
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    29
  Paper
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 47
diff changeset
    30
  Journal:     isabelle build -c -v -d . Journal
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    31
  Literature
47
2e6c8d530216 Just a test change
xingyuan zhang <xingyuanzhang@126.com>
parents: 45
diff changeset
    32
  
0
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    33
29
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    34
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    35
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    36
408ff78ce28f updated readme
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 0
diff changeset
    37
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 29
diff changeset
    38
195
6b26b1fd4da5 polished
Christian Urban <urbanc@in.tum.de>
parents: 151
diff changeset
    39