30
|
1 |
@Misc{Bornat-lecture,
|
124
|
2 |
author = {R.~Bornat},
|
|
3 |
title = {In {D}efence of {P}rogramming},
|
30
|
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 |
}
|
2
|
12 |
|
30
|
13 |
@inproceedings{Krauss-IJCAR06,
|
124
|
14 |
author = {A.~Krauss},
|
30
|
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 |
}
|
5
|
26 |
|
30
|
27 |
@INPROCEEDINGS{Melham:1992:PIR,
|
124
|
28 |
AUTHOR = {T.~F.~Melham},
|
30
|
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 |
}
|
5
|
42 |
|
|
43 |
@Book{isa-tutorial,
|
124
|
44 |
author = {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},
|
5
|
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},
|
30
|
55 |
publisher = {Cambridge University Press}}
|
|
56 |
|
|
57 |
@InCollection{Paulson-ind-defs,
|
124
|
58 |
author = {L.~C.~Paulson},
|
30
|
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,
|
124
|
70 |
author = {N.~Schirmer},
|
30
|
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,
|
124
|
84 |
author = {H.~Schwichtenberg},
|
30
|
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,
|
124
|
95 |
author = {C.~Urban and S.~Berghofer},
|
30
|
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,
|
124
|
110 |
author = {P.~Wadler},
|
30
|
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,
|
124
|
125 |
author = {M.~Wenzel},
|
30
|
126 |
title = {The {Isabelle/Isar} Implementation},
|
|
127 |
institution = {Technische Universit\"at M\"unchen},
|
|
128 |
note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
|
124
|
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 |
} |