A type theory for probabilistic \(\lambda \)-calculus. (English) Zbl 1440.68043

Di Pierro, Alessandra (ed.) et al., From lambda calculus to cybersecurity through program analysis. Essays dedicated to Chris Hankin on the occasion of his retirement. Cham: Springer. Lect. Notes Comput. Sci. 12065, 86-102 (2020).
Summary: We present a theory of types where formulas may contain a choice constructor. This constructor allows for the selection of a particular type among a finite set of options, each corresponding to a given probabilistic term. We show that this theory induces a type assignment system for the probabilistic \(\lambda \)-calculus introduced in an earlier work by Chris Hankin, Herbert Wiklicky and the author, where probabilistic terms represent probability distributions on classical terms of the simply typed \(\lambda \)-calculus. We prove the soundness of the type assignment with respect to a probabilistic term reduction and a normalization property of the latter.
For the entire collection see [Zbl 1435.68026].


68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus


Full Text: DOI


[1] Abramsky, S., Hankin, C. (eds.): Abstract Interpretation of Declarative Languages. Halsted Press, Sydney (1987)
[2] Abramsky, S., Jensen, T.P.: A relational approach to strictness analysis for higher-order polymorphic functions. In: Proceedings of ACM Symposium on Principles of Programming Languages, pp. 49-54 (1991)
[3] Barbanera, F., Dezani-Ciancaglini, M., de’Liguoro, U.: Intersection and union types: syntax and semantics. Inf. Comput. 119(2), 202-230 (1995). https://doi.org/10.1006/inco.1995.1086. https://dx.doi.org/10.1006/inco.1995.1086 · Zbl 0832.68065
[4] Barendregt, H.P.: The Lambda Calculus, Studies in Logic and the Foundations of Mathematics, vol. 103, revised edn. North-Holland (1991) · Zbl 1159.03304
[5] Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, pp. 117-309. Oxford University Press Inc., New York (1992), http://dl.acm.org/citation.cfm?id=162552.162561
[6] Barendregt, H.: The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103. Elsevier (1984) · Zbl 0551.03007
[7] Cardelli, L., Wegner, P.: On understanding types, data abstraction, and polymorphism. ACM Comput. Surv. 17(4), 471-523 (1985). https://doi.org/10.1145/6041.6042
[8] Castagna, G., Ghelli, G., Longo, G.: A calculus for overloaded functions with subtyping. Inform. Comput. 117(1), 115-135 (1995). https://doi.org/10.1006/inco.1995.1033 · Zbl 0819.03005
[9] Dal Lago, U., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inform. Appl. 46(3), 413-450 (2012) · Zbl 1279.68183
[10] Dezani, M.: Logical semantics for concurrent lambda calculus, ph.D. Thesis, Radboud University Nijmegen (1996)
[11] Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic lambda-calculus and quantitative program analysis. J. Logic Comput. 15(2), 159-179 (2005) · Zbl 1070.03008
[12] Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. LOPSTR 2000. LNCS, vol. 2042, pp. 147-164. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45142-0_9 · Zbl 1018.68505
[13] Draheim, D.: Semantics of the Probabilistic Typed Lambda Calculus - Markov Chain Semantics, Termination Behavior, and Denotational Semantics. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-642-55198-7 · Zbl 1439.03005
[14] Girard, J.Y.: Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In: Proceedings of the 2nd Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol. 63, pp. 63-92. North-Holland (1971) · Zbl 0221.02013
[15] Gunter, C.A.: Foundations of Computing. MIT Press, Cambridge (1992)
[16] Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Functional characters of solvable terms. Math. Logic Q. 27(2-6), 45-58 (1981) · Zbl 0479.03006
[17] Park, S.: A calculus for probabilistic languages. In: Proceedings of the ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 38-49. ACM (2003)
[18] Park, S., Pfenning, F., Thrun, S.: A monadic probabilistic language (2003). manuscript. http://www.cs.cmu.edu/ fp/papers/prob03.pdf · Zbl 1369.68083
[19] Park, S., Pfenning, F., Thrun, S.: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1), 4:1-4:46 (2008). https://doi.org/10.1145/1452044.1452048. https://doi.acm.org/10.1145/1452044.1452048 · Zbl 1369.68083
[20] Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002) · Zbl 0995.68018
[21] Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. Theor. Comput. Sci. 1(2), 125-159 (1975) · Zbl 0325.68006
[22] Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223-255 (1977) · Zbl 0369.68006
[23] Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of ACM Symposium on Principles of Programming Languages, pp. 154-165. ACM Press (2002) · Zbl 1323.68150
[24] Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19, pp. 408-425. Springer, Heidelberg (1974). https://doi.org/10.1007/3-540-06859-7_148
[25] Roman, S.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.