1 |
1 |
2 @Unpublished{KaliszykUrban11, |
2 @inproceedings{KaliszykUrban11, |
3 author = {C.~Kaliszyk and C.~Urban}, |
3 author = {C.~Kaliszyk and C.~Urban}, |
4 title = {{Q}uotients {R}evisited for {I}sabelle/{HOL}}, |
4 title = {{Q}uotients {R}evisited for {I}sabelle/{HOL}}, |
5 note = {To appear in the Proc.~of the 26th ACM Symposium On Applied Computing}, |
5 booktitle = {Proc.~of the 26th ACM Symposium On Applied Computing (SAC)}, |
6 year = {2011} |
6 year = {2011}, |
|
7 pages = {1639--1644} |
7 } |
8 } |
8 |
9 |
9 @InProceedings{cheney05a, |
10 @InProceedings{cheney05a, |
10 author = {J.~Cheney}, |
11 author = {J.~Cheney}, |
11 title = {{S}crap your {N}ameplate ({F}unctional {P}earl)}, |
12 title = {{S}crap your {N}ameplate ({F}unctional {P}earl)}, |
12 booktitle = {Proc.~of the 10th ICFP Conference}, |
13 booktitle = {Proc.~of the 10th International Conference on Functional Programming (ICFP)}, |
13 pages = {180--191}, |
14 pages = {180--191}, |
14 year = {2005} |
15 year = {2005} |
15 } |
16 } |
16 |
17 |
17 @Inproceedings{Altenkirch10, |
18 @Inproceedings{Altenkirch10, |
18 author = {T.~Altenkirch and N.~A.~Danielsson and A.~L\"oh and N.~Oury}, |
19 author = {T.~Altenkirch and N.~A.~Danielsson and A.~L\"oh and N.~Oury}, |
19 title = {{PiSigma}: {D}ependent {T}ypes {W}ithout the {S}ugar}, |
20 title = {{PiSigma}: {D}ependent {T}ypes {W}ithout the {S}ugar}, |
20 booktitle = "Proc.~of the 10th FLOPS Conference", |
21 booktitle = "Proc.~of the 10th International Symposium on Functional and Logic Programming (FLOPS)", |
21 year = 2010, |
22 year = 2010, |
22 series = "LNCS", |
23 series = "LNCS", |
23 pages = "40--55", |
24 pages = "40--55", |
24 volume = 6009 |
25 volume = 6009 |
25 } |
26 } |
26 |
27 |
27 |
28 |
28 @InProceedings{ UrbanTasson05, |
29 @InProceedings{ UrbanTasson05, |
29 author = "C. Urban and C. Tasson", |
30 author = "C. Urban and C. Tasson", |
30 title = "{N}ominal {T}echniques in {I}sabelle/{HOL}", |
31 title = "{N}ominal {T}echniques in {I}sabelle/{HOL}", |
31 booktitle = "Proc.~of the 20th CADE Conference", |
32 booktitle = "Proc.~of the 20th Conference on Automated Deduction (CADE)", |
32 year = 2005, |
33 year = 2005, |
33 series = "LNCS", |
34 series = "LNCS", |
34 pages = "38--53", |
35 pages = "38--53", |
35 volume = 3632 |
36 volume = 3632 |
36 } |
37 } |
37 |
38 |
38 @InProceedings{ UrbanBerghofer06, |
39 @InProceedings{ UrbanBerghofer06, |
39 author = "C. Urban and S. Berghofer", |
40 author = "C. Urban and S. Berghofer", |
40 title = "{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes {I}mplemented in {I}sabelle/{HOL}", |
41 title = "{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes {I}mplemented in {I}sabelle/{HOL}", |
41 booktitle = "Proc.~of the 3rd IJCAR Conference", |
42 booktitle = "Proc.~of the 3rd International Joint Conference on Automated Deduction (IJCAR)", |
42 year = 2006, |
43 year = 2006, |
43 series = "LNAI", |
44 series = "LNAI", |
44 volume = 4130, |
45 volume = 4130, |
45 pages = "498--512" |
46 pages = "498--512" |
46 } |
47 } |
47 |
48 |
48 @InProceedings{LeeCraryHarper07, |
49 @InProceedings{LeeCraryHarper07, |
49 author = {D.~K.~Lee and K.~Crary and R.~Harper}, |
50 author = {D.~K.~Lee and K.~Crary and R.~Harper}, |
50 title = {{T}owards a {M}echanized {M}etatheory of {Standard ML}}, |
51 title = {{T}owards a {M}echanized {M}etatheory of {Standard ML}}, |
51 booktitle = {Proc.~of the 34th POPL Symposium}, |
52 booktitle = {Proc.~of the 34th Symposium on Principles of Programming Languages (POPL)}, |
52 year = 2007, |
53 year = 2007, |
53 pages = {173--184} |
54 pages = {173--184} |
54 } |
55 } |
55 |
56 |
56 @Unpublished{chargueraud09, |
57 @Unpublished{chargueraud09, |
57 author = "A.~Chargu{\'e}raud", |
58 author = "A.~Chargu{\'e}raud", |
58 title = "{T}he {L}ocally {N}ameless {R}epresentation", |
59 title = "{T}he {L}ocally {N}ameless {R}epresentation", |
59 Note = "To appear in J.~of Automated Reasoning." |
60 Note = "To appear in Journal of Automated Reasoning." |
60 } |
61 } |
61 |
62 |
62 @article{NaraschewskiNipkow99, |
63 @article{NaraschewskiNipkow99, |
63 author={W.~Naraschewski and T.~Nipkow}, |
64 author={W.~Naraschewski and T.~Nipkow}, |
64 title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}}, |
65 title={{T}ype {I}nference {V}erified: {A}lgorithm {W} in {Isabelle/HOL}}, |
65 journal={J.~of Automated Reasoning}, |
66 journal={Journal of Automated Reasoning}, |
66 year=1999, |
67 year=1999, |
67 volume=23, |
68 volume=23, |
68 pages={299--318}} |
69 pages={299--318}} |
69 |
70 |
70 @InProceedings{Berghofer99, |
71 @InProceedings{Berghofer99, |
71 author = {S.~Berghofer and M.~Wenzel}, |
72 author = {S.~Berghofer and M.~Wenzel}, |
72 title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in |
73 title = {{I}nductive {D}atatypes in {HOL} - {L}essons {L}earned in |
73 {F}ormal-{L}ogic {E}ngineering}, |
74 {F}ormal-{L}ogic {E}ngineering}, |
74 booktitle = {Proc.~of the 12th TPHOLs conference}, |
75 booktitle = {Proc.~of the 12th Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, |
75 pages = {19--36}, |
76 pages = {19--36}, |
76 year = 1999, |
77 year = 1999, |
77 volume = 1690, |
78 volume = 1690, |
78 series = {LNCS} |
79 series = {LNCS} |
79 } |
80 } |
80 |
81 |
81 @InProceedings{CoreHaskell, |
82 @InProceedings{CoreHaskell, |
82 author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly}, |
83 author = {M.~Sulzmann and M.~Chakravarty and S.~Peyton Jones and K.~Donnelly}, |
83 title = {{S}ystem {F} with {T}ype {E}quality {C}oercions}, |
84 title = {{S}ystem {F} with {T}ype {E}quality {C}oercions}, |
84 booktitle = {Proc.~of the TLDI Workshop}, |
85 booktitle = {Proc.~of the 3rd Workshop on Types in Language Design and Implementation (TLDI)}, |
85 pages = {53-66}, |
86 pages = {53-66}, |
86 year = {2007} |
87 year = {2007} |
87 } |
88 } |
88 |
89 |
89 @inproceedings{cheney05, |
90 @inproceedings{cheney05, |
90 author = {J.~Cheney}, |
91 author = {J.~Cheney}, |
91 title = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope}, |
92 title = {{T}oward a {G}eneral {T}heory of {N}ames: {B}inding and {S}cope}, |
92 booktitle = {Proc.~of the 3rd MERLIN workshop}, |
93 booktitle = {Proc.~of the 3rd ACM Workshop on Mechanized Reasoning about Languages |
|
94 with Variable Binding and Names (MERLIN)}, |
93 year = {2005}, |
95 year = {2005}, |
94 pages = {33-40} |
96 pages = {33-40} |
95 } |
97 } |
96 |
98 |
97 @Unpublished{Pitts04, |
99 @Unpublished{Pitts04, |
177 J.~N.~Foster and B.~C.~Pierce and P.~Sewell and |
179 J.~N.~Foster and B.~C.~Pierce and P.~Sewell and |
178 D.~Vytiniotis and G.~Washburn and S.~Weirich and |
180 D.~Vytiniotis and G.~Washburn and S.~Weirich and |
179 S.~Zdancewic}, |
181 S.~Zdancewic}, |
180 title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark |
182 title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark |
181 {C}hallenge}, |
183 {C}hallenge}, |
182 booktitle = {Proc.~of the 18th TPHOLs Conference}, |
184 booktitle = {Proc.~of the 18th Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, |
183 pages = {50--65}, |
185 pages = {50--65}, |
184 year = {2005}, |
186 year = {2005}, |
185 volume = {3603}, |
187 volume = {3603}, |
186 series = {LNCS} |
188 series = {LNCS} |
187 } |
189 } |
188 |
190 |
189 @article{MckinnaPollack99, |
191 @article{MckinnaPollack99, |
190 author = {J.~McKinna and R.~Pollack}, |
192 author = {J.~McKinna and R.~Pollack}, |
191 title = {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised}, |
193 title = {{S}ome {T}ype {T}heory and {L}ambda {C}alculus {F}ormalised}, |
192 journal = {J.~of Automated Reasoning}, |
194 journal = {Journal of Automated Reasoning}, |
193 volume = 23, |
195 volume = 23, |
194 number = {1-4}, |
196 number = {1-4}, |
195 year = 1999 |
197 year = 1999 |
196 } |
198 } |
197 |
199 |
198 @article{SatoPollack10, |
200 @article{SatoPollack10, |
199 author = {M.~Sato and R.~Pollack}, |
201 author = {M.~Sato and R.~Pollack}, |
200 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
202 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
201 journal = {J.~of Symbolic Computation}, |
203 journal = {Journal of Symbolic Computation}, |
202 volume = 45, |
204 volume = 45, |
203 pages = {598--616}, |
205 pages = {598--616}, |
204 year = 2010 |
206 year = 2010 |
205 } |
207 } |
206 |
208 |
225 } |
227 } |
226 |
228 |
227 @InProceedings{BengtsonParrow07, |
229 @InProceedings{BengtsonParrow07, |
228 author = {J.~Bengtson and J.~Parrow}, |
230 author = {J.~Bengtson and J.~Parrow}, |
229 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
231 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
230 booktitle = {Proc.~of the 10th FOSSACS Conference}, |
232 booktitle = {Proc.~of the 10th FOSSACS Conference ???}, |
231 year = 2007, |
233 year = 2007, |
232 pages = {63--77}, |
234 pages = {63--77}, |
233 series = {LNCS}, |
235 series = {LNCS}, |
234 volume = {4423} |
236 volume = {4423} |
235 } |
237 } |
236 |
238 |
237 @inproceedings{BengtsonParow09, |
239 @inproceedings{BengtsonParow09, |
238 author = {J.~Bengtson and J.~Parrow}, |
240 author = {J.~Bengtson and J.~Parrow}, |
239 title = {{P}si-{C}alculi in {I}sabelle}, |
241 title = {{P}si-{C}alculi in {I}sabelle}, |
240 booktitle = {Proc of the 22nd TPHOLs Conference}, |
242 booktitle = {Proc of the 22nd Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, |
241 year = 2009, |
243 year = 2009, |
242 pages = {99--114}, |
244 pages = {99--114}, |
243 series = {LNCS}, |
245 series = {LNCS}, |
244 volume = {5674} |
246 volume = {5674} |
245 } |
247 } |
246 |
248 |
247 @inproceedings{TobinHochstadtFelleisen08, |
249 @inproceedings{TobinHochstadtFelleisen08, |
248 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
250 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
249 booktitle = {Proc.~of the 35rd POPL Symposium}, |
251 booktitle = {Proc.~of the 35rd Symposium on Principles of Programming Languages (POPL)}, |
250 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
252 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
251 year = {2008}, |
253 year = {2008}, |
252 pages = {395--406} |
254 pages = {395--406} |
253 } |
255 } |
254 |
256 |
255 @InProceedings{UrbanCheneyBerghofer08, |
257 @InProceedings{UrbanCheneyBerghofer08, |
256 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
258 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
257 title = "{M}echanizing the {M}etatheory of {LF}", |
259 title = "{M}echanizing the {M}etatheory of {LF}", |
258 pages = "45--56", |
260 pages = "45--56", |
259 year = 2008, |
261 year = 2008, |
260 booktitle = "Proc.~of the 23rd LICS Symposium" |
262 booktitle = "Proc.~of the 23rd Symposium on Logic in Computer Science (LICS)" |
261 } |
263 } |
262 |
264 |
263 @InProceedings{UrbanZhu08, |
265 @InProceedings{UrbanZhu08, |
264 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
266 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
265 author = "C.~Urban and B.~Zhu", |
267 author = "C.~Urban and B.~Zhu", |
266 booktitle = "Proc.~of the 9th RTA Conference", |
268 booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques and Applications (RTA)", |
267 year = "2008", |
269 year = "2008", |
268 pages = "409--424", |
270 pages = "409--424", |
269 series = "LNCS", |
271 series = "LNCS", |
270 volume = 5117 |
272 volume = 5117 |
271 } |
273 } |