This may happen on the first request due to CSS mimetype issues. Try clearing your browser cache and refreshing.

@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}} }