Rewrite the Probability theory.
Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
% BibTeX database for the Isabelle documentation
%publishers
@string{AP="Academic Press"}
@string{CUP="Cambridge University Press"}
@string{IEEE="IEEE Computer Society Press"}
@string{LNCS="Lecture Notes in Computer Science"}
@string{MIT="MIT Press"}
@string{NH="North-Holland"}
@string{Prentice="Prentice-Hall"}
@string{PH="Prentice-Hall"}
@string{Springer="Springer-Verlag"}
%institutions
@string{CUCL="Computer Laboratory, University of Cambridge"}
@string{Edinburgh="Department of Computer Science, University of Edinburgh"}
@string{TUM="Department of Informatics, Technical University of Munich"}
%journals
@string{AI="Artificial Intelligence"}
@string{FAC="Formal Aspects of Computing"}
@string{JAR="Journal of Automated Reasoning"}
@string{JCS="Journal of Computer Security"}
@string{JFP="Journal of Functional Programming"}
@string{JLC="Journal of Logic and Computation"}
@string{JLP="Journal of Logic Programming"}
@string{JSC="Journal of Symbolic Computation"}
@string{JSL="Journal of Symbolic Logic"}
@string{PROYAL="Proceedings of the Royal Society of London"}
@string{SIGPLAN="{SIGPLAN} Notices"}
@string{TISSEC="ACM Transactions on Information and System Security"}
%conferences
@string{CADE="International Conference on Automated Deduction"}
@string{POPL="Symposium on Principles of Programming Languages"}
@string{TYPES="Types for Proofs and Programs"}
%A
@incollection{abramsky90,
author = {Samson Abramsky},
title = {The Lazy Lambda Calculus},
pages = {65-116},
editor = {David A. Turner},
booktitle = {Research Topics in Functional Programming},
publisher = {Addison-Wesley},
year = 1990}
@Unpublished{abrial93,
author = {J. R. Abrial and G. Laffitte},
title = {Towards the Mechanization of the Proofs of Some Classical
Theorems of Set Theory},
note = {preprint},
year = 1993,
month = Feb}
@incollection{aczel77,
author = {Peter Aczel},
title = {An Introduction to Inductive Definitions},
pages = {739-782},
crossref = {barwise-handbk}}
@Book{aczel88,
author = {Peter Aczel},
title = {Non-Well-Founded Sets},
publisher = {CSLI},
year = 1988}
@InProceedings{alf,
author = {Lena Magnusson and Bengt {Nordstr\"{o}m}},
title = {The {ALF} Proof Editor and Its Proof Engine},
crossref = {types93},
pages = {213-237}}
@inproceedings{andersson-1993,
author = "Arne Andersson",
title = "Balanced Search Trees Made Simple",
editor = "F. K. H. A. Dehne and N. Santoro and S. Whitesides",
booktitle = "WADS 1993",
series = LNCS,
volume = {709},
pages = "61--70",
year = 1993,
publisher = Springer}
@book{andrews86,
author = "Peter Andrews",
title = "An Introduction to Mathematical Logic and Type Theory: to Truth
through Proof",
publisher = AP,
series = "Computer Science and Applied Mathematics",
year = 1986}
@InProceedings{Aspinall:2000:eProof,
author = {David Aspinall},
title = {Protocols for Interactive {e-Proof}},
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs)},
year = 2000,
note = {Unpublished work-in-progress paper,
\url{http://homepages.inf.ed.ac.uk/da/papers/drafts/eproof.ps.gz}}
}
@InProceedings{Aspinall:TACAS:2000,
author = {David Aspinall},
title = {{P}roof {G}eneral: A Generic Tool for Proof Development},
booktitle = {Tools and Algorithms for the Construction and Analysis of
Systems (TACAS)},
year = 2000,
publisher = Springer,
series = LNCS,
volume = 1785,
pages = "38--42"
}
@Misc{isamode,
author = {David Aspinall},
title = {Isamode --- {U}sing {I}sabelle with {E}macs},
note = {\url{http://homepages.inf.ed.ac.uk/da/Isamode/}}
}
@Misc{proofgeneral,
author = {David Aspinall},
title = {{P}roof {G}eneral},
note = {\url{http://proofgeneral.inf.ed.ac.uk/}}
}
%B
@book{Baader-Nipkow,author={Franz Baader and Tobias Nipkow},
title="Term Rewriting and All That",publisher=CUP,year=1998}
@manual{isabelle-locale,
author = {Clemens Ballarin},
title = {Tutorial to Locales and Locale Interpretation},
institution = TUM,
note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
}
@InCollection{Barendregt-Geuvers:2001,
author = {H. Barendregt and H. Geuvers},
title = {Proof Assistants using Dependent Type Systems},
booktitle = {Handbook of Automated Reasoning},
publisher = {Elsevier},
year = 2001,
editor = {A. Robinson and A. Voronkov}
}
@incollection{basin91,
author = {David Basin and Matt Kaufmann},
title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental
Comparison},
crossref = {huet-plotkin91},
pages = {89-119}}
@Unpublished{HOL-Library,
author = {Gertrud Bauer and Tobias Nipkow and Oheimb, David von and
Lawrence C Paulson and Thomas M Rasmussen and Christophe Tabacznyj and
Markus Wenzel},
title = {The Supplemental {Isabelle/HOL} Library},
note = {Part of the Isabelle distribution,
\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}},
year = 2002
}
@InProceedings{Bauer-Wenzel:2000:HB,
author = {Gertrud Bauer and Markus Wenzel},
title = {Computer-Assisted Mathematics at Work --- The {H}ahn-{B}anach Theorem in
{I}sabelle/{I}sar},
booktitle = {Types for Proofs and Programs: TYPES'99},
editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m
and Jan Smith},
series = {LNCS},
year = 2000
}
@InProceedings{Bauer-Wenzel:2001,
author = {Gertrud Bauer and Markus Wenzel},
title = {Calculational reasoning revisited --- an {Isabelle/Isar} experience},
crossref = {tphols2001}}
@inProceedings{Berghofer-Bulwahn-Haftmann:2009:TPHOL,
author = {Berghofer, Stefan and Bulwahn, Lukas and Haftmann, Florian},
booktitle = {Theorem Proving in Higher Order Logics},
pages = {131--146},
title = {Turning Inductive into Equational Specifications},
year = {2009}
}
@INPROCEEDINGS{Berghofer-Nipkow:2000:TPHOL,
crossref = "tphols2000",
title = "Proof terms for simply typed higher order logic",
author = "Stefan Berghofer and Tobias Nipkow",
pages = "38--52"}
@inproceedings{berghofer-nipkow-2004,
author = {Stefan Berghofer and Tobias Nipkow},
title = {Random Testing in {I}sabelle/{HOL}},
pages = {230--239},
editor = "J. Cuellar and Z. Liu",
booktitle = {{SEFM} 2004},
publisher = IEEE,
year = 2004}
@InProceedings{Berghofer-Nipkow:2002,
author = {Stefan Berghofer and Tobias Nipkow},
title = {Executing Higher Order Logic},
booktitle = {Types for Proofs and Programs: TYPES'2000},
editor = {P. Callaghan and Z. Luo and J. McKinna and R. Pollack},
series = LNCS,
publisher = Springer,
volume = 2277,
year = 2002}
@InProceedings{Berghofer-Wenzel:1999:TPHOL,
author = {Stefan Berghofer and Markus Wenzel},
title = {Inductive datatypes in {HOL} --- lessons learned in
{F}ormal-{L}ogic {E}ngineering},
crossref = {tphols99}}
@InProceedings{Bezem-Coquand:2005,
author = {M.A. Bezem and T. Coquand},
title = {Automating {Coherent Logic}},
booktitle = {LPAR-12},
editor = {G. Sutcliffe and A. Voronkov},
volume = 3835,
series = LNCS,
publisher = Springer}
@book{Bird-Wadler,author="Richard Bird and Philip Wadler",
title="Introduction to Functional Programming",publisher=PH,year=1988}
@book{Bird-Haskell,author="Richard Bird",
title="Introduction to Functional Programming using Haskell",
publisher=PH,year=1998}
@inproceedings{blanchette-nipkow-2010,
title = "Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder",
author = "Jasmin Christian Blanchette and Tobias Nipkow",
crossref = {itp2010}}
@inproceedings{boehme-nipkow-2010,
author={Sascha B\"ohme and Tobias Nipkow},
title={Sledgehammer: Judgement Day},
booktitle={Automated Reasoning: IJCAR 2010},
editor={J. Giesl and R. H\"ahnle},
publisher=Springer,
series=LNCS,
year=2010}
@Article{boyer86,
author = {Robert Boyer and Ewing Lusk and William McCune and Ross
Overbeek and Mark Stickel and Lawrence Wos},
title = {Set Theory in First-Order Logic: Clauses for {G\"{o}del's}
Axioms},
journal = JAR,
year = 1986,
volume = 2,
number = 3,
pages = {287-327}}
@book{bm79,
author = {Robert S. Boyer and J Strother Moore},
title = {A Computational Logic},
publisher = {Academic Press},
year = 1979}
@book{bm88book,
author = {Robert S. Boyer and J Strother Moore},
title = {A Computational Logic Handbook},
publisher = {Academic Press},
year = 1988}
@Article{debruijn72,
author = {N. G. de Bruijn},
title = {Lambda Calculus Notation with Nameless Dummies,
a Tool for Automatic Formula Manipulation,
with Application to the {Church-Rosser Theorem}},
journal = {Indag. Math.},
volume = 34,
pages = {381-392},
year = 1972}
@InProceedings{bulwahnKN07,
author = {Lukas Bulwahn and Alexander Krauss and Tobias Nipkow},
title = {Finding Lexicographic Orders for Termination Proofs in {Isabelle/HOL}},
crossref = {tphols2007},
pages = {38--53}
}
@InProceedings{bulwahn-et-al:2008:imperative,
author = {Lukas Bulwahn and Alexander Krauss and Florian Haftmann and Levent Erkök and John Matthews},
title = {Imperative Functional Programming with {Isabelle/HOL}},
crossref = {tphols2008},
}
% pages = {38--53}
@Article{ban89,
author = {M. Burrows and M. Abadi and R. M. Needham},
title = {A Logic of Authentication},
journal = PROYAL,
year = 1989,
volume = 426,
pages = {233-271}}
%C
@TechReport{camilleri92,
author = {J. Camilleri and T. F. Melham},
title = {Reasoning with Inductively Defined Relations in the
{HOL} Theorem Prover},
institution = CUCL,
year = 1992,
number = 265,
month = Aug}
@Book{charniak80,
author = {E. Charniak and C. K. Riesbeck and D. V. McDermott},
title = {Artificial Intelligence Programming},
publisher = {Lawrence Erlbaum Associates},
year = 1980}
@article{church40,
author = "Alonzo Church",
title = "A Formulation of the Simple Theory of Types",
journal = JSL,
year = 1940,
volume = 5,
pages = "56-68"}
@book{ClarkeGP-book,author="Edmund Clarke and Orna Grumberg and Doron Peled",
title="Model Checking",publisher=MIT,year=1999}
@PhdThesis{coen92,
author = {Martin D. Coen},
title = {Interactive Program Derivation},
school = {University of Cambridge},
note = {Computer Laboratory Technical Report 272},
month = nov,
year = 1992}
@book{constable86,
author = {R. L. Constable and others},
title = {Implementing Mathematics with the Nuprl Proof
Development System},
publisher = Prentice,
year = 1986}
%D
@Book{davey-priestley,
author = {B. A. Davey and H. A. Priestley},
title = {Introduction to Lattices and Order},
publisher = CUP,
year = 1990}
@Book{devlin79,
author = {Keith J. Devlin},
title = {Fundamentals of Contemporary Set Theory},
publisher = {Springer},
year = 1979}
@book{dummett,
author = {Michael Dummett},
title = {Elements of Intuitionism},
year = 1977,
publisher = {Oxford University Press}}
@incollection{dybjer91,
author = {Peter Dybjer},
title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type
Theory and Their Set-Theoretic Semantics},
crossref = {huet-plotkin91},
pages = {280-306}}
@Article{dyckhoff,
author = {Roy Dyckhoff},
title = {Contraction-Free Sequent Calculi for Intuitionistic Logic},
journal = JSL,
year = 1992,
volume = 57,
number = 3,
pages = {795-807}}
%F
@Article{IMPS,
author = {William M. Farmer and Joshua D. Guttman and F. Javier
Thayer},
title = {{IMPS}: An Interactive Mathematical Proof System},
journal = JAR,
volume = 11,
number = 2,
year = 1993,
pages = {213-248}}
@InProceedings{felty91a,
Author = {Amy Felty},
Title = {A Logic Program for Transforming Sequent Proofs to Natural
Deduction Proofs},
crossref = {extensions91},
pages = {157-178}}
@Article{fleuriot-jcm,
author = {Jacques Fleuriot and Lawrence C. Paulson},
title = {Mechanizing Nonstandard Real Analysis},
journal = {LMS Journal of Computation and Mathematics},
year = 2000,
volume = 3,
pages = {140-190},
note = {\url{http://www.lms.ac.uk/jcm/3/lms1999-027/}}
}
@TechReport{frost93,
author = {Jacob Frost},
title = {A Case Study of Co-induction in {Isabelle HOL}},
institution = CUCL,
number = 308,
year = 1993,
month = Aug}
%revised version of frost93
@TechReport{frost95,
author = {Jacob Frost},
title = {A Case Study of Co-induction in {Isabelle}},
institution = CUCL,
number = 359,
year = 1995,
month = Feb}
@inproceedings{OBJ,
author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud
and J. Meseguer},
title = {Principles of {OBJ2}},
booktitle = POPL,
year = 1985,
pages = {52-66}}
%G
@book{gallier86,
author = {J. H. Gallier},
title = {Logic for Computer Science:
Foundations of Automatic Theorem Proving},
year = 1986,
publisher = {Harper \& Row}}
@Book{galton90,
author = {Antony Galton},
title = {Logic for Information Technology},
publisher = {Wiley},
year = 1990}
@Article{Gentzen:1935,
author = {G. Gentzen},
title = {Untersuchungen {\"u}ber das logische {S}chlie{\ss}en},
journal = {Math. Zeitschrift},
year = 1935
}
@InProceedings{gimenez-codifying,
author = {Eduardo Gim{\'e}nez},
title = {Codifying Guarded Definitions with Recursive Schemes},
crossref = {types94},
pages = {39-59}
}
@book{girard89,
author = {Jean-Yves Girard},
title = {Proofs and Types},
year = 1989,
publisher = CUP,
note = {Translated by Yves LaFont and Paul Taylor}}
@Book{mgordon-hol,
editor = {M. J. C. Gordon and T. F. Melham},
title = {Introduction to {HOL}: A Theorem Proving Environment for
Higher Order Logic},
publisher = CUP,
year = 1993}
@book{mgordon79,
author = {Michael J. C. Gordon and Robin Milner and Christopher P.
Wadsworth},
title = {Edinburgh {LCF}: A Mechanised Logic of Computation},
year = 1979,
publisher = {Springer},
series = {LNCS 78}}
@inproceedings{Gunter-HOL92,author={Elsa L. Gunter},
title={Why we can't have {SML} style datatype declarations in {HOL}},
booktitle={Higher Order Logic Theorem Proving and its Applications: Proc.\
IFIP TC10/WG10.2 Intl. Workshop, 1992},
editor={L.J.M. Claesen and M.J.C. Gordon},
publisher=NH,year=1993,pages={561--568}}
@InProceedings{gunter-trees,
author = {Elsa L. Gunter},
title = {A Broader Class of Trees for Recursive Type Definitions for
{HOL}},
crossref = {hug93},
pages = {141-154}}
%H
@InProceedings{Haftmann-Wenzel:2006:classes,
author = {Florian Haftmann and Makarius Wenzel},
title = {Constructive Type Classes in {Isabelle}},
editor = {T. Altenkirch and C. McBride},
booktitle = {Types for Proofs and Programs, TYPES 2006},
publisher = {Springer},
series = {LNCS},
volume = {4502},
year = {2007}
}
@inproceedings{Haftmann-Nipkow:2010:code,
author = {Florian Haftmann and Tobias Nipkow},
title = {Code Generation via Higher-Order Rewrite Systems},
booktitle = {Functional and Logic Programming: 10th International Symposium: FLOPS 2010},
year = 2010,
publisher = Springer,
series = LNCS,
editor = {Matthias Blume and Naoki Kobayashi and Germ{\'a}n Vidal},
volume = 6009
}
@InProceedings{Haftmann-Wenzel:2009,
author = {Florian Haftmann and Makarius Wenzel},
title = {Local theory specifications in {Isabelle/Isar}},
editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
booktitle = {Types for Proofs and Programs, TYPES 2008},
publisher = {Springer},
series = {LNCS},
volume = {5497},
year = {2009}
}
@manual{isabelle-classes,
author = {Florian Haftmann},
title = {Haskell-style type classes with {Isabelle}/{Isar}},
institution = TUM,
note = {\url{http://isabelle.in.tum.de/doc/classes.pdf}}
}
@manual{isabelle-codegen,
author = {Florian Haftmann},
title = {Code generation from Isabelle theories},
institution = TUM,
note = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}}
}
@Book{halmos60,
author = {Paul R. Halmos},
title = {Naive Set Theory},
publisher = {Van Nostrand},
year = 1960}
@book{HarelKT-DL,author={David Harel and Dexter Kozen and Jerzy Tiuryn},
title={Dynamic Logic},publisher=MIT,year=2000}
@Book{hennessy90,
author = {Matthew Hennessy},
title = {The Semantics of Programming Languages: An Elementary
Introduction Using Structural Operational Semantics},
publisher = {Wiley},
year = 1990}
@book{HopcroftUllman,author={John E. Hopcroft and Jeffrey D. Ullman},
title={Introduction to Automata Theory, Languages, and Computation.},
publisher={Addison-Wesley},year=1979}
@Article{haskell-report,
author = {Paul Hudak and Simon Peyton Jones and Philip Wadler},
title = {Report on the Programming Language {Haskell}: A
Non-strict, Purely Functional Language},
journal = SIGPLAN,
year = 1992,
volume = 27,
number = 5,
month = May,
note = {Version 1.2}}
@Article{haskell-tutorial,
author = {Paul Hudak and Joseph H. Fasel},
title = {A Gentle Introduction to {Haskell}},
journal = SIGPLAN,
year = 1992,
volume = 27,
number = 5,
month = May}
@misc{sine,
author = "Kry\v{s}tof Hoder",
title = "SInE (Sumo Inference Engine)",
note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"}
@book{Hudak-Haskell,author={Paul Hudak},
title={The Haskell School of Expression},publisher=CUP,year=2000}
@article{huet75,
author = {G. P. Huet},
title = {A Unification Algorithm for Typed $\lambda$-Calculus},
journal = TCS,
volume = 1,
year = 1975,
pages = {27-57}}
@article{huet78,
author = {G. P. Huet and B. Lang},
title = {Proving and Applying Program Transformations Expressed with
Second-Order Patterns},
journal = acta,
volume = 11,
year = 1978,
pages = {31-55}}
@inproceedings{huet88,
author = {G{\'e}rard Huet},
title = {Induction Principles Formalized in the {Calculus of
Constructions}},
booktitle = {Programming of Future Generation Computers},
editor = {K. Fuchi and M. Nivat},
year = 1988,
pages = {205-216},
publisher = {Elsevier}}
@Book{Huth-Ryan-book,
author = {Michael Huth and Mark Ryan},
title = {Logic in Computer Science. Modelling and reasoning about systems},
publisher = CUP,
year = 2000}
@InProceedings{Harrison:1996:MizarHOL,
author = {J. Harrison},
title = {A {Mizar} Mode for {HOL}},
pages = {203--220},
crossref = {tphols96}}
@misc{metis,
author = "Joe Hurd",
title = "Metis Theorem Prover",
note = "\url{http://www.gilith.com/software/metis/}"}
%J
@article{haskell-revised-report,
author = {Simon {Peyton Jones} and others},
title = {The {Haskell} 98 Language and Libraries: The Revised Report},
journal = {Journal of Functional Programming},
volume = 13,
number = 1,
pages = {0--255},
month = {Jan},
year = 2003,
note = {\url{http://www.haskell.org/definition/}}}
@book{jackson-2006,
author = "Daniel Jackson",
title = "Software Abstractions: Logic, Language, and Analysis",
publisher = MIT,
year = 2006}
%K
@InProceedings{kammueller-locales,
author = {Florian Kamm{\"u}ller and Markus Wenzel and
Lawrence C. Paulson},
title = {Locales: A Sectioning Concept for {Isabelle}},
crossref = {tphols99}}
@book{Knuth3-75,
author={Donald E. Knuth},
title={The Art of Computer Programming, Volume 3: Sorting and Searching},
publisher={Addison-Wesley},
year=1975}
@Article{korf85,
author = {R. E. Korf},
title = {Depth-First Iterative-Deepening: an Optimal Admissible
Tree Search},
journal = AI,
year = 1985,
volume = 27,
pages = {97-109}}
@InProceedings{krauss2006,
author = {Alexander Krauss},
title = {Partial Recursive Functions in {Higher-Order Logic}},
crossref = {ijcar2006},
pages = {589--603}}
@PhdThesis{krauss_phd,
author = {Alexander Krauss},
title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
school = {Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
year = {2009},
address = {Germany}
}
@manual{isabelle-function,
author = {Alexander Krauss},
title = {Defining Recursive Functions in {Isabelle/HOL}},
institution = TUM,
note = {\url{http://isabelle.in.tum.de/doc/functions.pdf}}
}
@Book{kunen80,
author = {Kenneth Kunen},
title = {Set Theory: An Introduction to Independence Proofs},
publisher = NH,
year = 1980}
%L
@manual{OCaml,
author = {Xavier Leroy and others},
title = {The Objective Caml system -- Documentation and user's manual},
note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}}
@incollection{lochbihler-2010,
title = "Coinduction",
author = "Andreas Lochbihler",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence C. Paulson",
publisher = "\url{http://afp.sourceforge.net/entries/Coinductive.shtml}",
month = "Feb.",
year = 2010}
@InProceedings{lowe-fdr,
author = {Gavin Lowe},
title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key
Protocol using {CSP} and {FDR}},
booktitle = {Tools and Algorithms for the Construction and Analysis
of Systems: second international workshop, TACAS '96},
editor = {T. Margaria and B. Steffen},
series = {LNCS 1055},
year = 1996,
publisher = {Springer},
pages = {147-166}}
%M
@Article{mw81,
author = {Zohar Manna and Richard Waldinger},
title = {Deductive Synthesis of the Unification Algorithm},
journal = SCP,
year = 1981,
volume = 1,
number = 1,
pages = {5-48}}
@InProceedings{martin-nipkow,
author = {Ursula Martin and Tobias Nipkow},
title = {Ordered Rewriting and Confluence},
crossref = {cade10},
pages = {366-380}}
@book{martinlof84,
author = {Per Martin-L{\"o}f},
title = {Intuitionistic type theory},
year = 1984,
publisher = {Bibliopolis}}
@incollection{melham89,
author = {Thomas F. Melham},
title = {Automating Recursive Type Definitions in Higher Order
Logic},
pages = {341-386},
crossref = {birtwistle89}}
@Article{Miller:1991,
author = {Dale Miller},
title = {A Logic Programming Language with Lambda-Abstraction, Function Variables,
and Simple Unification},
journal = {Journal of Logic and Computation},
year = 1991,
volume = 1,
number = 4
}
@Article{miller-mixed,
Author = {Dale Miller},
Title = {Unification Under a Mixed Prefix},
journal = JSC,
volume = 14,
number = 4,
pages = {321-358},
Year = 1992}
@Article{milner78,
author = {Robin Milner},
title = {A Theory of Type Polymorphism in Programming},
journal = "J. Comp.\ Sys.\ Sci.",
year = 1978,
volume = 17,
pages = {348-375}}
@TechReport{milner-ind,
author = {Robin Milner},
title = {How to Derive Inductions in {LCF}},
institution = Edinburgh,
year = 1980,
type = {note}}
@Article{milner-coind,
author = {Robin Milner and Mads Tofte},
title = {Co-induction in Relational Semantics},
journal = TCS,
year = 1991,
volume = 87,
pages = {209-220}}
@Book{milner89,
author = {Robin Milner},
title = {Communication and Concurrency},
publisher = Prentice,
year = 1989}
@book{SML,author="Robin Milner and Mads Tofte and Robert Harper",
title="The Definition of Standard ML",publisher=MIT,year=1990}
@PhdThesis{monahan84,
author = {Brian Q. Monahan},
title = {Data Type Proofs using Edinburgh {LCF}},
school = {University of Edinburgh},
year = 1984}
@article{MuellerNvOS99,
author=
{Olaf M{\"u}ller and Tobias Nipkow and Oheimb, David von and Oscar Slotosch},
title={{HOLCF = HOL + LCF}},journal=JFP,year=1999,volume=9,pages={191--223}}
@Manual{Muzalewski:Mizar,
title = {An Outline of {PC} {Mizar}},
author = {Micha{\l} Muzalewski},
organization = {Fondation of Logic, Mathematics and Informatics
--- Mizar Users Group},
year = 1993,
note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz}}
}
%N
@InProceedings{NaraschewskiW-TPHOLs98,
author = {Wolfgang Naraschewski and Markus Wenzel},
title =
{Object-Oriented Verification based on Record Subtyping in
Higher-Order Logic},
crossref = {tphols98}}
@inproceedings{nazareth-nipkow,
author = {Dieter Nazareth and Tobias Nipkow},
title = {Formal Verification of Algorithm {W}: The Monomorphic Case},
crossref = {tphols96},
pages = {331-345},
year = 1996}
@Article{needham-schroeder,
author = "Roger M. Needham and Michael D. Schroeder",
title = "Using Encryption for Authentication in Large Networks
of Computers",
journal = cacm,
volume = 21,
number = 12,
pages = "993-999",
month = dec,
year = 1978}
@inproceedings{nipkow-W,
author = {Wolfgang Naraschewski and Tobias Nipkow},
title = {Type Inference Verified: Algorithm {W} in {Isabelle/HOL}},
booktitle = {Types for Proofs and Programs: Intl. Workshop TYPES '96},
editor = {E. Gim{\'e}nez and C. Paulin-Mohring},
publisher = Springer,
series = LNCS,
volume = 1512,
pages = {317-332},
year = 1998}
@InCollection{nipkow-sorts93,
author = {T. Nipkow},
title = {Order-Sorted Polymorphism in {Isabelle}},
booktitle = {Logical Environments},
publisher = CUP,
year = 1993,
editor = {G. Huet and G. Plotkin},
pages = {164--188}
}
@Misc{nipkow-types93,
author = {Tobias Nipkow},
title = {Axiomatic Type Classes (in {I}sabelle)},
howpublished = {Presentation at the workshop \emph{Types for Proof and Programs}, Nijmegen},
year = 1993
}
@inproceedings{Nipkow-CR,
author = {Tobias Nipkow},
title = {More {Church-Rosser} Proofs (in {Isabelle/HOL})},
booktitle = {Automated Deduction --- CADE-13},
editor = {M. McRobbie and J.K. Slaney},
publisher = Springer,
series = LNCS,
volume = 1104,
pages = {733-747},
year = 1996}
% WAS Nipkow-LICS-93
@InProceedings{nipkow-patterns,
title = {Functional Unification of Higher-Order Patterns},
author = {Tobias Nipkow},
pages = {64-74},
crossref = {lics8},
url = {\url{ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/lics93.html}},
keywords = {unification}}
@article{nipkow-IMP,
author = {Tobias Nipkow},
title = {Winskel is (almost) Right: Towards a Mechanized Semantics Textbook},
journal = FAC,
volume = 10,
pages = {171-186},
year = 1998}
@inproceedings{Nipkow-TYPES02,
author = {Tobias Nipkow},
title = {{Structured Proofs in Isar/HOL}},
booktitle = {Types for Proofs and Programs (TYPES 2002)},
editor = {H. Geuvers and F. Wiedijk},
year = 2003,
publisher = Springer,
series = LNCS,
volume = 2646,
pages = {259-278}}
@manual{isabelle-HOL,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {{Isabelle}'s Logics: {HOL}},
institution = {Institut f{\"u}r Informatik, Technische Universi{\"a}t
M{\"u}nchen and Computer Laboratory, University of Cambridge},
note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}}}
@article{nipkow-prehofer,
author = {Tobias Nipkow and Christian Prehofer},
title = {Type Reconstruction for Type Classes},
journal = JFP,
volume = 5,
number = 2,
year = 1995,
pages = {201-224}}
@InProceedings{Nipkow-Prehofer:1993,
author = {T. Nipkow and C. Prehofer},
title = {Type checking type classes},
booktitle = {ACM Symp.\ Principles of Programming Languages},
year = 1993
}
@Book{isa-tutorial,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {Isabelle/{HOL}: A Proof Assistant for Higher-Order Logic},
publisher = Springer,
year = 2002,
series = LNCS,
volume = 2283}
@Article{noel,
author = {Philippe No{\"e}l},
title = {Experimenting with {Isabelle} in {ZF} Set Theory},
journal = JAR,
volume = 10,
number = 1,
pages = {15-58},
year = 1993}
@book{nordstrom90,
author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith},
title = {Programming in {Martin-L{\"o}f}'s Type Theory. An
Introduction},
publisher = {Oxford University Press},
year = 1990}
%O
@Manual{pvs-language,
title = {The {PVS} specification language},
author = {S. Owre and N. Shankar and J. M. Rushby},
organization = {Computer Science Laboratory, SRI International},
address = {Menlo Park, CA},
note = {Beta release},
year = 1993,
month = apr,
url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
%P
% replaces paulin92
@InProceedings{paulin-tlca,
author = {Christine Paulin-Mohring},
title = {Inductive Definitions in the System {Coq}: Rules and
Properties},
crossref = {tlca93},
pages = {328-345}}
@InProceedings{paulson-CADE,
author = {Lawrence C. Paulson},
title = {A Fixedpoint Approach to Implementing (Co)Inductive
Definitions},
pages = {148-161},
crossref = {cade12}}
@InProceedings{paulson-COLOG,
author = {Lawrence C. Paulson},
title = {A Formulation of the Simple Theory of Types (for
{Isabelle})},
pages = {246-274},
crossref = {colog88},
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
@Article{paulson-coind,
author = {Lawrence C. Paulson},
title = {Mechanizing Coinduction and Corecursion in Higher-Order
Logic},
journal = JLC,
year = 1997,
volume = 7,
number = 2,
month = mar,
pages = {175-204}}
@manual{isabelle-intro,
author = {Lawrence C. Paulson},
title = {Introduction to {Isabelle}},
institution = CUCL,
note = {\url{http://isabelle.in.tum.de/doc/intro.pdf}}}
@manual{isabelle-logics,
author = {Lawrence C. Paulson},
title = {{Isabelle's} Logics},
institution = CUCL,
note = {\url{http://isabelle.in.tum.de/doc/logics.pdf}}}
@manual{isabelle-ref,
author = {Lawrence C. Paulson},
title = {The {Isabelle} Reference Manual},
institution = CUCL,
note = {\url{http://isabelle.in.tum.de/doc/ref.pdf}}}
@manual{isabelle-ZF,
author = {Lawrence C. Paulson},
title = {{Isabelle}'s Logics: {FOL} and {ZF}},
institution = CUCL,
note = {\url{http://isabelle.in.tum.de/doc/logics-ZF.pdf}}}
@article{paulson-found,
author = {Lawrence C. Paulson},
title = {The Foundation of a Generic Theorem Prover},
journal = JAR,
volume = 5,
number = 3,
pages = {363-397},
year = 1989,
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
%replaces paulson-final
@Article{paulson-mscs,
author = {Lawrence C. Paulson},
title = {Final Coalgebras as Greatest Fixed Points
in {ZF} Set Theory},
journal = {Mathematical Structures in Computer Science},
year = 1999,
volume = 9,
number = 5,
pages = {545-567}}
@InCollection{paulson-generic,
author = {Lawrence C. Paulson},
title = {Generic Automatic Proof Tools},
crossref = {wos-fest},
chapter = 3}
@Article{paulson-gr,
author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of
Choice},
journal = JAR,
year = 1996,
volume = 17,
number = 3,
month = dec,
pages = {291-323}}
@InCollection{paulson-fixedpt-milner,
author = {Lawrence C. Paulson},
title = {A Fixedpoint Approach to (Co)inductive and
(Co)datatype Definitions},
pages = {187-211},
crossref = {milner-fest}}
@book{milner-fest,
title = {Proof, Language, and Interaction:
Essays in Honor of {Robin Milner}},
booktitle = {Proof, Language, and Interaction:
Essays in Honor of {Robin Milner}},
publisher = MIT,
year = 2000,
editor = {Gordon Plotkin and Colin Stirling and Mads Tofte}}
@InCollection{paulson-handbook,
author = {Lawrence C. Paulson},
title = {Designing a Theorem Prover},
crossref = {handbk-lics2},
pages = {415-475}}
@Book{paulson-isa-book,
author = {Lawrence C. Paulson},
title = {Isabelle: A Generic Theorem Prover},
publisher = {Springer},
year = 1994,
note = {LNCS 828}}
@Book{isabelle-hol-book,
author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
publisher = {Springer},
year = 2002,
note = {LNCS 2283}}
@InCollection{paulson-markt,
author = {Lawrence C. Paulson},
title = {Tool Support for Logics of Programs},
booktitle = {Mathematical Methods in Program Development:
Summer School Marktoberdorf 1996},
publisher = {Springer},
pages = {461-498},
year = {Published 1997},
editor = {Manfred Broy},
series = {NATO ASI Series F}}
%replaces Paulson-ML and paulson91
@book{paulson-ml2,
author = {Lawrence C. Paulson},
title = {{ML} for the Working Programmer},
year = 1996,
edition = {2nd},
publisher = CUP}
@article{paulson-natural,
author = {Lawrence C. Paulson},
title = {Natural Deduction as Higher-order Resolution},
journal = JLP,
volume = 3,
pages = {237-258},
year = 1986,
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
@Article{paulson-set-I,
author = {Lawrence C. Paulson},
title = {Set Theory for Verification: {I}. {From}
Foundations to Functions},
journal = JAR,
volume = 11,
number = 3,
pages = {353-389},
year = 1993,
url = {\url{http://www.cl.cam.ac.uk/users/lcp/papers/Sets/set-I.pdf}}}
@Article{paulson-set-II,
author = {Lawrence C. Paulson},
title = {Set Theory for Verification: {II}. {Induction} and
Recursion},
journal = JAR,
volume = 15,
number = 2,
pages = {167-215},
year = 1995,
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
@article{paulson85,
author = {Lawrence C. Paulson},
title = {Verifying the Unification Algorithm in {LCF}},
journal = SCP,
volume = 5,
pages = {143-170},
year = 1985}
%replaces Paulson-LCF
@book{paulson87,
author = {Lawrence C. Paulson},
title = {Logic and Computation: Interactive proof with Cambridge
LCF},
year = 1987,
publisher = CUP}
@incollection{paulson700,
author = {Lawrence C. Paulson},
title = {{Isabelle}: The Next 700 Theorem Provers},
crossref = {odifreddi90},
pages = {361-386},
url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
% replaces paulson-ns and paulson-security
@Article{paulson-jcs,
author = {Lawrence C. Paulson},
title = {The Inductive Approach to Verifying Cryptographic Protocols},
journal = JCS,
year = 1998,
volume = 6,
pages = {85-128}}
@Article{paulson-tls,
author = {Lawrence C. Paulson},
title = {Inductive Analysis of the {Internet} Protocol {TLS}},
journal = TISSEC,
month = aug,
year = 1999,
volume = 2,
number = 3,
pages = {332-351}}
@Article{paulson-yahalom,
author = {Lawrence C. Paulson},
title = {Relations Between Secrets:
Two Formal Analyses of the {Yahalom} Protocol},
journal = JCS,
volume = 9,
number = 3,
pages = {197-216},
year = 2001}}
@article{pelletier86,
author = {F. J. Pelletier},
title = {Seventy-five Problems for Testing Automatic Theorem
Provers},
journal = JAR,
volume = 2,
pages = {191-216},
year = 1986,
note = {Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135}}
@Article{pitts94,
author = {Andrew M. Pitts},
title = {A Co-induction Principle for Recursively Defined Domains},
journal = TCS,
volume = 124,
pages = {195-219},
year = 1994}
@Article{plaisted90,
author = {David A. Plaisted},
title = {A Sequent-Style Model Elimination Strategy and a Positive
Refinement},
journal = JAR,
year = 1990,
volume = 6,
number = 4,
pages = {389-402}}
%Q
@Article{quaife92,
author = {Art Quaife},
title = {Automated Deduction in {von Neumann-Bernays-G\"{o}del} Set
Theory},
journal = JAR,
year = 1992,
volume = 8,
number = 1,
pages = {91-147}}
%R
@TechReport{rasmussen95,
author = {Ole Rasmussen},
title = {The {Church-Rosser} Theorem in {Isabelle}: A Proof Porting
Experiment},
institution = {Computer Laboratory, University of Cambridge},
year = 1995,
number = 364,
month = may,
url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
@Book{reeves90,
author = {Steve Reeves and Michael Clarke},
title = {Logic for Computer Science},
publisher = {Addison-Wesley},
year = 1990}
@article{riazanov-voronkov-2002,
author = "Alexander Riazanov and Andrei Voronkov",
title = "The Design and Implementation of {Vampire}",
journal = "Journal of AI Communications",
year = 2002,
volume = 15,
number ="2/3",
pages = "91--110"}
@book{Rosen-DMA,author={Kenneth H. Rosen},
title={Discrete Mathematics and Its Applications},
publisher={McGraw-Hill},year=1998}
@InProceedings{Rudnicki:1992:MizarOverview,
author = {P. Rudnicki},
title = {An Overview of the {MIZAR} Project},
booktitle = {1992 Workshop on Types for Proofs and Programs},
year = 1992,
organization = {Chalmers University of Technology},
publisher = {Bastad}
}
%S
@inproceedings{saaltink-fme,
author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and
Dan Craigen and Irwin Meisels},
title = {An {EVES} Data Abstraction Example},
pages = {578-596},
crossref = {fme93}}
@Article{Schroeder-Heister:1984,
author = {Peter Schroeder-Heister},
title = {A Natural Extension of Natural Deduction},
journal = {Journal of Symbolic Logic},
year = 1984,
volume = 49,
number = 4
}
@article{schulz-2002,
author = "Stephan Schulz",
title = "E---A Brainiac Theorem Prover",
journal = "Journal of AI Communications",
year = 2002,
volume = 15,
number ="2/3",
pages = "111--126"}
@misc{sledgehammer-2009,
key = "Sledgehammer",
title = "The {S}ledgehammer: Let Automatic Theorem Provers
Write Your {I}s\-a\-belle Scripts",
note = "\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/sledgehammer.html}"}
@inproceedings{slind-tfl,
author = {Konrad Slind},
title = {Function Definition in Higher Order Logic},
crossref = {tphols96},
pages = {381-397}}
@inproceedings{snark,
author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
title = {Deductive composition of astronomical software from subroutine libraries},
pages = "341--355",
crossref = {cade12}}
@book{suppes72,
author = {Patrick Suppes},
title = {Axiomatic Set Theory},
year = 1972,
publisher = {Dover}}
@inproceedings{sutcliffe-2000,
author = "Geoff Sutcliffe",
title = "System Description: {SystemOnTPTP}",
editor = "J. G. Carbonell and J. Siekmann",
booktitle = {Automated Deduction --- {CADE}-17 International Conference},
series = "Lecture Notes in Artificial Intelligence",
volume = {1831},
pages = "406--410",
year = 2000,
publisher = Springer}
@InCollection{szasz93,
author = {Nora Szasz},
title = {A Machine Checked Proof that {Ackermann's} Function is not
Primitive Recursive},
crossref = {huet-plotkin93},
pages = {317-338}}
@TechReport{Syme:1997:DECLARE,
author = {D. Syme},
title = {{DECLARE}: A Prototype Declarative Proof System for Higher Order Logic},
institution = {University of Cambridge Computer Laboratory},
year = 1997,
number = 416
}
@PhdThesis{Syme:1998:thesis,
author = {D. Syme},
title = {Declarative Theorem Proving for Operational Semantics},
school = {University of Cambridge},
year = 1998,
note = {Submitted}
}
@InProceedings{Syme:1999:TPHOL,
author = {D. Syme},
title = {Three Tactic Theorem Proving},
crossref = {tphols99}}
%T
@book{takeuti87,
author = {G. Takeuti},
title = {Proof Theory},
year = 1987,
publisher = NH,
edition = {2nd}}
@Book{thompson91,
author = {Simon Thompson},
title = {Type Theory and Functional Programming},
publisher = {Addison-Wesley},
year = 1991}
@book{Thompson-Haskell,author={Simon Thompson},
title={Haskell: The Craft of Functional Programming},
publisher={Addison-Wesley},year=1999}
@misc{kodkod-2009,
author = "Emina Torlak",
title = {Kodkod: Constraint Solver for Relational Logic},
note = "\url{http://alloy.mit.edu/kodkod/}"}
@misc{kodkod-2009-options,
author = "Emina Torlak",
title = "Kodkod {API}: Class {Options}",
note = "\url{http://alloy.mit.edu/kodkod/docs/kodkod/engine/config/Options.html}"}
@inproceedings{torlak-jackson-2007,
title = "Kodkod: A Relational Model Finder",
author = "Emina Torlak and Daniel Jackson",
editor = "Orna Grumberg and Michael Huth",
booktitle = "TACAS 2007",
series = LNCS,
volume = {4424},
pages = "632--647",
year = 2007,
publisher = Springer}
@Unpublished{Trybulec:1993:MizarFeatures,
author = {A. Trybulec},
title = {Some Features of the {Mizar} Language},
note = {Presented at a workshop in Turin, Italy},
year = 1993
}
%V
@Unpublished{voelker94,
author = {Norbert V{\"o}lker},
title = {The Verification of a Timer Program using {Isabelle/HOL}},
url = {\url{ftp://ftp.fernuni-hagen.de/pub/fachb/et/dvt/projects/verification/timer.tar.gz}},
year = 1994,
month = aug}
%W
@inproceedings{wadler89how,
author = {P. Wadler and S. Blott},
title = {How to make ad-hoc polymorphism less ad-hoc},
booktitle = {ACM Symp.\ Principles of Programming Languages},
year = 1989
}
@phdthesis{weber-2008,
author = "Tjark Weber",
title = "SAT-Based Finite Model Generation for Higher-Order Logic",
school = {Dept.\ of Informatics, T.U. M\"unchen},
type = "{Ph.D.}\ thesis",
year = 2008}
@Misc{x-symbol,
author = {Christoph Wedler},
title = {Emacs package ``{X-Symbol}''},
note = {\url{http://x-symbol.sourceforge.net}}
}
@misc{weidenbach-et-al-2009,
author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski",
title = "{SPASS} Version 3.5",
note = {\url{http://www.spass-prover.org/publications/spass.pdf}}}
@manual{isabelle-sys,
author = {Markus Wenzel and Stefan Berghofer},
title = {The {Isabelle} System Manual},
institution = {TU Munich},
note = {\url{http://isabelle.in.tum.de/doc/system.pdf}}}
@manual{isabelle-isar-ref,
author = {Makarius Wenzel},
title = {The {Isabelle/Isar} Reference Manual},
institution = {TU Munich},
note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}}}
@manual{isabelle-implementation,
author = {Makarius Wenzel},
title = {The {Isabelle/Isar} Implementation},
institution = {TU Munich},
note = {\url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
@InProceedings{Wenzel:1999:TPHOL,
author = {Markus Wenzel},
title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents},
crossref = {tphols99}}
@InProceedings{Wenzel:1997:TPHOL,
author = {Markus Wenzel},
title = {Type Classes and Overloading in Higher-Order Logic},
crossref = {tphols97}}
@phdthesis{Wenzel-PhD,
author={Markus Wenzel},
title={Isabelle/Isar --- a versatile environment for human-readable formal proof documents},
school={Institut f{\"u}r Informatik, Technische Universit{\"a}t M{\"u}nchen},
year=2002,
note = {\url{http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2002/wenzel.html}}}
@Article{Wenzel-Wiedijk:2002,
author = {Freek Wiedijk and Markus Wenzel},
title = {A comparison of the mathematical proof languages {Mizar} and {Isar}.},
journal = {Journal of Automated Reasoning},
year = 2002,
volume = 29,
number = {3-4}
}
@InCollection{Wenzel-Paulson:2006,
author = {Markus Wenzel and Lawrence C. Paulson},
title = {{Isabelle/Isar}},
booktitle = {The Seventeen Provers of the World},
year = 2006,
editor = {F. Wiedijk},
series = {LNAI 3600}
}
@InCollection{Wenzel:2006:Festschrift,
author = {Makarius Wenzel},
title = {{Isabelle/Isar} --- a generic framework for human-readable proof documents},
booktitle = {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
publisher = {University of Bia{\l}ystok},
year = 2007,
editor = {R. Matuszewski and A. Zalewska},
volume = {10(23)},
series = {Studies in Logic, Grammar, and Rhetoric},
note = {\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}}
}
@book{principia,
author = {A. N. Whitehead and B. Russell},
title = {Principia Mathematica},
year = 1962,
publisher = CUP,
note = {Paperback edition to *56,
abridged from the 2nd edition (1927)}}
@Misc{Wiedijk:1999:Mizar,
author = {Freek Wiedijk},
title = {Mizar: An Impression},
howpublished = {Unpublished paper},
year = 1999,
note = {\url{http://www.cs.kun.nl/~freek/mizar/mizarintro.ps.gz}}
}
@Misc{Wiedijk:2000:MV,
author = {Freek Wiedijk},
title = {The Mathematical Vernacular},
howpublished = {Unpublished paper},
year = 2000,
note = {\url{http://www.cs.kun.nl/~freek/notes/mv.ps.gz}}
}
@book{winskel93,
author = {Glynn Winskel},
title = {The Formal Semantics of Programming Languages},
publisher = MIT,year=1993}
@InCollection{wos-bledsoe,
author = {Larry Wos},
title = {Automated Reasoning and {Bledsoe's} Dream for the Field},
crossref = {bledsoe-fest},
pages = {297-342}}
@InProceedings{Zammit:1999:TPHOL,
author = {Vincent Zammit},
title = {On the Implementation of an Extensible Declarative Proof Language},
crossref = {tphols99}}
%Z
% CROSS REFERENCES
@book{handbk-lics2,
editor = {S. Abramsky and D. M. Gabbay and T. S. E. Maibaum},
title = {Handbook of Logic in Computer Science},
booktitle = {Handbook of Logic in Computer Science},
publisher = {Oxford University Press},
year = 1992,
volume = 2}
@book{types93,
editor = {Henk Barendregt and Tobias Nipkow},
title = TYPES # {: International Workshop {TYPES '93}},
booktitle = TYPES # {: International Workshop {TYPES '93}},
year = {published 1994},
publisher = {Springer},
series = {LNCS 806}}
@book{barwise-handbk,
editor = {J. Barwise},
title = {Handbook of Mathematical Logic},
booktitle = {Handbook of Mathematical Logic},
year = 1977,
publisher = NH}
@Proceedings{tlca93,
title = {Typed Lambda Calculi and Applications},
booktitle = {Typed Lambda Calculi and Applications},
editor = {M. Bezem and J.F. Groote},
year = 1993,
publisher = {Springer},
series = {LNCS 664}}
@book{birtwistle89,
editor = {Graham Birtwistle and P. A. Subrahmanyam},
title = {Current Trends in Hardware Verification and Automated
Theorem Proving},
booktitle = {Current Trends in Hardware Verification and Automated
Theorem Proving},
publisher = {Springer},
year = 1989}
@book{bledsoe-fest,
title = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
booktitle = {Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
publisher = {Kluwer Academic Publishers},
year = 1991,
editor = {Robert S. Boyer}}
@Proceedings{cade12,
editor = {Alan Bundy},
title = {Automated Deduction --- {CADE}-12
International Conference},
booktitle = {Automated Deduction --- {CADE}-12
International Conference},
year = 1994,
series = {LNAI 814},
publisher = {Springer}}
@book{types94,
editor = {Peter Dybjer and Bengt Nordstr{{\"o}m} and Jan Smith},
title = TYPES # {: International Workshop {TYPES '94}},
booktitle = TYPES # {: International Workshop {TYPES '94}},
year = 1995,
publisher = {Springer},
series = {LNCS 996}}
@book{huet-plotkin91,
editor = {{G{\'e}rard} Huet and Gordon Plotkin},
title = {Logical Frameworks},
booktitle = {Logical Frameworks},
publisher = CUP,
year = 1991}
@book{huet-plotkin93,
editor = {{G{\'e}rard} Huet and Gordon Plotkin},
title = {Logical Environments},
booktitle = {Logical Environments},
publisher = CUP,
year = 1993}
@Proceedings{hug93,
editor = {J. Joyce and C. Seger},
title = {Higher Order Logic Theorem Proving and Its
Applications: HUG '93},
booktitle = {Higher Order Logic Theorem Proving and Its
Applications: HUG '93},
year = {Published 1994},
publisher = {Springer},
series = {LNCS 780}}
@proceedings{colog88,
editor = {P. Martin-L{\"o}f and G. Mints},
title = {COLOG-88: International Conference on Computer Logic},
booktitle = {COLOG-88: International Conference on Computer Logic},
year = {Published 1990},
publisher = {Springer},
organization = {Estonian Academy of Sciences},
address = {Tallinn},
series = {LNCS 417}}
@book{odifreddi90,
editor = {P. Odifreddi},
title = {Logic and Computer Science},
booktitle = {Logic and Computer Science},
publisher = {Academic Press},
year = 1990}
@proceedings{extensions91,
editor = {Peter Schroeder-Heister},
title = {Extensions of Logic Programming},
booktitle = {Extensions of Logic Programming},
year = 1991,
series = {LNAI 475},
publisher = {Springer}}
@proceedings{cade10,
editor = {Mark E. Stickel},
title = {10th } # CADE,
booktitle = {10th } # CADE,
year = 1990,
publisher = {Springer},
series = {LNAI 449}}
@Proceedings{lics8,
editor = {M. Vardi},
title = {Eighth Annual Symposium on Logic in Computer Science},
booktitle = {Eighth Annual Symposium on Logic in Computer Science},
publisher = IEEE,
year = 1993}
@book{wos-fest,
title = {Automated Reasoning and its Applications:
Essays in Honor of {Larry Wos}},
booktitle = {Automated Reasoning and its Applications:
Essays in Honor of {Larry Wos}},
publisher = MIT,
year = 1997,
editor = {Robert Veroff}}
@proceedings{fme93,
editor = {J. C. P. Woodcock and P. G. Larsen},
title = {FME '93: Industrial-Strength Formal Methods},
booktitle = {FME '93: Industrial-Strength Formal Methods},
year = 1993,
publisher = Springer,
series = LNCS,
volume = 670}
@Proceedings{tphols96,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '96},
editor = {J. von Wright and J. Grundy and J. Harrison},
publisher = Springer,
series = LNCS,
volume = 1125,
year = 1996}
@Proceedings{tphols97,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
editor = {Elsa L. Gunter and Amy Felty},
publisher = Springer,
series = LNCS,
volume = 1275,
year = 1997}
@Proceedings{tphols98,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '98},
editor = {Jim Grundy and Malcom Newey},
publisher = Springer,
series = LNCS,
volume = 1479,
year = 1998}
@Proceedings{tphols99,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99},
editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and
Paulin, C. and Thery, L.},
publisher = Springer,
series = LNCS,
volume = 1690,
year = 1999}
@Proceedings{tphols2000,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2000},
editor = {J. Harrison and M. Aagaard},
publisher = Springer,
series = LNCS,
volume = 1869,
year = 2000}
@Proceedings{tphols2001,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2001},
editor = {R. J. Boulton and P. B. Jackson},
publisher = Springer,
series = LNCS,
volume = 2152,
year = 2001}
@Proceedings{ijcar2006,
title = {Automated Reasoning: {IJCAR} 2006},
booktitle = {Automated Reasoning: {IJCAR} 2006},
editor = {U. Furbach and N. Shankar},
publisher = Springer,
series = LNCS,
volume = 4130,
year = 2006}
@Proceedings{tphols2007,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2007},
editor = {K. Schneider and J. Brandt},
publisher = Springer,
series = LNCS,
volume = 4732,
year = 2007}
@Proceedings{tphols2008,
title = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} 2008},
publisher = Springer,
series = LNCS,
year = 2008}
% editor =
% volume = 4732,
@Proceedings{itp2010,
title = {Interactive Theorem Proving: {ITP}-10},
booktitle = {Interactive Theorem Proving: {ITP}-10},
editor = "Matt Kaufmann and Lawrence Paulson",
publisher = Springer,
series = LNCS,
year = 2010}
@unpublished{classes_modules,
title = {{ML} Modules and {Haskell} Type Classes: A Constructive Comparison},
author = {Stefan Wehr et. al.}
}
@misc{wikipedia-2009-aa-trees,
key = "Wikipedia",
title = "Wikipedia: {AA} Tree",
note = "\url{http://en.wikipedia.org/wiki/AA_tree}"}