### Computer Science Special Session

**Sylvain Schmitz:
Well-quasi-orders in Logic
**
Well-quasi-orders are a versatile tool for proving expressivity and decidability results. The talk will provide a glimpse of their applications in logic, through examples from proof theory, finite model theory, and verification.

**Ana Sokolova:
Semantics for Probability and Nondeterminism via Coalgebra
**
In this talk I will introduce the very basics of coalgebra, and show you how different semantics
(bisimilarity, convex bisimilarity, distribution bisimilarity, trace semantics) for systems with
probability and nondeterminism elegantly fit in the theory of coalgebra.

**
Niki Vazou: Liquid Haskell:
Theorem Proving for All
**
Formal verification has been gaining the attention and resources of both the academic and the industrial world since it prevents critical software bugs that cost money, energy, time, and even lives. Yet, software development and formal verification are decoupled, requiring verification experts to prove properties of a template – instead of the actual – implementation ported into verification specific languages. Niki's goal is to bridge formal verification and software development for the programming language Haskell. Haskell is a unique programming language in that it is a general purpose, a functional language used for industrial development, but simultaneously it stands at the leading edge of research and teaching welcoming new, experimental, yet useful features. In this talk, Niki is presenting Liquid Haskell, a refinement type checker in which formal specifications are expressed as a combination of Haskell’s types and expressions and are automatically checked against real Haskell code. This natural integration of specifications in the language, combined with automatic checking, established Liquid Haskell as a usable verifier, enthusiastically accepted by both industrial and academic Haskell users. Recently, Niki turned Liquid Haskell into a theorem prover, in which arbitrary theorems about Haskell functions would be proved within the language. As a consequence, Liquid Haskell can be used to prove theorems about Haskell functions by all Haskell programmers.