--- a/ProgTutorial/document/root.bib Wed Aug 19 09:25:49 2009 +0200
+++ b/ProgTutorial/document/root.bib Thu Aug 20 10:38:26 2009 +0200
@@ -10,36 +10,6 @@
Computing Science, Middlesex University}
}
-@inproceedings{Krauss-IJCAR06,
- author = {A.~Krauss},
- title = {{P}artial {R}ecursive {F}unctions in {H}igher-{O}rder {L}ogic},
- editor = {Ulrich Furbach and Natarajan Shankar},
- booktitle = {Automated Reasoning, Third International Joint
- Conference, IJCAR 2006, Seattle, WA, USA, August
- 17-20, 2006, Proceedings},
- publisher = {Springer-Verlag},
- series = {Lecture Notes in Computer Science},
- volume = {4130},
- year = {2006},
- pages = {589-603}
-}
-
-@INPROCEEDINGS{Melham:1992:PIR,
- AUTHOR = {T.~F.~Melham},
- TITLE = {{A} {P}ackage for {I}nductive {R}elation {D}efinitions in
- {HOL}},
- BOOKTITLE = {Proceedings of the 1991 International Workshop on
- the {HOL} Theorem Proving System and its
- Applications, {D}avis, {C}alifornia, {A}ugust
- 28--30, 1991},
- EDITOR = {Myla Archer and Jeffrey J. Joyce and Karl N. Levitt
- and Phillip J. Windley},
- PUBLISHER = {IEEE Computer Society Press},
- YEAR = {1992},
- PAGES = {350--357},
- ISBN = {0-8186-2460-4},
-}
-
@Book{isa-tutorial,
author = {T.~Nipkow and L.~C.~Paulson and M.~Wenzel},
title = {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
@@ -54,73 +24,6 @@
edition = {2nd},
publisher = {Cambridge University Press}}
-@InCollection{Paulson-ind-defs,
- author = {L.~C.~Paulson},
- title = {A fixedpoint approach to (co)inductive and
- (co)datatype definitions},
- booktitle = {Proof, Language, and Interaction: Essays in Honour
- of Robin Milner},
- pages = {187--211},
- publisher = {MIT Press},
- year = 2000,
- editor = {G. Plotkin and C. Stirling and M. Tofte}
-}
-
-@inproceedings{Schirmer-LPAR04,
- author = {N.~Schirmer},
- title = {{A} {V}erification {E}nvironment for {S}equential {I}mperative
- Programs in {I}sabelle/{HOL}},
- booktitle = "Logic for Programming, Artificial Intelligence, and
- Reasoning",
- editor = "F. Baader and A. Voronkov",
- year = 2005,
- publisher = "Springer-Verlag",
- series = "Lecture Notes in Artificial Intelligence",
- volume = 3452,
- pages = {398--414}
-}
-
-@TechReport{Schwichtenberg-MLCF,
- author = {H.~Schwichtenberg},
- title = {{M}inimal {L}ogic {f}or {C}omputable {F}unctionals},
- institution = {Mathematisches Institut,
- Ludwig-Maximilians-Universit{\"a}t M{\"u}nchen},
- year = 2005,
- month = {December},
- note = {Available online at
- \url{http://www.mathematik.uni-muenchen.de/~minlog/minlog/mlcf.pdf}}
-}
-
-@inproceedings{Urban-Berghofer06,
- author = {C.~Urban and S.~Berghofer},
- title = {{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes
- {I}mplemented in {I}sabelle/{HOL}},
- editor = {Ulrich Furbach and Natarajan Shankar},
- booktitle = {Automated Reasoning, Third International Joint
- Conference, IJCAR 2006, Seattle, WA, USA, August
- 17-20, 2006, Proceedings},
- publisher = {Springer-Verlag},
- series = {Lecture Notes in Computer Science},
- volume = {4130},
- year = {2006},
- pages = {498-512}
-}
-
-@inproceedings{Wadler-AFP95,
- author = {P.~Wadler},
- title = {Monads for Functional Programming},
- pages = {24-52},
- editor = {Johan Jeuring and Erik Meijer},
- booktitle = {Advanced Functional Programming, First International
- Spring School on Advanced Functional Programming
- Techniques, B{\aa}stad, Sweden, May 24-30, 1995,
- Tutorial Text},
- publisher = {Springer-Verlag},
- series = {Lecture Notes in Computer Science},
- volume = {925},
- year = {1995}
-}
-
@manual{isa-imp,
author = {M.~Wenzel},
title = {The {Isabelle/Isar} Implementation},
@@ -145,3 +48,13 @@
pages = {465--483}
}
+@Article{ Dyckhoff92,
+ title = "{Contraction-Free Sequent Calculi for Intuitionistic Logic}",
+ author = "R. Dyckhoff",
+ journal = "The Journal of Symbolic Logic",
+ volume = "57",
+ number = "3",
+ pages = "795--807",
+ year = "1992",
+ publisher = "JSTOR"
+}
\ No newline at end of file