@Book{Bauer, 
  author = 	 {Heinz Bauer},
  ALTeditor = 	 {},
  title = 	 {Maß- und Integrationstheorie},
  publisher = 	 {de Gruyter},
  year = 	 {1990},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {Berlin; New York},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}
@Book{Billingsley86,
  author =       "Patrick Billingsley",
  title =        "Probability and Measure",
  edition =      "Second",
  publisher =    "John Wiley",
  OPTaddress =      "New York",
  year =         "1986",
}

@Article{ChurchA:forstt,
  author =       "Alonzo Church",
  title =        "A simple theory of types",
  journal =      "Journal of Symbolic Logic",
  volume =       "5",
  year =         "1940",
  pages =        "56--68"
}

@Article{Fleuriot:2000:MNR,
  author =       "Jacques D. Fleuriot and Lawrence C. Paulson",
  title =        "Mechanizing nonstandard real analysis",
  journal =      "LMS Journal of Computation and Mathematics",
  volume =       "3",
  pages =        "140--190",
  year =         "2000",
  coden =        "????",
  ISSN =         "1461-1570",
  mrclass =      "03B35 (03H10 26E35)",
  mrnumber =     "2001j:03022",
  mrreviewer =   "Peter W. Day",
  url =          "http://www.lms.ac.uk/jcm/3/lms1999-027/",
  note = {{Available on the web as} \url{http://www.lms.ac.uk/jcm/3/lms1999-027/}},
  fjournal =     "LMS Journal of Computation and Mathematics",
},
  OPTannote = 	 {}
}

@book{GordonMJCa1993a,
 author      ="Gordon, Michael J. C. and Melham, Thomas F.",
 title       ="Introduction to HOL: A theorem proving 
               environment for higher order logic",
 publisher   ="Cambridge University Press",
 year        ="1993",
 abstractURL ="http://www.dcs.glasgow.ac.uk/~tfm/HOLbook.html"
}

@Article{MIL77a,
  author =       "Robin Milner",
  title =        "A Theory of Type Polymorphism in Programming",
  journal =      "Journal of Computer and System Sciences",
  volume =       "17",
  pages =        "348--375",
  OPTpublisher =    "Academic Press",
  year =         "1977"
}

@Book{MotRag97,
  author =       "Rajeev Motwani and Prabhakar Raghavan",
  title =        "Randomized Algorithms",
  publisher =    "Cambridge University Press",
  year =         "1997",
}
@Book{Nipkow-Paulson-Wenzel:2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002,
note = {{Available on the web as} \url{http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf}}
}
@InCollection{Nipkow93,
  author =       "Tobias Nipkow",
  editor =       "G\'{e}rard Huet and Gordon Plotkin",
  title =        "Order-Sorted Polymorphism in Isabelle",
  booktitle =    "Logical Environments",
  pages =        "164--188",
  publisher =    "Cambridge University Press",
  OPTaddress =      "Cambridge, UK",
  year =         "1993",
  keywords =     "functional programming",
  ISBN =         "0-521-43312-6",
  abstract =     "ML-style polymorphism can be generalized from a
                 single-sorted algebra of types to an order-sorted one
                 by adding a partially ordered layer of 'sorts' on top
                 of the types. Type inference proceeds as in the
                 Hindley/Milner system, except that order-sorted
                 unification of types is used. The resulting system has
                 been implemented in Isabelle to permit type variables
                 to range over user-definable subsets of all types.
                 Order-sorted polymorphism allows a simple specification
                 of type restriction in many logical systems. It
                 accommodates user-defined parametric overloading and
                 allows for a limited form of abstract axiomatic
                 reasoning. It can also explain type inference with
                 Standard ML's equality types and Haskell's type classes
                 (T. Nipkow and G.Snetting, 1991).",
note = {{Available on the web as} \url{http://www4.informatik.tu-muenchen.de/~nipkow/pubs/lf91.html}}
}
@Book{Oberschelp1993,
  author = 	 {Arnold Oberschelp},
  ALTeditor = 	 {},
  title = 	 {Rekursionstheorie},
  OPTchapter = 	 {},
  publisher = 	 {BI-Wissenschafts-Verlag},
  year = 	 {1993},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {Mannheim; Leipzig; Wien; Zürich},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTpages = 	 {85},
  OPTnote = 	 {},
  OPTannote = 	 {}
}
@Book{Paulson96,
  key =          "Paulson",
  author =       "Lawrence C. Paulson",
  title =        "{ML} for the Working Programmer",
  publisher =    "Cambridge University Press",
  year =         "1996",
  OPTaddress =      "New York, NY",
  edition =      "second",
  annote =       "Many references.",
}
@Article{Paulson:1994:IGT,
  author =       "Lawrence C. Paulson",
  title =        "{Isabelle}: {A} Generic Theorem Prover",
  journal =      "Lecture Notes in Computer Science",
  volume =       "828",
  pages =        "xvii + 321",
  year =         "1994",
  coden =        "LNCSD9",
  ISSN =         "0302-9743",
  bibdate =      "Tue Apr 28 14:47:35 1998",
  OPTpublisher = {Springer},
  acknowledgement = ack-nhfb,
}
@InProceedings{QED,
  author = 	 {Anonymous},
  title = 	 {The {QED} manifesto},
  booktitle = 	 {12th International Conference on Automated Deduction (CADE-12)},
  OPTcrossref =  {},
  OPTkey = 	 {},
  OPTpages = 	 {},
  year = 	 {1994},
  editor = 	 {Alan Bundy},
  volume = 	 {814},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Artificial Intelligence},
  OPTaddress = 	 {Nancy, France},
  OPTmonth = 	 {June},
  OPTorganization = {},
  OPTpublisher = {Springer},
  OPTnote = 	 {},
  OPTannote = 	 {},
note = {{Available on the web as} \url{http://www.rbjones.com/rbjpub/logic/qedres00.htm}}
}
@InBook{Royden1968,
  author = 	 {Halsey Lawrence Royden},
  ALTeditor = 	 {},
  title = 	 {Real Analysis},
  chapter = 	 {},
  publisher = 	 {Macmillan},
  year = 	 {1968},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {New York},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTpages = 	 {32 ff},
  OPTnote = 	 {},
  OPTannote = 	 {}
}
@misc{Schechter,
  author = 	 {Eric Schechter},
  title = 	 {An Introduction to The Gauge Integral},
  OPTkey = 	 {},
  OPTmonth = 	 {},
  year = 	 {2001},
  note = {\mbox{Unpublished. Available on the web} as \url{http://www.math.vanderbilt.edu/~schectex/ccc/gauge/}}
}


@Misc{Skalberg,
  OPTkey = 	 {},
  author = 	 {Sebastian Skalberg},
  title = 	 {Import Tool},
  OPThowpublished = {},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  note = 	 {Available on the web as \url{http://www.mangust.dk/skalberg/isabelle.php}},
  OPTannote = 	 {}
}

@PhdThesis{Wenzel2001,
  author = 	 {Markus Wenzel},
  title = 	 {Isabelle/Isar --- a versatile environment for human-readable formal proof documents},
  school = 	 {Technische Universität München},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {},
 note = {{Available on the web} as \url{http://isabelle.in.tum.de/Isar/isar-thesis-Isabelle2002.pdf}}
}
@Book{Williams.mart,
  author =       "David Williams",
  title =        "Probability with Martingales",
  publisher =    "Cambridge University Press",
  year =         "1991",
}
@Article{basrat,
  author = 	 {Andrzej Kondracki},
  title = 	 {Basic Properties of Rational Numbers},
  journal = 	 {Journal of Formalized Mathematics},
  year = 	 {1990},
  OPTkey = 	 {},
  volume = 	 {2},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = {{Available on the web as} \url{http://mizar.uwb.edu.pl/JFM/Vol2/rat_1.html}},
  OPTannote = 	 {}
}
@TECHREPORT{harrison-form,
        author          = "John Harrison",
        title           = "Formalized Mathematics",
        institution     = "Turku Centre for Computer Science (TUCS)",
        OPTaddress         = "Lemminkäisenkatu 14 A, FIN-20520 Turku,
                           Finland",
        year            = 1996,
        type            = "Technical Report",
        number          = 36,
        note            = "{Available on the web as}
 \url{http://www.cl.cam.ac.uk/users/jrh/papers/form-math3.html}"
}
}
@book{ harrison98theorem,
    author = "John Harrison",
    title = "Theorem Proving with the Real Numbers",
    publisher = "Springer",
    year = "1996",
    note            = "{Available on the web as}
 \url{http://citeseer.nj.nec.com/harrison96theorem.html}"
}
@PHDTHESIS{hurd2002,
  AUTHOR = {Joe Hurd},
  TITLE = {Formal Verification of Probabilistic Algorithms},
  SCHOOL = {University of Cambridge},
  YEAR = 2002,
  note = "{Available on the web as} \url{http://www.cl.cam.ac.uk/~jeh1004/research/papers/thesis.html}",
  ABSTRACT = {This thesis shows how probabilistic algorithms can be formally
verified using a mechanical theorem prover.

We begin with an extensive foundational development of probability,
creating a higher-order logic formalization of mathematical measure
theory. This allows the definition of the probability space we use to
model a random bit generator, which informally is a stream of
coin-flips, or technically an infinite sequence of IID Bernoulli(1/2)
random variables.

Probabilistic programs are modelled using the state-transformer monad
familiar from functional programming, where the random bit generator
is passed around in the computation. Functions remove random bits from
the generator to perform their calculation, and then pass back the
changed random bit generator with the result.

Our probability space modelling the random bit generator allows us to
give precise probabilistic specifications of such programs, and then
verify them in the theorem prover.

We also develop technical support designed to expedite verification:
probabilistic quantifiers; a compositional property subsuming
measurability and independence; a probabilistic while loop together
with a formal concept of termination with probability 1. We also
introduce a technique for reducing properties of a probabilistic while
loop to properties of programs that are guaranteed to terminate: these
can then be established using induction and standard methods of
program correctness.

We demonstrate the formal framework with some example probabilistic
programs: sampling algorithms for four probability distributions; some
optimal procedures for generating dice rolls from coin flips; the
symmetric simple random walk. In addition, we verify the Miller-Rabin
primality test, a well-known and commercially used probabilistic
algorithm. Our fundamental perspective allows us to define a version
with strong properties, which we can execute in the logic to prove
compositeness of numbers.}
}
@InProceedings{ijcai85*26,
  author =       "Andrzej Trybulec and Howard Blair",
  title =        "Computer Assisted Reasoning with {MIZAR}",
  pages =        "26--28",
  ISBN =         "0-934613-02-8",
  editor =       "Joshi Aravind",
  booktitle =    "Proceedings of the 9th International Joint Conference
                 on Artificial Intelligence",
  OPTaddress =      "Los Angeles, CA",
  OPTmonth =        aug,
  year =         "1985",
  OPTpublisher =    "Morgan Kaufmann",
}
@Article{mesfunc1,
  author = {Noboru Endou and Katsumi Wasaki and Yasunari Shidama},
  title = {Definitions and Basic Properties of Measurable Functions},
  journal = {Journal of Formalized Mathematics},
  year = 	 {2000},
  OPTkey = 	 {},
  volume = 	 {12},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = {{Available on the web as} \url{http://mizar.uwb.edu.pl/JFM/Vol12/mesfunc1.html}}
}
@Article{mesfunc2,
  author = {Noboru Endou and  Katsumi Wasaki and Yasunari Shidama},
  title = {The Measurability of Extended Real Valued Functions},
  journal = {Journal of Formalized Mathematics},
  year = 	 {2000},
  OPTkey = 	 {},
  volume = 	 {12},
  OPTnumber = 	 {},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  note = {{Available on the web as} \url{http://mizar.uwb.edu.pl/JFM/Vol12/mesfunc2.html}}
}
@misc{ nipkow-isabelles,
  author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
  title = "Isabelle's logics: {HOL}",
  year  = "2002",
  note  = "{Unpublished. Available on the web as} \url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}",
  url = "citeseer.nj.nec.com/nipkow00isabelles.html" 
}
@InCollection{paulson90abs,
  author =       "Lawrence C. Paulson",
  title =        "Isabelle: The Next 700 Theorem Provers",
  booktitle =    "Logic and Computer Science",
  editor =       "Piergiorgio Odifreddi",
  publisher =    "Academic Press",
  pages =        "361--386",
  year =         "1990",
note  = "{Available on the web} as \mbox{\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.pdf}}"
}
@misc{wenzelax,
  author = 	 {Markus Wenzel},
  title = 	 {Using Axiomatic Type Classes in {Isabelle}},
  OPTkey = 	 {},
  OPTmonth = 	 {},
  year = 	 {2002},
  note = {{Unpublished. Available on the web as} \url{http://isabelle.in.tum.de/dist/Isabelle2002/doc/axclass.pdf}}
}
