1 @Misc{Bornat-lecture, |
1 @Misc{Bornat-lecture, |
2 author = {Richard Bornat}, |
2 author = {R.~Bornat}, |
3 title = {In defence of programming}, |
3 title = {In {D}efence of {P}rogramming}, |
4 howpublished = {Available online via |
4 howpublished = {Available online via |
5 \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}}, |
5 \url{http://www.cs.mdx.ac.uk/staffpages/r_bornat/lectures/ revisedinauguraltext.pdf}}, |
6 month = {April}, |
6 month = {April}, |
7 year = 2005, |
7 year = 2005, |
8 note = {Corrected and revised version of inaugural lecture, |
8 note = {Corrected and revised version of inaugural lecture, |
9 delivered on 22nd January 2004 at the School of |
9 delivered on 22nd January 2004 at the School of |
10 Computing Science, Middlesex University} |
10 Computing Science, Middlesex University} |
11 } |
11 } |
12 |
12 |
13 @inproceedings{Krauss-IJCAR06, |
13 @inproceedings{Krauss-IJCAR06, |
14 author = {Alexander Krauss}, |
14 author = {A.~Krauss}, |
15 title = {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic}, |
15 title = {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic}, |
16 editor = {Ulrich Furbach and Natarajan Shankar}, |
16 editor = {Ulrich Furbach and Natarajan Shankar}, |
17 booktitle = {Automated Reasoning, Third International Joint |
17 booktitle = {Automated Reasoning, Third International Joint |
18 Conference, IJCAR 2006, Seattle, WA, USA, August |
18 Conference, IJCAR 2006, Seattle, WA, USA, August |
19 17-20, 2006, Proceedings}, |
19 17-20, 2006, Proceedings}, |
23 year = {2006}, |
23 year = {2006}, |
24 pages = {589-603} |
24 pages = {589-603} |
25 } |
25 } |
26 |
26 |
27 @INPROCEEDINGS{Melham:1992:PIR, |
27 @INPROCEEDINGS{Melham:1992:PIR, |
28 AUTHOR = {T. F. Melham}, |
28 AUTHOR = {T.~F.~Melham}, |
29 TITLE = {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in |
29 TITLE = {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in |
30 {HOL}}, |
30 {HOL}}, |
31 BOOKTITLE = {Proceedings of the 1991 International Workshop on |
31 BOOKTITLE = {Proceedings of the 1991 International Workshop on |
32 the {HOL} Theorem Proving System and its |
32 the {HOL} Theorem Proving System and its |
33 Applications, {D}avis, {C}alifornia, {A}ugust |
33 Applications, {D}avis, {C}alifornia, {A}ugust |
39 PAGES = {350--357}, |
39 PAGES = {350--357}, |
40 ISBN = {0-8186-2460-4}, |
40 ISBN = {0-8186-2460-4}, |
41 } |
41 } |
42 |
42 |
43 @Book{isa-tutorial, |
43 @Book{isa-tutorial, |
44 author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, |
44 author = {T.~Nipkow and L.~C.~Paulson and M.~Wenzel}, |
45 title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic}, |
45 title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic}, |
46 publisher = {Springer}, |
46 publisher = {Springer}, |
47 year = 2002, |
47 year = 2002, |
48 note = {LNCS Tutorial 2283}} |
48 note = {LNCS Tutorial 2283}} |
49 |
49 |
53 year = 1996, |
53 year = 1996, |
54 edition = {2nd}, |
54 edition = {2nd}, |
55 publisher = {Cambridge University Press}} |
55 publisher = {Cambridge University Press}} |
56 |
56 |
57 @InCollection{Paulson-ind-defs, |
57 @InCollection{Paulson-ind-defs, |
58 author = {L. C. Paulson}, |
58 author = {L.~C.~Paulson}, |
59 title = {A fixedpoint approach to (co)inductive and |
59 title = {A fixedpoint approach to (co)inductive and |
60 (co)datatype definitions}, |
60 (co)datatype definitions}, |
61 booktitle = {Proof, Language, and Interaction: Essays in Honour |
61 booktitle = {Proof, Language, and Interaction: Essays in Honour |
62 of Robin Milner}, |
62 of Robin Milner}, |
63 pages = {187--211}, |
63 pages = {187--211}, |
65 year = 2000, |
65 year = 2000, |
66 editor = {G. Plotkin and C. Stirling and M. Tofte} |
66 editor = {G. Plotkin and C. Stirling and M. Tofte} |
67 } |
67 } |
68 |
68 |
69 @inproceedings{Schirmer-LPAR04, |
69 @inproceedings{Schirmer-LPAR04, |
70 author = {Norbert Schirmer}, |
70 author = {N.~Schirmer}, |
71 title = {{A} {V}erification {E}nvironment for {S}equential {I}mperative |
71 title = {{A} {V}erification {E}nvironment for {S}equential {I}mperative |
72 Programs in {I}sabelle/{HOL}}, |
72 Programs in {I}sabelle/{HOL}}, |
73 booktitle = "Logic for Programming, Artificial Intelligence, and |
73 booktitle = "Logic for Programming, Artificial Intelligence, and |
74 Reasoning", |
74 Reasoning", |
75 editor = "F. Baader and A. Voronkov", |
75 editor = "F. Baader and A. Voronkov", |
79 volume = 3452, |
79 volume = 3452, |
80 pages = {398--414} |
80 pages = {398--414} |
81 } |
81 } |
82 |
82 |
83 @TechReport{Schwichtenberg-MLCF, |
83 @TechReport{Schwichtenberg-MLCF, |
84 author = {Helmut Schwichtenberg}, |
84 author = {H.~Schwichtenberg}, |
85 title = {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals}, |
85 title = {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals}, |
86 institution = {Mathematisches Institut, |
86 institution = {Mathematisches Institut, |
87 Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen}, |
87 Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen}, |
88 year = 2005, |
88 year = 2005, |
89 month = {December}, |
89 month = {December}, |
90 note = {Available online at |
90 note = {Available online at |
91 \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}} |
91 \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}} |
92 } |
92 } |
93 |
93 |
94 @inproceedings{Urban-Berghofer06, |
94 @inproceedings{Urban-Berghofer06, |
95 author = {Christian Urban and Stefan Berghofer}, |
95 author = {C.~Urban and S.~Berghofer}, |
96 title = {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes |
96 title = {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes |
97 {I}mplemented in {I}sabelle/{HOL}}, |
97 {I}mplemented in {I}sabelle/{HOL}}, |
98 editor = {Ulrich Furbach and Natarajan Shankar}, |
98 editor = {Ulrich Furbach and Natarajan Shankar}, |
99 booktitle = {Automated Reasoning, Third International Joint |
99 booktitle = {Automated Reasoning, Third International Joint |
100 Conference, IJCAR 2006, Seattle, WA, USA, August |
100 Conference, IJCAR 2006, Seattle, WA, USA, August |
105 year = {2006}, |
105 year = {2006}, |
106 pages = {498-512} |
106 pages = {498-512} |
107 } |
107 } |
108 |
108 |
109 @inproceedings{Wadler-AFP95, |
109 @inproceedings{Wadler-AFP95, |
110 author = {Philip Wadler}, |
110 author = {P.~Wadler}, |
111 title = {Monads for Functional Programming}, |
111 title = {Monads for Functional Programming}, |
112 pages = {24-52}, |
112 pages = {24-52}, |
113 editor = {Johan Jeuring and Erik Meijer}, |
113 editor = {Johan Jeuring and Erik Meijer}, |
114 booktitle = {Advanced Functional Programming, First International |
114 booktitle = {Advanced Functional Programming, First International |
115 Spring School on Advanced Functional Programming |
115 Spring School on Advanced Functional Programming |
120 volume = {925}, |
120 volume = {925}, |
121 year = {1995} |
121 year = {1995} |
122 } |
122 } |
123 |
123 |
124 @manual{isa-imp, |
124 @manual{isa-imp, |
125 author = {Makarius Wenzel}, |
125 author = {M.~Wenzel}, |
126 title = {The {Isabelle/Isar} Implementation}, |
126 title = {The {Isabelle/Isar} Implementation}, |
127 institution = {Technische Universit\"at M\"unchen}, |
127 institution = {Technische Universit\"at M\"unchen}, |
128 note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}} |
128 note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}} |
|
129 |
|
130 |
|
131 @book{GordonMilnerWadsworth79, |
|
132 author = {M.~Gordon and R.~Milner and C.~P.~Wadsworth}, |
|
133 title = {{E}dinburgh {LCF}}, |
|
134 publisher = {Springer}, |
|
135 series = {Lecture Notes in Computer Science}, |
|
136 volume = {78}, |
|
137 year = {1979} |
|
138 } |