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