README
author Christian Urban <urbanc@in.tum.de>
Sat, 28 Aug 2010 13:41:31 +0800
changeset 2446 63c936b09764
parent 2382 e8b9c0ebf5dd
child 2452 39f8d405d7a2
permissions -rw-r--r--
updated to new Isabelle
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
This repository contain a new implementation of
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
Nominal Isabelle.
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
Subdirectories:
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
     6
Attic         ... old version of the quotient package (is now 
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
     7
                  part of the Isabelle distribution)
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
     9
Literature    ... some relevant papers about binders and
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    10
                  Core-Haskell
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    11
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    12
Nominal-General . implementation of the abstract nominal theory
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    14
Nominal       ... main files for new Nominal Isabelle
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    16
Nominal/Ex    ... examples for new implementation
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    17
2382
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    18
Paper         ... submitted to POPL
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
2382
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    20
Pearl         ... accepted at ITP 
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    21
Pearl-jv      ... journal version
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    22
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    23
Quotient-Paper .. submitted to APLAS