# HG changeset patch # User Christian Urban # Date 1269015625 -3600 # Node ID d14b8b21bef2d9b09b13be4701b378a681ff4e8c # Parent 50838e25f73c1f0043148b55cf34dc4a0cdc4902 picture diff -r 50838e25f73c -r d14b8b21bef2 Paper/Paper.thy --- 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 *} diff -r 50838e25f73c -r d14b8b21bef2 Paper/document/root.bib --- 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",