Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case

DOI
Publisher DOI
Abstract
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.
Date Issued
2020-01-03
Publication Type
Conference Item
Subject(s)
Language(s)
en
Author(s)
Ghilezan, Silvia
Ivetic, Jelena
Kasterovic, Simona
Ognjanovic, Zoran
Editor(s)
Herzig, Andreas
Kontinen, Juha
Additional Credits
Publisher
Springer
ISBN
978-3-030-39950-4
Title of Event
Access(Rights)
restricted
Show full item