--- a/Paper/Paper.thy Fri Mar 19 15:43:59 2010 +0100
+++ b/Paper/Paper.thy Fri Mar 19 17:20:25 2010 +0100
@@ -220,8 +220,30 @@
can perform in HOL is illustrated by the following picture:
\begin{center}
- figure
- %\begin{pspicture}(0.5,0.0)(8,2.5)
+ \begin{tikzpicture}
+ %\draw[step=2mm] (-4,-1) grid (4,1);
+
+ \draw[very thick] (0.7,0.4) circle (4.25mm);
+ \draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);
+ \draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);
+
+ \draw (-2.0, 0.845) -- (0.7,0.845);
+ \draw (-2.0,-0.045) -- (0.7,-0.045);
+
+ \draw ( 0.7, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]clas.\end{tabular}};
+ \draw (-2.4, 0.4) node {\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};
+ \draw (1.8, 0.48) node[right=-0.1mm]
+ {\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ (sets of raw terms)\end{tabular}};
+ \draw (0.9, -0.35) node {\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};
+ \draw (-3.25, 0.55) node {\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};
+
+ \draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);
+ \draw (-0.95, 0.3) node[above=0mm] {isomorphism};
+
+ %\rput(3.7,1.75){isomorphism}
+ \end{tikzpicture}
+
+ %%\begin{pspicture}(0.5,0.0)(8,2.5)
%%\showgrid
%\psframe[linewidth=0.4mm,framearc=0.2](5,0.0)(7.7,2.5)
%\pscircle[linewidth=0.3mm,dimen=middle](6,1.5){0.6}
@@ -255,9 +277,9 @@
inspired by earlier work of Pitts \cite{}. By means of automatic
proofs, we establish a reasoning infrastructure for alpha-equated
terms, including properties about support, freshness and equality
- conditions for alpha-equated terms. We will also derive for these
- terms a strong induction principle that has the variable convention
- already built in.
+ conditions for alpha-equated terms. We re also able to derive, at the moment
+ only manually, for these terms a strong induction principle that
+ has the variable convention already built in.
*}
section {* A Short Review of the Nominal Logic Work *}
--- a/Paper/document/root.bib Fri Mar 19 15:43:59 2010 +0100
+++ b/Paper/document/root.bib Fri Mar 19 17:20:25 2010 +0100
@@ -11,8 +11,7 @@
@InProceedings{Homeier05,
author = {P.~Homeier},
title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients},
- booktitle = {Proc.~of the 18th International Conference on Theorem
- Proving in Higher Order Logics (TPHOLs)},
+ booktitle = {Proc.~of the 18th TPHOLs Conference},
pages = {130--146},
year = {2005},
volume = {3603},
@@ -28,7 +27,7 @@
S.~Sarkar and
R.~Strni\v{s}a},
title = {{Ott}: {E}ffective {T}ool {S}upport for the {W}orking {S}emanticist},
- journal = {Journal of Functional Programming},
+ journal = {J.~of Functional Programming},
year = {2010},
volume = {20},
number = {1},
@@ -49,7 +48,7 @@
@Unpublished{HuffmanUrban10,
author = {B.~Huffman and C.~Urban},
title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
- note = {To appear at ITP 2010},
+ note = {To appear at {\it ITP'10 Conference}},
annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf},
year = {2010}
}
@@ -75,8 +74,7 @@
S.~Zdancewic},
title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark
{C}hallenge},
- booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order
- Logics (TPHOLs)},
+ booktitle = {Proc.~of the 18th TPHOLs Conference},
pages = {50--65},
year = {2005},
volume = {3603},
@@ -86,7 +84,7 @@
@Unpublished{SatoPollack10,
author = {M.~Sato and R.~Pollack},
title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus},
- note = {To appear in {\it Journal of Symbolic Computation}}
+ note = {To appear in {\it J.~of Symbolic Computation}}
}
@article{GabbayPitts02,
@@ -112,8 +110,7 @@
@InProceedings{BengtsonParrow07,
author = {J.~Bengtson and J.~Parrow},
title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic},
- booktitle = {Proc.~of the 10th International Conference on
- Foundations of Software Science and Computation Structures (FOSSACS)},
+ booktitle = {Proc.~of the 10th FOSSACS Conference},
year = 2007,
pages = {63--77},
series = {LNCS},
@@ -123,8 +120,7 @@
@inproceedings{BengtsonParow09,
author = {J.~Bengtson and J.~Parrow},
title = {{P}si-{C}alculi in {I}sabelle},
- booktitle = {Proc of the 22nd Conference on Theorem Proving in
- Higher Order Logics (TPHOLs)},
+ booktitle = {Proc of the 22nd TPHOLs Conference},
year = 2009,
pages = {99--114},
series = {LNCS},
@@ -133,8 +129,7 @@
@inproceedings{TobinHochstadtFelleisen08,
author = {S.~Tobin-Hochstadt and M.~Felleisen},
- booktitle = {Proc.~of the 35rd Symposium on
- Principles of Programming Languages (POPL)},
+ booktitle = {Proc.~of the 35rd POPL Symposium},
title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme},
publisher = {ACM},
year = {2008},
@@ -146,14 +141,13 @@
title = "{M}echanizing the {M}etatheory of {LF}",
pages = "45--56",
year = 2008,
- booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)"
+ booktitle = "Proc.~of the 23rd LICS Symposium"
}
@InProceedings{UrbanZhu08,
title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof",
author = "C.~Urban and B.~Zhu",
- booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques
- and Applications (RTA)",
+ booktitle = "Proc.~of the 9th RTA Conference",
year = "2008",
pages = "409--424",
series = "LNCS",