Second FISP Meeting

Paris, June 8 to June 10, 2017

Overview

The FISP project is part of a long-term, ambitious project whose objective is to apply the powerful and promising techniques from structural proof theory to central problems in computer science for which they have not been used before, especially the understanding of the computational content of proofs, the extraction of programs from proofs and the logical control of refined computational operations.

The purpose of this second meeting is to discuss recent advances made the participants of the "FISP project".

Invited Speakers

Sergey Slavnov (HSE Tikhonov Moscow Institute of Electronics and Mathematics)
Simona Ronchi Della Rocca (Università di Torino)
Christian Retoré (LIRMM, Université Montpellier)
Alessio Guglielmi (University of Bath)
Emmanuel Beffara (Université d'Aix-Marseille)

Participants

Juan P. Aguilera (Vienna) .
Andrea Aler-Tubella (Paris) .
Matthias Baaz (Vienna) .
Emmanuel Beffara (Marseille) .
Roberto Blanco (Paris) ?
Eng Sambo Boris (Paris) .
Anupam Das (Lyon) *
Francesco Genco (Vienna) .
Ulysse Gérard (Paris) .
Nicolas Guenot (Berlin) ?
Alessio Guglielmi (Bath) .
Delia Kesner (Paris) .
François Lamarche (Paris) -
Anela Lolic (Vienna) .
Sonia Marin (Paris) *
Matteo Manighetti (Paris) *
Dale Miller (Paris) *
Kenji Miyamoto (Innsbruck) .
Georg Moser (Innsbruck) -
Michel Parigot (Paris) *
Giselle Reis (Qatar) *
Christian Retoré (Montpellier) .
Paul Rozière (Paris) .
Simona Ronchi Della Rocca (Turin) .
David R. Sherratt (Bath) .
Sergey Slavnov (Moscow) .
Lutz Straßburger (Paris) *
Marco Volpe (Paris) -

Programme

Time Thursday 8 June 2017
09:00-9:30

Welcome and Coffee

9:30-10:30

Simona Ronchi Della Rocca: Proof normalisation and approximation

10:30-10:45

Break

10:45-11:25

Giselle Reis: Ceres in intuitionistic logic

11:25-12:05

Francesco Genco: From hypersequents to parallel computation: Gödel logic and beyond

12:05-14:00

Lunch

14:00-15:00

Sergey Slavnov: Pomset logic and its generalizations: proof-nets and sequent calculus

15:00-15:30

Break

15:30-16:10

Andrea Aler-Tubella: Full decomposition: the rules that go through

16:10-16:50

Anupam Das: On the linear fragment of classical propositional logic

16:50-17:00

Break

17:00-17:40

Delia Kesner: Quantitative Types for the Lambda-Mu Calculus

17:40-19:30

Open discussion

19:30-

Dinner

Time Friday 9 June 2017
09:00-9:30

Welcome and Coffee

9:30-10:30

Christian Retoré: From logical and linguistic generics to Hilbert's tau and epsilon quantifiers

10:30-10:45

Break

10:45-11:25

Juan P. Aguilera: The Infinite Epsilon Calculus

11:25-12:05

Kenji Miyamoto: Embedding Lemma in Epsilon Calculus with Equality

12:05-14:00

Lunch

14:00-15:00

Emmanuel Beffara: Describing processes and their interactions with proof theory

15:00-15:30

Break

15:30-16:10

Matthias Baaz: Gödel logics and the fully boxed fragment of LTL

16:10-16:50

Anela Lolic: A Sequent-Based Translation into the Epsilon Format

16:50-17:00

Break

17:00-17:40

David R. Sherratt: Towards an atomic abstract machine

17:40-19:30

Open discussion

Time Saturday 10 June 2017
09:00-9:30

Welcome and Coffee

9:30-10:30

Alessio Guglielmi: Proposal for a New Approach to Quantification

10:30-10:45

Break

10:45-11:25

Ulysse Gérard: Separating Functional Computation from Relations

11:25-12:05

Nicolas Guenot: Problems with proof systems for multi-conclusion logics

12:05-14:00

Lunch

14:00-19:30

Open discussion

Abstracts of Talks

Venue

On Thursday and Friday we will be in the Sophie Germain building of IRIF, Université Paris Paris-Diderot - Paris 7, Room 1009.

And on Saturday we will be in the Halle aux Farines, Université Paris Paris-Diderot - Paris 7, Room 478F.

We have a workshop dinner on Thursday evening Au Petit Marguery Rive Gauche.

Organization

Andrea Aler-Tubella
Delia Kesner
Michel Parigot
Paul Rozière
Lutz Straßburger