Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

Semantics of proofs and programs

Dates and location

From June 10 to June 13, at Institut Henri Poincaré.

Presentation

This workshop is focussed on mathematical models of programs and proofs, using concepts and tools coming from:

  • linear logic and it extensions or restrictions,
  • (synthetic) domain theory,
  • category theory,
  • higher dimensional algebra and rewriting
  • game semantics,
  • linear algebra,
  • probabilities,
  • operads
  • topology etc.

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

  • non-deterministic and/or probabilistic computations
  • (local) states
  • (delimited) continuations and classical logical systems
  • concurrency and mobility
  • quantum computations

Speakers

  • Samson Abramsky: Game and Coherence Semantics for Linear Dependent Types
  • Richard Blute: Homological structures arising in differential linear logic
  • Alberto Carraro: Thirty years of questions about ordered models of lambda calculus
  • Pierre Clairambault: Concurrent Hyland-Ong Games
  • Ugo Dal Lago: On bisimulation relations for probabilistic higher-order functional programs
  • Martin Escardo: Continuity in type theory
  • Marcelo Fiore: Algebraic Theories and Control Effects, Back and Forth
  • Jean Goubault-Larrecq: The Read-Once Tape Monad
  • Alexis Goyet: Building simple languages with the power of references
  • Martin Hyland: Propositions as Types as a perspective on Proof Theory
  • Guy McCusker: Relational semantics and game semantics
  • Rasmus Ejlers Mogelberg: Guarded recursion in type theory
  • Paul-André Melliès: Tensorial logic with algebraic effects
  • Michele Pagani: Quantitative semantics for higher-order probabilistic computation
  • Gordon Plotkin: The algebraic theory of effects
  • Giuseppe Rosolini: Equivocal Frames
  • Sam Staton: Parameterized algebraic theories and notions of computation
  • Thomas Streicher: Computability in Basic Quantum Theory
  • Nikos Tzevelekos: Nominal game semantics and automata

Programme

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

Abstracts

Richard Blute

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.

Alberto Carraro

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:

  • whether for every consistent lambda-theory T, there exists a model in S whose theory is T;
  • whether any two lambda-terms equal in all models of S are beta-convertible (equational completeness).

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.

Pierre Clairambault

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.

Ugo Dal Lago

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.

Alexis Goyet

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.

Jean Goubault-Larrecq

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.

Martin Hyland

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.

Paul-André Melliès

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.

Rasmus Ejlers Mogelberg

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.

Michele Pagani

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.

Giuseppe Rosolini

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.

Thomas Streicher

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.

Nikos Tzevelekos

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.

Organizers

workshop_3.txt · Last modified: 2014/06/05 10:11 by mellies
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0