Second FISP Meeting
Paris, June 8 to June 10, 2017
Overview
The FISP project is part of a longterm, 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
Participants
Programme
Time 
Thursday 8 June 2017 
09:009:30 
Welcome and Coffee

9:3010:30 
Simona Ronchi Della Rocca: Proof normalisation and
approximation

10:3010:45 
Break

10:4511:25 
Giselle Reis: Ceres in intuitionistic logic

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

12:0514:00 
Lunch

14:0015:00 
Sergey Slavnov: Pomset logic and its generalizations: proofnets and sequent calculus

15:0015:30 
Break

15:3016:10 
Andrea AlerTubella: Full decomposition: the rules that go through

16:1016:50 
Anupam Das: On the linear fragment of classical propositional logic

16:5017:00 
Break

17:0017:40 
Delia Kesner: Quantitative Types for the LambdaMu Calculus

17:4019:30 
Open discussion

19:30 
Dinner

Time 
Friday 9 June 2017 
09:009:30 
Welcome and Coffee

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

10:3010:45 
Break

10:4511:25 
Juan P. Aguilera: The Infinite Epsilon Calculus

11:2512:05 
Kenji Miyamoto: Embedding Lemma in Epsilon Calculus with Equality

12:0514:00 
Lunch

14:0015:00 
Emmanuel Beffara: Describing processes and their interactions with proof theory

15:0015:30 
Break

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

16:1016:50 
Anela Lolic: A SequentBased Translation into the Epsilon Format

16:5017:00 
Break

17:0017:40 
David R. Sherratt: Towards an atomic abstract machine

17:4019:30 
Open discussion

Time 
Saturday 10 June 2017 
09:009:30 
Welcome and Coffee

9:3010:30 
Alessio Guglielmi: Proposal for a New Approach to Quantification

10:3010:45 
Break

10:4511:25 
Ulysse Gérard: Separating Functional Computation from Relations

11:2512:05 
Nicolas Guenot: Problems with proof systems for multiconclusion logics

12:0514:00 
Lunch

14:0019:30 
Open discussion

Abstracts of
Talks

Juan P. Aguilera (Vienna)
Title: The Infinite Epsilon Calculus
We outline the general theory of the Epsilon Calculus for formulae of
infinite length, including its connection to various settheoretic principles.

Andrea AlerTubella (Paris)
Title: Full decomposition: the rules that go through
abstract tba

Matthias Baaz (Vienna)
Title: Gödel logics and the fully boxed fragment of LTL
In this lecture we show that a very basic fragment of FOLTL, the monadic
fully boxed fragment (all connectives and quantifiers are guarded by P) is not
recursively enumerable wrt validity and 1satisfiability if three predicates are
present. This result is obtained by reduction of the fully boxed fragment of FOLTL
to the Gödel logic G↓, the infinitely valued Gödel logic with truth values in
[0,1] such that all but 0 are isolated. The result on 1satisfiability is in no way
symmetric to the result on validity as in classical logic: this is demonstrated by
the analysis of G↑, the related infinitelyvalued Gödel logic with truth values in
[0, 1] such that all but 1 are isolated. Validity of the monadic fragment with at
least two predicates is not recursively enumerable, 1satisfiability of the monadic
fragment is decidable. (joint work with Norbert Preining)

Emmanuel Beffara (Marseille)
Title: Describing processes and their interactions with proof theory
abstract tba

Anupam Das (Lyon)
Title: On the linear fragment of classical propositional logic
I will present a recent line of work, joint with Lutz Straßburger, on
the sound linear implications of classical propositional logic (CPL),
where variables may only occur once in the premiss and conclusion. This
fragment includes inferences such as 'switch' and 'medial' from deep
inference systems, and coincides with the 'multiplicative' fragment of
computability logic, due to Japaridze, and Blass' game semantics for
linear logic. Linear inferences already form a coNPcomplete set, i.e.
they can express all of CPL, and our main result is that they admit no
sound complete axiomatisation by any polynomialtime decidable subset of
linear inferences, unless coNP=NP. The proof itself brings techniques
and invariants from graph theory and Boolean function theory to the
area, and constitutes a rich framework for reasoning about linear
inferences in general.

Francesco Genco (Vienna)
Title: From hypersequents to parallel computation: Gödel logic and beyond
abstract tba

