Reasoning with uncertainty has gained an important role in logic, computer science, artificial intelligence and cognitive science. There has been a growing interest in probabilistic reasoning about proofs and programs. These applications urge for development of formal models which capture reasoning with probabilistic features. We discuss and develop means of probabilistic logic within lambda calculus with types.
We propose a formal model for reasoning about probabilities of typed lambda terms, which is a combination of lambda calculus and probabilistic logic. We present its syntax, Kripke-style semantics and axiomatic system. We then prove the soundness and strong completeness, which rely on two key facts: the completeness of the type assignment and the existence of the maximal consistent extension of a consistent set.
This is joint work with Zoran Ognjanovic, Jelena Ivetic, Nenad Savic and Simona Kasterovic.