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