Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

References

Abrahamsson, Oskar, and Magnus O. Myreen. 2023. “Fast, Verified Computation for Candle.” In Interactive Theorem Proving (ITP). LIPIcs. https://cakeml.org/itp23.pdf.
Andrews, Peter B. 1986. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Computer Science and Applied Mathematics Series. Academic Press.
Bartle, Robert Gardner. 2001. A Modern Theory of Integration. American Mathematical Soc.
Blanchette, Jasmin Christian, Andrei Popescu, and Dmitriy Traytel. 2014. Cardinals in Isabelle/HOL.” In LNCS 8558 - Interactive Theorem Proving (ITP 2014). Springer. https://doi.org/10.1007/978-3-319-08970-6_8.
Chung, Kai Lai. 2001. A Course in Probability Theory. Third. Academic Press.
Church, Alonzo. 1940. “A Formulation of the Simple Theory of Types.” Journal of Symbolic Logic 5: 56–68.
Coble, Aaron R. 2010. “Anonymity, Information, and Machine-Assisted Proof.” PhD thesis, University of Cambridge.
Feller, William. 2004. An Introduction to Probability Theory and Its Applications. Third. Vol. 1. New York, N.Y.: John Wiley & Sons, Inc.
Fitzpatrick, Patrick, and Halsey Royden. 2010. Real Analysis. 4th ed. Prentice Hall.
Gnedenko, B. V., and A. N. Kolmogorov. 1954. Limit Distributions for Sums of Independent Random Variables. Cambridge, MA: Addison-Wesley Publishing Company, Inc.
Harrison, John. 1998. Theorem-Proving with the Real Numbers. CPHC/BCS Distinguished Dissertations. Springer.
Harrison, John. 2012. The HOL Light Theory of Euclidean Space.” Journal of Automated Reasoning 50 (2): 173–90. https://doi.org/10.1007/s10817-012-9250-9.
Harrison, John. 2017. HOL Light Tutorial. http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf.
Hasan, Osman. 2008. “Formal Probabilistic Analysis Using Theorem Proving.” PhD thesis, Concordia University.
Hurd, Joe. 2002. “Formal Verification of Probabilistic Algorithms.” PhD thesis, University of Cambridge.
Kaufmann, Matt, Panagiotis Manolios, and J Strother Moore. 2000. Computer-Aided Reasoning: An Approach. Vol. 3. Advances in Formal Methods. Boston, MA: Springer. https://doi.org/10.1007/978-1-4615-4449-4.
Kolmogorov, A. N. 1950. Foundations of the Theory of Probability. New York: Chelsea Publishing Company.
Leisenring, A. C. 1969. Mathematical Logic and Hilbert’s ϵ-Symbol. University Mathematical Series. London: Macdonald & Co.  Ltd.
Maranget, Luc. 2008. “Compiling Pattern Matching to Good Decision Trees.” In Proceedings of the 2008 ACM SIGPLAN Workshop on ML, 35–46. ML ’08. New York, NY, USA: ACM. https://doi.org/10.1145/1411304.1411311.
Melham, T. F. 1989. “Automating Recursive Type Definitions in Higher Order Logic.” In Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P. A. Subrahmanyam, 341–86. Springer-Verlag.
Mhamdi, Tarek. 2012. “Information-Theoretic Analysis Using Theorem Proving.” PhD thesis, Concordia University.
Mhamdi, Tarek, Osman Hasan, and Sofiène Tahar. 2011. “Formalization of Entropy Measures in HOL.” In LNCS 6898 - Interactive Theorem Proving (ITP 2011), 233–48. Berlin, Heidelberg: Springer. https://doi.org/10.1007/978-3-642-22863-6_18.
Milner, Robin. 1989. Communication and Concurrency. PHI Series in Computer Science. Prentice-Hall.
Norrish, Michael, and Brian Huffman. 2013. Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω1.” In LNCS 7998 - Interactive Theorem Proving (ITP 2013), 133–46. Springer. https://doi.org/10.1007/978-3-642-39634-2_12.
Paulson, L. 1983. “A Higher-Order Implementation of Rewriting.” Science of Computer Programming 3: 119–49.
Paulson, L. 1987. Logic and Computation: Interactive Proof with Cambridge LCF. Vol. 2. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
Qasim, Muhammad. 2016. “Formalization of Normal Random Variables.” PhD thesis, Montréal, Québec, Canada: Concordia University.
Rosenthal, Jeffrey S. 2006. A First Look at Rigorous Probability Theory. Second. Second Edition. World Scientific Publishing Company.
Sangiorgi, Davide. 2012. Introduction to Bisimulation and Coinduction. Cambridge University Press.
Schilling, René L. 2017. Measures, Integrals and Martingales. Second. Cambridge University Press. https://doi.org/10.1017/9781316718339.
Shiryaev, Albert Nikolaevich. 2016. Probability-1. 3rd ed. Vol. 95. Graduate Texts in Mathematics. New York, NY: Springer-Verlag. https://doi.org/10.1007/978-0-387-72206-1.
Slind, Konrad. 1999. “Reasoning about Terminating Functional Programs.” PhD thesis, Technical University of Munich.