Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case

Ghilezan, Silvia; Ivetic, Jelena; Kasterovic, Simona; Ognjanovic, Zoran; Savic, Nenad (3 January 2020). Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case. In: Herzig, Andreas; Kontinen, Juha (eds.) Foundations of Information and Knowledge Systems. Lecture Notes in Computer Science: Vol. 12012 (pp. 122-139). Springer 10.1007/978-3-030-39951-1_8

Text GIKOS_FoIKS2020.pdf - Published Version Restricted to registered users only Available under License Publisher holds Copyright. Download (385kB)

The development of different probabilistic models of uncertainty has been inspired by the rapid progress in various fields, e.g. in AI, probabilistic programming, etc. Lambda calculus is a universal model of computation suitable to express programming languages concepts. Hence, different methods for probabilistic reasoning in lambda calculus have been investigated. In this paper, we develop a formal model for probabilistic reasoning about lambda terms with intersection types, which is a combination of lambda calculus and probabilistic logic. The language of lambda calculus with intersection types is endowed with a probabilistic operator. We propose a semantics based on the possible world approach. An infinitary axiomatization is given for this system and it is proved to be sound with respect to the proposed semantics.

Interest & Impact

Downloads

3 since deposited on 20 Apr 2020
0 in the past 12 months

Citations

5 Citations in Web of Science ®
6 Citations in Scopus

Search

in Google Scholar™

Services

Actions (login required)

Edit item

Actions (login required)

Edit item