General programme
30 January – 3 February: Complexity
The theme of this week is the logical approach to logical complexity. The last decade has seen the development of logical formalisms derived from linear logic that characterize functions computable in various complexity classes (polynomial or elementary in time, logarithmic in space) in an implicit way, that is to say by contruction of the languages instead of using explicit measures. The theory that underlies these formalisms naturally meets the more established tradition of studying the complexity of algorithmic problems from logic (satisfiability, constraints solving, etc). The goal of this week is to survey the various aspects of the theory of algorithmic complexity where these communities meet, so as to trigger new interactions and enrich the various approaches.
6 – 10 February: Logic and interaction
This week is dedicated to the theme of interactive approaches of logic: models and fameworks in which the fundamental mechanism is that of a dialog between proofs and counter-proofs. Areas of interest notably include the Geometry of interaction programme, aiming at a reconstruction of logic from interaction as the primitive notion, considered as an abstract counterpart of cut elimination; the study of mathematical structures that represent dialog processes (game semantics, ludics), including recent developments at the boundary between mathematical logic and linguistics.
13 – 17 February: Proofs and programs
The theme of this week is the correspondence between mathematical proofs and computer programs, known as the Curry-Howard correspondence. It notably includes the latest developments the theory of realizability, which can give computational content to proofs in classical logic, so as to allow the extraction of effective programs from classical proofs. In contrast to the previous week (logic and interaction), this week will focus on the study of logical aspects of non-functional programming: delimited continuations, references, effects, etc.
20 – 24 February: Quantitative approaches
This week aims to bring together the different approaches that extend the classical correspondence between proofs and programs to models where a quantitative aspect is significant. From the computer science perspective, the two mainly concerned areas are quantum computing and stochastic systems, approached in particular through algebraic extensions of the λ-calculus. On the logical side, topics of interest mainly involve differential linear logic and related quantitative denotational models.
27 February – 2 March: Algebra and computation
This week deals with interactions between algebraic combinatorics and rewriting theory: algebraic invariants in computation, relating homological and algorithmic properties of rewriting systems, and the use of rewriting in algebraic combinatorics, offering effective computation and proof techniques. Themes of interest includes the use of ordered structures (lattices, event structures, directed homotopy) in logic and concurrency theory, as well as recent work on interpretations of type theory in homotopy.