BREUVART , Flavien

We define two intersection type systems for the pure, un-typed, probabilistic λ-calculus, and prove that type derivations precisely reflect the probability of convergence of the underlying term. We first define a simple system of oracle intersection types in which derivations are annotated by binary strings and the probability of termination...

We study the expressive power of subrecursive probabilistic higher-order calculi. More specifically, we show that endowing a very expressive deterministic calculus like Gödel's T with various forms of probabilistic choice operators may result in calculi which are not equivalent as for the class of distributions they give rise to, although they...

Working in the untyped lambda calculus, we study Morris's λ-theory H +. Introduced in 1968, this is the original extensional theory of contextual equivalence. On the syntactic side, we show that this λ-theory validates the ω-rule, thus settling a long-standing open problem. On the semantic side, we provide sufficient and necessary conditions...