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