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