|
1 @Unpublished{HuffmanUrban10, |
|
2 author = {B.~Huffman and C.~Urban}, |
|
3 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
|
4 note = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, |
|
5 year = {2010} |
|
6 } |
|
7 |
|
8 @Unpublished{SatoPollack10, |
|
9 author = {M.~Sato and R.~Pollack}, |
|
10 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
|
11 note = {To appear in {\it Journal of Symbolic Computation}} |
|
12 } |
|
13 |
|
14 @article{GabbayPitts02, |
|
15 author = {M.~J.~Gabbay and A.~M.~Pitts}, |
|
16 title = {A New Approach to Abstract Syntax with Variable |
|
17 Binding}, |
|
18 journal = {Formal Aspects of Computing}, |
|
19 volume = {13}, |
|
20 year = 2002, |
|
21 pages = {341--363} |
|
22 } |
|
23 |
|
24 @article{Pitts03, |
|
25 author = {A.~M.~Pitts}, |
|
26 title = {Nominal Logic, A First Order Theory of Names and |
|
27 Binding}, |
|
28 journal = {Information and Computation}, |
|
29 year = {2003}, |
|
30 volume = {183}, |
|
31 pages = {165--193} |
|
32 } |
|
33 |
|
34 @InProceedings{BengtsonParrow07, |
|
35 author = {J.~Bengtson and J.~Parrow}, |
|
36 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
|
37 booktitle = {Proc.~of the 10th International Conference on |
|
38 Foundations of Software Science and Computation Structures (FOSSACS)}, |
|
39 year = 2007, |
|
40 pages = {63--77}, |
|
41 series = {LNCS}, |
|
42 volume = {4423} |
|
43 } |
|
44 |
|
45 @inproceedings{BengtsonParow09, |
|
46 author = {J.~Bengtson and J.~Parrow}, |
|
47 title = {{P}si-{C}alculi in {I}sabelle}, |
|
48 booktitle = {Proc of the 22nd Conference on Theorem Proving in |
|
49 Higher Order Logics (TPHOLs)}, |
|
50 year = 2009, |
|
51 pages = {99--114}, |
|
52 series = {LNCS}, |
|
53 volume = {5674} |
|
54 } |
|
55 |
|
56 @inproceedings{TobinHochstadtFelleisen08, |
|
57 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
|
58 booktitle = {Proc.~of the 35rd Symposium on |
|
59 Principles of Programming Languages (POPL)}, |
|
60 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
|
61 publisher = {ACM}, |
|
62 year = {2008}, |
|
63 pages = {395--406} |
|
64 } |
|
65 |
|
66 @InProceedings{UrbanCheneyBerghofer08, |
|
67 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
|
68 title = "{M}echanizing the {M}etatheory of {LF}", |
|
69 pages = "45--56", |
|
70 year = 2008, |
|
71 booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)" |
|
72 } |
|
73 |
|
74 @InProceedings{UrbanZhu08, |
|
75 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
|
76 author = "C.~Urban and B.~Zhu", |
|
77 booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques |
|
78 and Applications (RTA)", |
|
79 year = "2008", |
|
80 pages = "409--424", |
|
81 series = "LNCS", |
|
82 volume = 5117 |
|
83 } |
|
84 |
|
85 @Article{UrbanPittsGabbay04, |
|
86 title = "{N}ominal {U}nification", |
|
87 author = "C.~Urban and A.M.~Pitts and M.J.~Gabbay", |
|
88 journal = "Theoretical Computer Science", |
|
89 pages = "473--497", |
|
90 volume = "323", |
|
91 number = "1-3", |
|
92 year = "2004" |
|
93 } |
|
94 |
|
95 @Article{Church40, |
|
96 author = {A.~Church}, |
|
97 title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes}, |
|
98 journal = {Journal of Symbolic Logic}, |
|
99 year = {1940}, |
|
100 volume = {5}, |
|
101 number = {2}, |
|
102 pages = {56--68} |
|
103 } |
|
104 |
|
105 |
|
106 @Manual{PittsHOL4, |
|
107 title = {{S}yntax and {S}emantics}, |
|
108 author = {A.~M.~Pitts}, |
|
109 note = {Part of the documentation for the HOL4 system.} |
|
110 } |
|
111 |
|
112 |
|
113 @book{PaulsonBenzmueller, |
|
114 year={2009}, |
|
115 author={Benzm{\"u}ller, Christoph and Paulson, Lawrence C.}, |
|
116 title={Quantified Multimodal Logics in Simple Type Theory}, |
|
117 note={{http://arxiv.org/abs/0905.2435}}, |
|
118 series={{SEKI Report SR--2009--02 (ISSN 1437-4447)}}, |
|
119 publisher={{SEKI Publications}} |
|
120 } |
|
121 |
|
122 @Article{Cheney06, |
|
123 author = {J.~Cheney}, |
|
124 title = {{C}ompleteness and {H}erbrand theorems for {N}ominal {L}ogic}, |
|
125 journal = {Journal of Symbolic Logic}, |
|
126 year = {2006}, |
|
127 volume = {71}, |
|
128 number = {1}, |
|
129 pages = {299--320} |
|
130 } |
|
131 |