• Simona Ronchi Della Rocca (Università di Torino)

Title: Intersection types for probabilistic computation

Abstract: Intersection types assignment systems are a powerful tool for proving properties of programs, in the sense that if a program can be typed then it enjoys the property for which the system has been designed. I will focus on the property of termination, both in functional and probabilistic setting. Intersection type assignment systems can supply a complete characterisation of such property, both in a qualitative and quantitative way. In particular, in the probabilistic case, I will show a system characterising both AST (Almost Sure Termination) and PAST (Positive Almost Sure Termination). The system is designed for a call-by-value lambda-calculus, enriched with a probabilistic choice, but all the results are robust and can be applied to the call-by-name calculus too.

• Rineke Verbrugge (University of Groningen)

Title: Zero-one laws for provability logic and its transitive sisters

Abstract: It has been shown in the late 1960s that each formula of first-order logic without constants and function symbols obeys a zero-one law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. Therefore, many properties of models, such as having an even number of elements, cannot be expressed in the language of first-order logic.

For modal logics, limit behavior for models and frames may differ. Halpern and Kapron proved zero-one laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zero-one laws for the corresponding classes of frames, but their zero-one law for K-frames has since been disproved.

In this lecture, I prove zero-one laws for provability logic with respect to both model and frame validity. Moreover, I axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, I use a combinatorial result by Kleitman and Rothschild about the structure of almost all finite partial orders. On the way, I also show that a previous result by Halpern and Kapron about the axiomatization of almost sure frame validity for S4 is not correct, and give pointers as to why a zero-one law for reflexive transitive frames may still hold. Finally, I give some glimpses into my personal history with zero-one laws for modal logics, starting 27 years ago.