Ulysse Gérard (Paris)
Title: Separating Functional Computation from Relations
The logical foundations of arithmetic generally start with a
quantificational logic of relations. Of course, one often wishes to
have a formal treatment of functions within this setting. Both
Hilbert and Church added to logic choice operators (such as the
epsilon operator) in order to coerce relations that happen to encode
functions into actual functions. Others have extended the term
language with confluent term rewriting in order to encode functional
computation as rewriting to a normal form. We take a different
approach that does not extend the underlying logic with either choice
principles or with an equality theory. Instead, we use the familiar
twophase construction of focused proofs and capture functional
computation entirely within one of these phases. As a result, our
logic remains purely relational even when it is computing functions.
(joint work with Dale Miller)

Nicolas Guenot
Title: Problems with proof systems for multiconclusion logics
I'll discuss in this talk different approaches to the design of proof systems
for multiconclusion logics (eg. linear logic or classical logic), and comment
on their benefits and drawbacks, in particular when it comes to canonicity.
Then, I'll describe a work in progress attempting to establish a satisfactory
generalisation of natural deduction to the multiconclusion setting.

Alessio Guglielmi (Bath)
Title: Proposal for a New Approach to Quantification
abstract tba

Delia Kesner (Paris)
Title: Quantitative Types for the LambdaMu Calculus
abstract tba

Anela Lolic (Vienna)
Title: A SequentBased Translation into the Epsilon Format
The optimal calculation of Herbrand disjunctions from unformalized or formalized mathematical
proofs is one of the most prominent problems of computational proof theory. The uptodate
most direct approach to calculate Herbrand disjunctions is based on Hilbert’s epsilon formalism
(which is in fact also the oldest framework for proof theory). The algorithm to calculate Herbrand
disjunctions is an integral part of the proof of the Extended First Epsilon Theorem.
We show how to connect epsilon proofs and sequent calculus derivations with cuts. This leads to
an improved notation for the epsilon formalism and a computationally improved version of the
Extended First Epsilon Theorem, which allows a nonelementary speedup of the computation of
Herbrand disjunctions.

Kenji Miyamoto (Innsbruck)
Title: Embedding Lemma in Epsilon Calculus with Equality
abstract tba

Giselle Reis (Qatar)
Title: Ceres in intuitionistic logic
Ceres is a cutelimination method that transforms a proof P with cuts into
a proof with atomic cuts by merging parts of P with a resolution refutation
of a clause set, obtained from the cuts in P. The adaptation of this method
to intuitionistic logic poses some challenges, as structural restrictions
on intuitionistic calculi are often violated by the operations. In this
talk we will present Ceresi, a modification of Ceres that can be
successfully applied to intuitionistic proofs, resulting, this time, in
cutfree proofs. The structural violations resulting from resolution are
avoided by substituting this step with a new operation called proof
resolution. We also show that the method is complete for LJ. This is joint
work with David Cerna, Alexander Leitsch and Simon Wolfsteiner.

Christian Retoré (Montpellier)
Title: From logical and linguistic generics to Hilbert's tau and epsilon quantifiers
With our starting point being (universal) generics appearing in both natural
language
and mathematical proofs, and were further conceptualised in philosophy of language,
we introduce the tau subnector that maps a formula F to an individual term τx F
such that F (τx F ) whenever ∀xF .
We then introduce the dual subnector εxF which expresses the existential
quantification since F(εxF) ≡ ∃xF,
and describe its use for the semantics of indefinite and definite noun phrases.
Some logical and linguistic properties of this intriguing way to express
quantification are discussed.

Simona Ronchi Della Rocca (Turin)
Title: Proof normalisation and
approximation
abstract tba

David R. Sherratt (Bath)
Title: Towards an atomic abstract machine
The atomic lambda calculus is the computational interpretation of a intuitionistic
logical system with deep inference and is known for its efficiency when evaluating
terms; it is naturally fully lazy. This calculus implements full laziness through
the distributor construct, which can also be seen as the CurryHoward
correspondence of one inference rule in said system. Abstract machines are used to
administer evaluation strategies. We discuss the idea and issues of developing an
abstract machine for the atomic lambda calculus, which mainly involve locating free
variables. We shall also discuss a variant of the calculus which overcomes these
problems, which involves the use of director strings; a mechanism used to keep
track of free variables in a term by annotating every subterm.

Sergey Slavnov (Moscow)
Title: Pomset logic and its generalizations: proofnets and sequent calculus
We discuss noncommutative extensions of linear logic, namely, pomset logic and recently discovered semicommutative linear
logic, in which noncommutative multiplicative connectives are no longer selfdual. (The latter is not to be confused with quite
different noncommutative linear logic of Abrusci & Ruet.) These logics are defined by means of specific proofnets, and pomset logic
appears as a certain degeneration of the other one. We introduce then ``decorated” sequent calculi for these logics, which are sound and
complete. In particular, we get a (sort of) sequent calculus formalization of pomset logic, and this is one of the key results.
Venue
Organization