Rencontre, 17 mai 2018

Programme

10:30 – 12:00

Tarmo Uustalu (Reykjavik University and Tallinn Univ. of Technology)

Invited talk: A Coalgebraic View of Bar Recursion and Bar Induction

We reformulate the bar recursion and induction principles in terms of recursive and wellfounded coalgebras. Bar induction was originally proposed by Brouwer as an axiom to recover certain classically valid theorems in a constructive setting. It is a form of induction on non-wellfounded trees satisfying certain properties. Bar recursion, introduced later by Spector, is the corresponding function definition principle.

We give a generalization of these principles, by introducing the notion of barred coalgebra: a process with a branching behaviour given by a functor, such that all possible computations terminate.

Coalgebraic bar recursion is the statement that every barred coalgebra is recursive; a recursive coalgebra is one that allows definition of functions by a coalgebra-to-algebra morphism. One application of this principle is tabulation of continuous functions: Ghani, Hancock and Pattinson defined a type of wellfounded trees that represent continuous functions on streams. Bar recursion allows us to prove that every stably continuous function can be tabulated to such a tree, where by stability we mean that the modulus of continuity is its own modulus.

Coalgebraic bar induction states that every barred coalgebra is wellfounded; a wellfounded coalgebra is one that admits proof by a form of induction.

This is joint work with Venanzio Capretta, University of Nottingham, published in Proc. of FoSSaCS 2016. Time permitting, I might also discuss our related ongoing work.

14:00 – 15:00

Florian Faissole (LRI)

Invited talk: Synthetic topology in homotopy type theory for probabilistic programming

The ALEA Coq library formalizes discrete measure theory using a variant of the Giry monad, as a submonad of the CPS monad: (A -> [0,1]) -> [0,1]. This allows one to use Moggi's monadic meta-language to give an interpretation of a language, Rml, into type theory. Rml is a functional language with a primitive for probabilistic choice. This formalization was the semantical basis for the Certicrypt system for verifying security protocols. We improve on the formalization by using homotopy type theory which provides e.g. quotients and functional extensionality. Moreover, homotopy type theory allows us to use synthetic topology to present a theory which also includes "continuous" data types, like [0,1]. We also get a constructive formalization of probabilistic programming.

15:30 – 16:30

Luca Padovani (Università di Torino)

Invited talk: Mailbox Types for Unordered Interactions

We present a behavioral type system for reasoning on protocol conformance in networks of processes that communicate through unordered mailboxes. This communication model is the one adopted by concurrent objects and actors.

In sharp contrast with other behavioral types (session types in particular), the type of a mailbox specifies which patterns of messages are supposed to be stored in - or retrieved from - a mailbox, but not in which order. This allows the description of mailboxes concurrently accessed by several processes, abstracting away from the state and behavior of the processes using them.

There seem to be analogies between mailbox types and linear logic formulas, as well as between the typing rules and the proof rules of classical linear logic. With this seminar we seek to initiate a deeper investigation of these analogies.