151 crossref = "tphols2000", |
151 crossref = "tphols2000", |
152 title = "Proof terms for simply typed higher order logic", |
152 title = "Proof terms for simply typed higher order logic", |
153 author = "Stefan Berghofer and Tobias Nipkow", |
153 author = "Stefan Berghofer and Tobias Nipkow", |
154 pages = "38--52"} |
154 pages = "38--52"} |
155 |
155 |
|
156 @InProceedings{Berghofer-Nipkow:2002, |
|
157 author = {Stefan Berghofer and Tobias Nipkow}, |
|
158 title = {Executing Higher Order Logic}, |
|
159 booktitle = {Types for Proofs and Programs: TYPES'2000}, |
|
160 editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack}, |
|
161 series = LNCS, |
|
162 publisher = Springer, |
|
163 note = {To appear}, |
|
164 year = 2002} |
|
165 |
156 @InProceedings{Berghofer-Wenzel:1999:TPHOL, |
166 @InProceedings{Berghofer-Wenzel:1999:TPHOL, |
157 author = {Stefan Berghofer and Markus Wenzel}, |
167 author = {Stefan Berghofer and Markus Wenzel}, |
158 title = {Inductive datatypes in {HOL} --- lessons learned in |
168 title = {Inductive datatypes in {HOL} --- lessons learned in |
159 {F}ormal-{L}ogic {E}ngineering}, |
169 {F}ormal-{L}ogic {E}ngineering}, |
160 crossref = {tphols99}} |
170 crossref = {tphols99}} |