equal
deleted
inserted
replaced
78 through Proof", |
78 through Proof", |
79 publisher = AP, |
79 publisher = AP, |
80 series = "Computer Science and Applied Mathematics", |
80 series = "Computer Science and Applied Mathematics", |
81 year = 1986} |
81 year = 1986} |
82 |
82 |
|
83 @InProceedings{Aspinall:2000:eProof, |
|
84 author = {David Aspinall}, |
|
85 title = {Protocols for Interactive {e-Proof}}, |
|
86 booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)}, |
|
87 year = 2000, |
|
88 note = {Unpublished work-in-progress paper, |
|
89 \url{http://zermelo.dcs.ed.ac.uk/~da/drafts/eproof.ps.gz}} |
|
90 } |
83 @InProceedings{Aspinall:TACAS:2000, |
91 @InProceedings{Aspinall:TACAS:2000, |
84 author = {David Aspinall}, |
92 author = {David Aspinall}, |
85 title = {Proof General: A Generic Tool for Proof Development}, |
93 title = {Proof General: A Generic Tool for Proof Development}, |
86 booktitle = {ETAPS / TACAS}, |
94 booktitle = {ETAPS / TACAS}, |
87 year = 2000, |
95 year = 2000, |
112 @InProceedings{Bauer-Wenzel:2000:HB, |
120 @InProceedings{Bauer-Wenzel:2000:HB, |
113 author = {Gertrud Bauer and Markus Wenzel}, |
121 author = {Gertrud Bauer and Markus Wenzel}, |
114 title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in |
122 title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in |
115 {I}sabelle/{I}sar}, |
123 {I}sabelle/{I}sar}, |
116 booktitle = {Types for Proofs and Programs: TYPES'99}, |
124 booktitle = {Types for Proofs and Programs: TYPES'99}, |
|
125 editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m |
|
126 and Jan Smith}, |
117 series = {LNCS}, |
127 series = {LNCS}, |
118 year = 2000, |
128 year = 2000 |
119 note = {To appear} |
|
120 } |
129 } |
121 |
130 |
122 @InProceedings{Berghofer-Wenzel:1999:TPHOL, |
131 @InProceedings{Berghofer-Wenzel:1999:TPHOL, |
123 author = {Stefan Berghofer and Markus Wenzel}, |
132 author = {Stefan Berghofer and Markus Wenzel}, |
124 title = {Inductive datatypes in {HOL} --- lessons learned in |
133 title = {Inductive datatypes in {HOL} --- lessons learned in |
506 @article{MuellerNvOS99, |
515 @article{MuellerNvOS99, |
507 author= |
516 author= |
508 {Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, |
517 {Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch}, |
509 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999} |
518 title={{HOLCF = HOL + LCF}},journal=JFP,year=1999} |
510 |
519 |
|
520 @Manual{Muzalewski:Mizar, |
|
521 title = {An Outline of {PC} {Mizar}}, |
|
522 author = {Micha{\l} Muzalewski}, |
|
523 organization = {Fondation of Logic, Mathematics and Informatics |
|
524 --- Mizar Users Group}, |
|
525 year = 1993, |
|
526 note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}} |
|
527 } |
|
528 |
511 %N |
529 %N |
512 |
530 |
513 @InProceedings{NaraschewskiW-TPHOLs98, |
531 @InProceedings{NaraschewskiW-TPHOLs98, |
514 author = {Wolfgang Naraschewski and Markus Wenzel}, |
532 author = {Wolfgang Naraschewski and Markus Wenzel}, |
515 title = |
533 title = |
1002 year = 1962, |
1020 year = 1962, |
1003 publisher = CUP, |
1021 publisher = CUP, |
1004 note = {Paperback edition to *56, |
1022 note = {Paperback edition to *56, |
1005 abridged from the 2nd edition (1927)}} |
1023 abridged from the 2nd edition (1927)}} |
1006 |
1024 |
|
1025 @Misc{Wiedijk:1999:Mizar, |
|
1026 author = {Freek Wiedijk}, |
|
1027 title = {Mizar: An Impression}, |
|
1028 howpublished = {Unpublished paper}, |
|
1029 year = 1999, |
|
1030 note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}} |
|
1031 } |
|
1032 |
|
1033 @Misc{Wiedijk:2000:MV, |
|
1034 author = {Freek Wiedijk}, |
|
1035 title = {The Mathematical Vernacular}, |
|
1036 howpublished = {Unpublished paper}, |
|
1037 year = 2000, |
|
1038 note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}} |
|
1039 } |
|
1040 |
1007 @book{winskel93, |
1041 @book{winskel93, |
1008 author = {Glynn Winskel}, |
1042 author = {Glynn Winskel}, |
1009 title = {The Formal Semantics of Programming Languages}, |
1043 title = {The Formal Semantics of Programming Languages}, |
1010 publisher = MIT,year=1993} |
1044 publisher = MIT,year=1993} |
1011 |
1045 |