Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

This is an old revision of the document!


Lectures

Wednesday 23 April
14h-15hGérard BerryConstructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification
15h30-16h30Gérard BerryConstructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification
Thursday 24 April
14h-15hJean-Yves GirardQu'est-ce qu'une réponse ? (l'analytique)
15h30-16h30Gérard BerryConstructive semantics, electricity propagation in circuits, 2-adic numbers, and formal verification
Friday 25 April
14h-15hJean-Yves GirardQu'est-ce qu'une question ? (le format)
15h30-16h30Jean-Yves GirardD'où vient la certitude ? (l’épidictique)
Monday 28 April
11h-12hPer Martin-LöfDependence and Causality
Tuesday 29 April
10h30-12hThorsten AltenkirchTowards a Syntax for Cubical Type Theory
14h-15h30François PottierThe practice and theory of Mezzo
16h-17h30Jean-Louis Krivine50 ans après le forcing, la correspondance de Curry-Howard donne de nouveaux modèles de ZF
Wednesday 30 April
10h30-12hJean-Louis Krivine50 ans après le forcing, la correspondance de Curry-Howard donne de nouveaux modèles de ZF
14h00-15h30Thorsten AltenkirchTowards a Syntax for Cubical Type Theory
16h00-17h30François PottierThe practice and theory of Mezzo
Monday 26 May
17h00-18h00Timothy Gowers Fully automatic problem solving with human-style output
Tuesday 27 May
14h00-15h00Bruno Vallette Théorie de la déformation des algèbres de Batalin—Vilkovisky
Wednesday 28 May
14h00-15h00Bruno Vallette Théorie de la déformation des algèbres de Batalin—Vilkovisky
Monday 16 June
11h00-12h30Olivier Serre Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs slides of the first lecture
Wednesday 18 June
10h30-12h00Olivier Serre Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs slides of the second lecture
Thursday 19 June
10h30-12h00Marc Pouzet Synchronous Languages and their extension to mix discrete and continuous time slides of the first lecture part Apart B
Friday 20 June
10h30-12hMarc Pouzet Synchronous Languages and their extension to mix discrete and continuous time
14h00-15h00Thomas Streicher A Model of Control Operators in Coherence Spaces giving rise to a New Model of Classical Set Theory

Abstracts

Thorsten Altenkirch
Towards a syntax for cubical type theory

One of the key problems of Homotopy Type Theory is that it introduces axioms such as extensionality and univalence for which there is no known computational interpretation. We propose to overcome this by introducing a Type Theory where a heterogenous equality is defined recursively and equality for the universe just is univalence. This cubical type theory is inspired by Bernardy and Moulin's internal parametricity and by Coquand, Bezem and Huber's cubical set model. This is ongoing work with Ambrus Kaposi at Nottingham.

Timothy Gowers (University of Cambridge)
Fully automatic problem solving with human-style output

I shall describe a program that Mohan Ganesalingam and I created that proves simple statements in elementary abstract analysis. I shall also discuss the broader project of which this is intended to be just a preliminary step. Briefly, the aim is to write a series of programs that solve problems in a “fully human” way, meaning that they do not undertake any search that a human mathematician would not consider undertaking. At first, this seems to be sacrificing everything that makes a computer worth using. However, I shall attempt to explain why we regard this view as mistaken.

Jean-Louis Krivine
50 years after forcing, Curry-Howard correspondence gives new models of ZF

Classical realizability appeared as a method to extend the proof-program correspondence to the whole of ZF set theory, even with DC (dependent choice). As a by-product, it gives completely new models of ZF + DC, that we shall consider in these talks. The method of forcing is indeed a (very) particular case, that we shall avoid, of course.

The principal tools are :

i) A conservative extension of ZF, called ZF_epsilon, with a new strong membership relation, which does not satisfy extensionality.

ii) The structure of realizability algebra, which is a three-sorted extension of the well known combinatory algebra of Curry.
The ordered sets of conditions, used in forcing, are degenerate cases of realizability algebras. he usual models of lambda-calculus (stable spaces, hypercoherence spaces, …) are examples of realizability algebras.

The models of ZF obtained in this way are much more difficult to study than the ordinary forcing models: they are not extensions of the ground model, ordinals and even integers are not preserved and neither is the axiom of choice. I shall explain what we already know about their structure. We shall look at some examples, which give some new relative consistency results, with DC and R not well ordered.

Up to now, there are few such new results, even though the method is much more general than forcing. The reason is, of course, that we do not yet understand sufficiently well the structure of these models.

François Pottier
The practice and theory of Mezzo

The programming language Mezzo is a member of the ML family, from whom it inherits algebraic data types, first-class functions, and automatic memory management. It is equipped with a rich type system that controls aliasing and access to mutable memory. This static discipline rules out certain programming mistakes, guarantees data race freedom, and opens up some new possibilities, such as gradual initialization and type(state) changes. In the first lecture, I will present Mezzo via a series of examples. In the second lecture, I would like to present the meta-theory of Mezzo. It is organized in a modular manner and has been machine-checked in Coq.

Olivier Serre
Tree Automata, Logic and Verification of (Higher-Order-) Functional Programs

The first goal of these two lectures is to introduce the audience with tree automata and their connections with model checking of various logic (with a special focus on monadic second order logic). In particular we will explain why these two formalisms are equi-expressive when describing sets of trees.
In a second part we will explain how a higher-order recursion scheme (a kind of term rewriting system) can be used to model the behaviour of a higher-order functional program by generating (assuming some restriction on the program) its syntax tree.
Finally we will combine these two concepts, automata/logic and higher-order recursion schemes, and argue that they can successfully be used to solve important questions related to verification of programs, in particular the model-checking problem (both local and global) as well as the synthesis problem.
Note: the slides of the two lectures are available here and here.

Bruno Vallette (Université Nice Sophia Antipolis)
Théorie de la déformation des algèbres de Batalin—Vilkovisky

La notion d’algèbre de Batalin—Vilkovisky est assez élémentaire : algèbre commutative munie d’un opérateur différentiel d’ordre 2 et de carré nul. Elle apparait aujourd’hui en algèbre (algèbres vertex), géométrie (variétés de Frobenius), topologie (topologie des cordes) et physique mathématique (renormalisation).
Le but de ces exposés sera d’établir la théorie de la déformation des algèbres de Batalin—Vilkovisky (BV). Pour cela, nous aurons besoin de plusieurs outils, que nous rappellerons : une opérade qui code la catégorie de algèbres BV, une bonne résolution de cette opérade (la résolution de Koszul et le modèle minimal), et enfin, une algèbre de Lie qui code les déformations de structures d’algèbres BV.
Au final, cette théorie permettra de résoudre plusieurs conjectures : celle de Lian—Zuckerman sur les algèbres vertex et celles de Kontsevich sur l’action du groupe de Givental, par exemple.
lectures.1403247794.txt.gz · Last modified: 2014/06/20 09:03 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