C. D. Manning and H. Schütze, Foundations of statistical natural language processing, 2001.

J. Pearl, Probabilistic reasoning in intelligent systems -networks of plausible inference, ser. Morgan Kaufmann series in representation and reasoning, 1989.

S. Thrun, Exploring artificial intelligence in the new millennium, vol.1, p.1, 2002.

K. De-leeuw, E. F. Moore, C. E. Shannon, and N. Shapiro, Computability by probabilistic machines, Automata Studies, vol.34, pp.183-198, 1956.

R. Motwani and P. Raghavan, Randomized algorithms, 1995.

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, Proc. of 36 th POPL, pp.90-101, 2009.

G. Barthe, B. Grégoire, S. Heraud, and S. Zanella-béguelin, Computeraided security proofs for the working cryptographer, Proc. of 31 st CRYPTO, ser. LNCS, vol.6841, pp.71-90, 2011.
URL : https://hal.archives-ouvertes.fr/hal-01112075

N. D. Goodman, V. K. Mansinghka, D. Roy, K. Bonawitz, and J. B. Tenenbaum, Church: A language for generative models, Proc. of 24 th UAI, pp.220-229, 2008.

D. Tolpin, J. Van-de-meent, and F. Wood, Probabilistic programming in Anglican, Machine Learning and Knowledge Discovery in Databases, ser. LNCS, vol.9286, pp.308-311, 2015.

M. O. Rabin, Probabilistic algorithm for testing primality, Journal of Number Theory, vol.12, issue.1, pp.128-138, 1980.

M. Agrawal, N. Kayal, and N. Saxena, Annals of Mathematics, vol.160, issue.2, pp.781-793, 2004.

K. Chatterjee, P. Novotný, and D. Zikelic, Stochastic invariants for probabilistic termination, Proc. of 44 th POPL, pp.145-160, 2017.

B. L. Kaminski, J. Katoen, C. Matheja, and F. Olmedo, Weakest precondition reasoning for expected run-times of probabilistic programs, Proc. of 25 th ESOP, ser. LNCS, vol.9632, pp.364-389, 2016.

S. Jost, K. Hammond, H. Loidl, and M. Hofmann, Static determination of quantitative resource usage for higher-order programs, Proc. of 37 th POPL, pp.223-236, 2010.

M. Avanzini, U. D. Lago, and A. Yamada, On probabilistic term rewriting, Proc. of 14 th FLOPS, ser. LNCS, vol.10818, pp.132-148, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926502

M. Hofmann and S. Jost, Type-based amortised heap-space analysis, Proc. of 15 th ESOP, ser. LNCS, vol.3924, pp.22-37, 2006.

U. Lago and M. Gaboardi, Linear dependent types and relative completeness, LMCS, vol.8, issue.4, pp.1-44, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00906347

U. Lago and C. Grellois, Probabilistic termination by monadic affine sized typing, Proc. of 26 th ESOP, ser. LNCS, vol.10201, pp.393-419, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01635077

F. Breuvart and U. Lago, On intersection types and probabilistic lambda calculi, Proc. of 20 th PPDP, vol.8, pp.1-8, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01926420

F. Mosteller, Fifty challenging problems in probability with solutions. Courier Corporation, 1987.

M. Mitzenmacher and E. , Probability and computing: Randomized algorithms and probabilistic analysis, 2005.

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proc. of 23 rd POPL, pp.410-423, 1996.

H. Barendregt, M. Coppo, and M. Dezani-ciancaglini, A filter lambda model and the completeness of type assignment, The Journal of Symbolic Logic, vol.48, issue.4, pp.931-940, 1983.

D. D. Carvalho, Execution time of lambda-terms via denotational semantics and intersection types, Mathematical Structures in Computer Science, vol.28, issue.7, pp.1169-1203, 2018.
URL : https://hal.archives-ouvertes.fr/inria-00319822

U. Lago and P. Parisen-toldin, A higher-order characterization of probabilistic polynomial time, Revised Selected Papers of 2 nd FOPARA, ser. LNCS, vol.7177, pp.1-18, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00909376

O. Bournez and C. Kirchner, Probabilistic Rewrite Strategies. Applications to ELAN, Proc. of 13 th RTA, ser. LNCS, vol.2378, pp.252-266, 2002.
URL : https://hal.archives-ouvertes.fr/inria-00100883

J. Esparza, A. Gaiser, and S. Kiefer, Proving termination of probabilistic programs using patterns, Proc. of 24 th CAV, ser. LNCS, vol.7358, pp.123-138, 2012.

F. Ferrer, L. María, and H. Hermanns, Probabilistic termination: Soundness, completeness, and compositionality, Proc. of 42 nd POPL, pp.489-501, 2015.

K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs, Proc. of 43 rd POPL, pp.327-342, 2016.

K. Chatterjee, H. Fu, and A. K. Goharshady, Termination analysis of probabilistic programs through Positivstellensatz's, Proc. of 28 th CAV, ser. LNCS, vol.9779, pp.3-22, 2016.

K. Chatterjee, H. Fu, and A. Murhekar, Automated recurrence analysis for almost-linear expected-runtime bounds, Proc. of 29 th CAV, ser. LNCS, vol.10426, pp.118-139, 2017.

V. C. Ngo, Q. Carbonneaux, and J. Hoffmann, Bounded expectations: Resource analysis for probabilistic programs, Proc. of 39 th PLDI, pp.496-512, 2018.

T. Freeman and F. Pfenning, Refinement types for ML, Proc. of 12 th PLDI, pp.268-277, 1991.

G. Barthe, M. Gaboardi, E. J. Arias, J. Hsu, A. Roth et al., Higher-order approximate relational refinement types for mechanism design and differential privacy, Proc. of 42 nd POPL, vol.50, pp.55-68, 2015.

C. A. Hoare, Quicksort, The Computer Journal, vol.5, issue.1, pp.10-16, 1962.

T. , Lectures on the Coupling Method, ser, 2002.

A. Chakarov and S. Sankaranarayanan, Probabilistic Program Analysis with Martingales, Proc. of 25 th CAV, ser. LNCS, vol.8044, pp.511-526, 2013.

G. D. Plotkin, LCF Considered as a Programming Language, TCS, vol.5, issue.3, pp.223-255, 1977.

A. Sabry and M. Felleisen, Reasoning about programs in continuationpassing style, Lisp and symbolic computation, vol.6, pp.289-360, 1993.

A. G. Avanzini and U. Lago, Type-Based Complexity Analysis of Probabilistic Functional Programs, Tech. Rep, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02103943

G. Barthe, B. Grégoire, J. Hsu, and P. Strub, Coupling proofs are probabilistic product programs, Proc. of 44 th POPL, pp.161-174, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01649028