Registration
From June 10 to June 13, at Institut Henri Poincaré.
This workshop is focussed on mathematical models of programs and proofs, using concepts and tools coming from:
A particular attention will be devoted to the relations between denotational and operational properties of programs and proofs and to possible applications of mathematical models to certification problems.
Various extensions of the ordinary functional settings will be considered, such as
Tuesday 10 June | ||
---|---|---|
10h00 - 10h45 | Registration | |
10h45 - 11h00 | T. Ehrhard, A. Simpson | Introduction |
11h00 - 12h00 | Marcelo Fiore | Algebraic Theories and Control Effects, Back and Forth |
12h00 - 14h00 | Free lunch | |
14h00 - 15h00 | Sam Staton | Parameterized algebraic theories and notions of computation |
15h00 - 16h00 | Pierre Clairambault | Concurrent Hyland-Ong Games |
16h00 - 16h30 | Coffee break | |
16h30 - 17h30 | Paul-André Melliès | Tensorial logic with algebraic effects |
Wednesday 11 June | ||
9h30 - 10h30 | Jean Goubault-Larrecq | The Read-Once Tape Monad |
10h30 - 11h00 | Coffee break | |
11h00 - 12h00 | Michele Pagani | Quantitative semantics for higher-order probabilistic computation |
12h00 - 14h00 | Free lunch | |
14h00 - 15h00 | Alexis Goyet | Building simple languages with the power of references |
15h00 - 16h00 | Guy McCusker | Relational semantics and game semantics |
16h00 - 16h30 | Coffee break | |
16h30 - 17h30 | Ugo Dal Lago | On bisimulation relations for probabilistic higher-order functional programs |
Thursday 12 June | ||
9h30 - 10h30 | Martin Escardo | Continuity in type theory |
10h30 - 11h00 | Coffee break | |
11h00 - 12h00 | Martin Hyland | Propositions as Types as a perspective on Proof Theory |
12h00 - 14h00 | Free lunch | |
14h00 - 15h00 | Thomas Streicher | Computability in Basic Quantum Theory |
15h00 - 16h00 | Nikos Tzevelekos | Nominal game semantics and automata |
16h00 - 16h30 | Coffee break | |
16h30 - 17h30 | Gordon Plotkin | The algebraic theory of effects |
18h30 | Coktail at IHP | |
Friday 13 June | ||
9h30 - 10h30 | Samson Abramsky | Game and Coherence Semantics for Linear Dependent Types |
10h30 - 11h00 | Coffee break | |
11h00 - 12h00 | Alberto Carraro | Thirty years of questions about ordered models of lambda calculus |
12h00 - 14h00 | Free lunch | |
14h00 - 15h00 | Rasmus Ejlers Mogelberg | Guarded recursion in type theory |
15h00 - 16h00 | Giuseppe Rosolini | Equivocal Frames |
16h00 - 16h30 | Coffee break | |
16h30 - 17h30 | Richard Blute | Homological structures arising in differential linear logic |
Homological algebra is a branch of mathematics which explores the interplay between algebraic and topological structures. It has been used in such fields as algebraic topology, group theory and algebraic geometry. We argue here that the structures present in models of differential linear logic are rich enough that several different notions of homological algebra can be abstracted in this setting.
The differential structure allows one to define Kahler differentials, which are a generalization of de Rham cohomology to more algebraic settings. The coassociative coalgebra structure allows for the definition of a dualized Hochschild cohomology and finally the exponential comonad can be used to define several versions of the cotriple cohomology introduced by Barr and Beck.
We introduce these various theories and explore their relationships.
After the construction of the first model of lambda-calculus by Dana Scott, a large number of mathematical models have been introduced in different categories of domains and have been classified into semantics (continuous semantics, stable semantics, strongly stable semantics, …). Some natural problems then arise for a given semantics S of lambda-calculus:
The equational completeness problem for Scott continuous semantics is one of most outstanding open problems of lambda-calculus, appeared in print over twenty years ago. This line of research produced many interesting related questions, like Plotkin-Selinger's order incompleteness problem and Honsell-Plotkin's equational consistency problem. We present these problems and some partial answers, among which the solution of an open problem of the TLCA list.
Recently, Rideau and Winskel described a (bi-)category of non-deterministic concurrent strategies playing on event structures. In this talk I will describe recent advances on how this category can serve as a basis for the game semantics of programming languages. Firstly, I will present an affine category of concurrent games, and describe in it the interpretation of an affine version of Parallel Idealized Algol. Then I will introduce an extension with a notion of symmetry, allowing to express the uniform duplication of events. In this setting I will desribe a concurrent analogue of the plays with pointers of Hyland-Ong games, and revisit the notions of P-visibility and innocence.
Various notions of bisimulation for higher-order functional programs have been introduced in the last twenty years, including applicative, normal form and environmental bisimulations. All of them have been shown to be sound for observational equivalence, both when deterministic and when nondeterministic calculi are considered. We show how some of these coinductive techniques can be applied to probabilistic functional programs in the form of pure, untyped, lambda-terms endowed with binary probabilistic choice. More specifically, we introduce a form of probabilistic applicative bisimulation, following Larsen and Skou, and give some surprising results about full-abstraction. We conclude by hinting at how the approach can be extended to complexity-bounded as well as quantum functional programs.
The aim of the lambda lambda-bar calculus is to represent as faithfully as possible the structure of non-deterministic, non-innocent, non-visible strategies in game semantics. Non-innocent strategies are known to model functional languages extended with references. The typical approach is to model the purely functional fragment with innocent strategies, to which a “memory-cell” strategy is added. Instead, our starting point is a simple concrete syntax of finite strategies, which are inherently non-innocent.
This approach is syntax driven, and the resulting language is a dualization of the lambda calculus. A new binder, the lambda-bar, names arguments which have been passed to the environment (whereas the lambda names arguments which have been received). This makes explicit the act of answering a function call, and allows this answer to change over time, granting the power of general states.
This syntax can then be used to build languages which are simple – i.e. for which interesting properties are decidable – while still allowing for the power of references. We do so by proceeding from the ground up, starting with very simple fragments of the lambda lambda-bar calculus. The duality of the general calculus allows us to give syntactic restrictions which apply uniformly to the Player and Opponent moves, and more directly affect the ability of the strategy to have “complex” behavior. An example of a simple behavior is one that only uses a bounded amount of memory; this can be obtained by checking, syntactically, that only a finite amount of names is needed (after garbage collection). This situation does not occur for any non-trivial innocent interaction; however it does for “pseudo-normal” terms of the calculus.
The domain-theoretic foundations of probabilistic choice have proved to conceal many a pitfall. As one of the latest instances, in 2011 I proposed to replace the Jones-Plotkin probabilistic powerdomain monad by the so-called continuous random variable monad… which Mike Mislove discovered was not a monad after all, in 2013. I'll describe another monad that does what the continuous random variable `monad' should have been from the very start. What it models is the domain-theoretic counterpart of a classic way of modeling random choice on Turing machines, by keeping a special read-only tape of pre-chosen random bits, restricted so that you can read each bit only once. The read-once tape monad retains many nice properties of the continuous random variable construction, notably that it preserves bc-domains… and it really is a strong monad. This also sheds light on what mistake I made in 2011: the ordering was wrong; replacing it by one that compares fewer elements (although in a rather counter-intuitive way) yields back the read-once tape construction.
The established reading of propositions as types is as a link between proof and computation encapsulated in the Curry-Howard correspondence of Type Theory and realised in proof assistants such as Coq. This link has also driven work in Linear Logic and the Geometry of Interaction and in Deep Inference. The unifying perspective of Categorical Proof Theory provides a challenging discipline to this wide range of work. I want to promote the idea that this perspective should be applied also within the proof theoretic tradition of functional interpretations. I shall give examples of taking propositions as types seriously in a range of such cases.
Tensorial logic is a primitive logic of tensor and negation which refines linear logic by relaxing the hypothesis that negation is involutive. One reason for introducing the logic is that its proof-nets coincide with innocent strategies between dialogue games. In this talk, we explain how to extend tensorial logic with various notions of algebraic effects. We then illustrate that principle by characterizing the notion of tensorial proof-net associated to various notions of effects, including nondeterminism, global states and local states.
We study extensions of type theory with guarded recursive types, i.e., recursively defined types in which the recursion variable only appears underneath a modal operator. One motivation for studying these type theories is that the guarded recursive types can be used to construct models of programming languages with advanced notions of state, which can be seen as synthetic variants of models constructed using step-indexing techniques, but unlike these offer a type system for expressing the model constructions. Guarded recursive variants of coinductive types have also been suggested as a way of building expressing productivity requirements of coinductive definitions using types.
In the talk I will describe the topos-of-trees model of guarded recursion and, if time permits, I’ll discuss intensional models of guarded recursion and relations between guarded recursive types and coinductive types.
Various models of Linear Logic have been defined in categories of vector spaces (more generally modules) and linear functions. These models provide semantics of quite expressive functional programming languages, where programs using their inputs exactly once correspond to linear functions and programs using their inputs an arbitrary number of times (like recursive programs) correspond to power series.
Quantitative semantics are particularly suitable for interpreting non-deterministic computations, such as probabilistic and quantum algorithms. The addition between vectors expresses a kind of superposition of atomic states and the scalars a quantitative estimation of this superposition.
In this talk I will introduce to the main ideas of quantitative semantics and I will present the most recent results achieved in the framework of higher-order probabilistic computation.
We consider the locally cartesian closed category Equ of equilogical spaces, which is a full conservative extension of the category of T0-spaces, and present a double-exponential monad on it that provides an algebraic presentation of the category of frames.
Work of A. Simpson and M. Schroeder has given rise to an intrinisc definition of those spaces for which “admissible representations” exist in the sense of Weihrauch's type 2 effectivity. This way they appear as a small full reflective subcategory of the function realizability topos and of its full subcategory of assemblies which gives rise to a model of the Inductive Calculus of Constructions. By a theorem of Schroeder spaces with admissible representations appear as those types which are double negation closed subobjects of powers of the Sierpinski space $\Sigma$. The corresponding full subcategory we call AdmRep. Since the latter contains $\Sigma$ and separable infinite dimensional Hilbert space the Hilbert lattice admits an admissible representation. We show that states and observables as defined from the Hilbert lattice also live within AdmRep and discuss how they correspond to their functional analytic analogues.
Names appear in computational scenarios where entities of specific kinds can be created at will and in such a manner that newly created entities are always fresh, i.e. distinct from any other created before. For example, references, objects and exceptions in languages like ML or Java can be seen as names. The behaviour of languages which feature names is in general very subtle due to issues of privacy, visibility and flow of names, and the ensuing notion of local state.
This talk is about formal reasoning techniques for programs with names which have emerged in the last years. We will in particular focus on the “nominal” strand of game semantics, which has so far contributed fully abstract models for a variety of fragments of ML and an imperative fragment of Java. We moreover see how these models can be given algorithmic representations by means of abstract machines operating on infinite alphabets of names.