README
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 19 Feb 2013 05:38:46 +0000
branchNominal2-Isabelle2013
changeset 3206 fb201e383f1b
parent 3205 645ee5189bec
child 3207 d3f7c8cce53b
child 3208 da575186d492
permissions -rw-r--r--
added Nominal2-Isabelle 2013 Branch
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
3204
b69c8660de14 fixed problem with not fresh enough permutation name in nominal_primrec
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2568
diff changeset
     4
Compilation of Tests
b69c8660de14 fixed problem with not fresh enough permutation name in nominal_primrec
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2568
diff changeset
     5
====================
b69c8660de14 fixed problem with not fresh enough permutation name in nominal_primrec
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2568
diff changeset
     6
b69c8660de14 fixed problem with not fresh enough permutation name in nominal_primrec
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2568
diff changeset
     7
isabelle build -d . -g Tests
b69c8660de14 fixed problem with not fresh enough permutation name in nominal_primrec
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 2568
diff changeset
     8
2452
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
     9
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
Subdirectories:
2452
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    11
===============
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    12
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    13
Nominal       ... main files for new Nominal Isabelle
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    14
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    15
Nominal/Ex    ... examples for new implementation
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    16
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    17
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    18
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    19
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    20
Outher Subdirectories:
39f8d405d7a2 updated todos
Christian Urban <urbanc@in.tum.de>
parents: 2382
diff changeset
    21
======================
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    23
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
    24
                  part of the Isabelle distribution)
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
1774
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    26
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
    27
                  Core-Haskell
c34347ec7ab3 separated general nominal theory into separate folder
Christian Urban <urbanc@in.tum.de>
parents: 1773
diff changeset
    28
3205
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3204
diff changeset
    29
Paper         ... accepted at ESOP
1773
c0eac04ae3b4 added README and moved examples into separate directory
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
2382
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    31
Pearl         ... accepted at ITP 
3205
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 3204
diff changeset
    32
Pearl-jv      ... accepted at LMCS
2382
e8b9c0ebf5dd added paper by james; some minor cleaning
Christian Urban <urbanc@in.tum.de>
parents: 1774
diff changeset
    33
2568
8193bbaa07fe merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
Christian Urban <urbanc@in.tum.de>
parents: 2523
diff changeset
    34
Quotient-Paper .. accepted to SAC
2453
Christian Urban <urbanc@in.tum.de>
parents: 2452
diff changeset
    35
Christian Urban <urbanc@in.tum.de>
parents: 2452
diff changeset
    36
Slides        ... various talks Christian gave recently