9 } |
9 } |
10 |
10 |
11 @InProceedings{Homeier05, |
11 @InProceedings{Homeier05, |
12 author = {P.~Homeier}, |
12 author = {P.~Homeier}, |
13 title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients}, |
13 title = {{A} {D}esign {S}tructure for {H}igher {O}rder {Q}uotients}, |
14 booktitle = {Proc.~of the 18th International Conference on Theorem |
14 booktitle = {Proc.~of the 18th TPHOLs Conference}, |
15 Proving in Higher Order Logics (TPHOLs)}, |
|
16 pages = {130--146}, |
15 pages = {130--146}, |
17 year = {2005}, |
16 year = {2005}, |
18 volume = {3603}, |
17 volume = {3603}, |
19 series = {LNCS} |
18 series = {LNCS} |
20 } |
19 } |
47 } |
46 } |
48 |
47 |
49 @Unpublished{HuffmanUrban10, |
48 @Unpublished{HuffmanUrban10, |
50 author = {B.~Huffman and C.~Urban}, |
49 author = {B.~Huffman and C.~Urban}, |
51 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
50 title = {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle}, |
52 note = {To appear at ITP 2010}, |
51 note = {To appear at {\it ITP'10 Conference}}, |
53 annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, |
52 annote = {http://www4.in.tum.de/\~{}urbanc/Publications/nominal-atoms.pdf}, |
54 year = {2010} |
53 year = {2010} |
55 } |
54 } |
56 |
55 |
57 @PhdThesis{Leroy92, |
56 @PhdThesis{Leroy92, |
73 J.~N.~Foster and B.~C.~Pierce and P.~Sewell and |
72 J.~N.~Foster and B.~C.~Pierce and P.~Sewell and |
74 D.~Vytiniotis and G.~Washburn and S.~Weirich and |
73 D.~Vytiniotis and G.~Washburn and S.~Weirich and |
75 S.~Zdancewic}, |
74 S.~Zdancewic}, |
76 title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark |
75 title = {{M}echanized {M}etatheory for the {M}asses: {T}he \mbox{Popl}{M}ark |
77 {C}hallenge}, |
76 {C}hallenge}, |
78 booktitle = {Proc.~of the 18th International Conference on Theorem Proving in Higher-Order |
77 booktitle = {Proc.~of the 18th TPHOLs Conference}, |
79 Logics (TPHOLs)}, |
|
80 pages = {50--65}, |
78 pages = {50--65}, |
81 year = {2005}, |
79 year = {2005}, |
82 volume = {3603}, |
80 volume = {3603}, |
83 series = {LNCS} |
81 series = {LNCS} |
84 } |
82 } |
85 |
83 |
86 @Unpublished{SatoPollack10, |
84 @Unpublished{SatoPollack10, |
87 author = {M.~Sato and R.~Pollack}, |
85 author = {M.~Sato and R.~Pollack}, |
88 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
86 title = {{E}xternal and {I}nternal {S}yntax of the {L}ambda-{C}alculus}, |
89 note = {To appear in {\it Journal of Symbolic Computation}} |
87 note = {To appear in {\it J.~of Symbolic Computation}} |
90 } |
88 } |
91 |
89 |
92 @article{GabbayPitts02, |
90 @article{GabbayPitts02, |
93 author = {M.~J.~Gabbay and A.~M.~Pitts}, |
91 author = {M.~J.~Gabbay and A.~M.~Pitts}, |
94 title = {A New Approach to Abstract Syntax with Variable |
92 title = {A New Approach to Abstract Syntax with Variable |
110 } |
108 } |
111 |
109 |
112 @InProceedings{BengtsonParrow07, |
110 @InProceedings{BengtsonParrow07, |
113 author = {J.~Bengtson and J.~Parrow}, |
111 author = {J.~Bengtson and J.~Parrow}, |
114 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
112 title = {Formalising the pi-{C}alculus using {N}ominal {L}ogic}, |
115 booktitle = {Proc.~of the 10th International Conference on |
113 booktitle = {Proc.~of the 10th FOSSACS Conference}, |
116 Foundations of Software Science and Computation Structures (FOSSACS)}, |
|
117 year = 2007, |
114 year = 2007, |
118 pages = {63--77}, |
115 pages = {63--77}, |
119 series = {LNCS}, |
116 series = {LNCS}, |
120 volume = {4423} |
117 volume = {4423} |
121 } |
118 } |
122 |
119 |
123 @inproceedings{BengtsonParow09, |
120 @inproceedings{BengtsonParow09, |
124 author = {J.~Bengtson and J.~Parrow}, |
121 author = {J.~Bengtson and J.~Parrow}, |
125 title = {{P}si-{C}alculi in {I}sabelle}, |
122 title = {{P}si-{C}alculi in {I}sabelle}, |
126 booktitle = {Proc of the 22nd Conference on Theorem Proving in |
123 booktitle = {Proc of the 22nd TPHOLs Conference}, |
127 Higher Order Logics (TPHOLs)}, |
|
128 year = 2009, |
124 year = 2009, |
129 pages = {99--114}, |
125 pages = {99--114}, |
130 series = {LNCS}, |
126 series = {LNCS}, |
131 volume = {5674} |
127 volume = {5674} |
132 } |
128 } |
133 |
129 |
134 @inproceedings{TobinHochstadtFelleisen08, |
130 @inproceedings{TobinHochstadtFelleisen08, |
135 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
131 author = {S.~Tobin-Hochstadt and M.~Felleisen}, |
136 booktitle = {Proc.~of the 35rd Symposium on |
132 booktitle = {Proc.~of the 35rd POPL Symposium}, |
137 Principles of Programming Languages (POPL)}, |
|
138 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
133 title = {{T}he {D}esign and {I}mplementation of {T}yped {S}cheme}, |
139 publisher = {ACM}, |
134 publisher = {ACM}, |
140 year = {2008}, |
135 year = {2008}, |
141 pages = {395--406} |
136 pages = {395--406} |
142 } |
137 } |
144 @InProceedings{UrbanCheneyBerghofer08, |
139 @InProceedings{UrbanCheneyBerghofer08, |
145 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
140 author = "C.~Urban and J.~Cheney and S.~Berghofer", |
146 title = "{M}echanizing the {M}etatheory of {LF}", |
141 title = "{M}echanizing the {M}etatheory of {LF}", |
147 pages = "45--56", |
142 pages = "45--56", |
148 year = 2008, |
143 year = 2008, |
149 booktitle = "Proc.~of the 23rd IEEE Symposium on Logic in Computer Science (LICS)" |
144 booktitle = "Proc.~of the 23rd LICS Symposium" |
150 } |
145 } |
151 |
146 |
152 @InProceedings{UrbanZhu08, |
147 @InProceedings{UrbanZhu08, |
153 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
148 title = "{R}evisiting {C}ut-{E}limination: {O}ne {D}ifficult {P}roof is {R}eally a {P}roof", |
154 author = "C.~Urban and B.~Zhu", |
149 author = "C.~Urban and B.~Zhu", |
155 booktitle = "Proc.~of the 9th International Conference on Rewriting Techniques |
150 booktitle = "Proc.~of the 9th RTA Conference", |
156 and Applications (RTA)", |
|
157 year = "2008", |
151 year = "2008", |
158 pages = "409--424", |
152 pages = "409--424", |
159 series = "LNCS", |
153 series = "LNCS", |
160 volume = 5117 |
154 volume = 5117 |
161 } |
155 } |