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.