Probabilistic reasoning about simply typed lambda terms

Abstract

Reasoning with uncertainty has gained an important role in computer science, artificial intelligence and cognitive science. These applications urge for development of formal models which capture reasoning of probabilistic features. We propose a formal model for reasoning about probabilities of simply typed lambda terms. We present its syntax, Kripke-style semantics and axiomatic system. The main results are the corresponding soundness and strong completeness, which rely on two key facts: the completeness of simple type assignment and the existence of a maximal consistent extension of a consistent set.