Workshop
Structural Proof Theory
Paris, November 19-21 2008
This workshop is devoted to structural proof theory questions, from the design of deduction systems for various logics (classical, intuitionistic, modal, etc.) to the computational interpretations of proofs through cut-elimination, proof-search, proof complexity.
There will be 4 invited talks and the rest of the program will consist of contributed talks and discussions.
The workshop is open to everyone interested. All proposals of contributed talks
are welcome, including works in progress and discussions of open problems.
If you intend to give a talk or simply participate, please
let us know by sending an
email to parigot[at]pps.jussieu.fr.
This workshop is sponsored and serves as workshop of the following projects:
- ECO-NET project "computational interpretation of modal logics" (Paris 7, Moscow, Tbilisi)
- ANR project "INFER - Theory and Application of Deep Inference" ((INRIA Futurs, INRIA Nancy, Paris 7)
- PHC project "The Realm of Cut Elimination" (INRIA Futurs, TU Vienna)
- PHC project "Deep Inference and the Essence of Proofs" (INRIA Futurs, Bern)
It is also sponsored by the Kurt Gödel Society.
See below
the programme and
the location
of the workshop.
Invited Talks :
Contributed Talks :
- Sergei Adian (Steklov Mathematical Institute, Moscow, RU): Estimation of derivation lengths in one particular string
rewriting system.
- Lev Beklemishev (Steklov Mathematical Institute, Moscow, RU): On topological models for polymodal provability logic GLP
- Kai Brünnler (University of Bern, CH): An algorithmic interpretation of a deep inference system
- Peter Chapman (St Andrews University, UK): Syntactic Conditions for Invertibility in Sequent Calculi
- Kaustuv Chaudhuri (INRIA Futurs, Palaiseau, FR): Focusing Strategies for Synthetic Connectives
- René David (University of Savoie, Chambéry, FR) : Strong normalization results by translation.
- David Gabelaia (Razmadze Mathematical Institute, Tbilisi, GE): Provability logic and related modal systems - semantical considerations
- Revaz Grigolia (Tbilisi State University, GE): Unification in many valued logic
- Tom Gundersen (University of Bath, UK): Normalisation in Deep Inference
- Hugo Herbelin (INRIA Futurs, Palaiseau, FR): From classical logic to side-effects: the hidden exception handler of
Lambda-mu-calculus.
- Stefan Hetzl (INRIA Futurs, Palaiseau, FR): On the non-confluence of cut-elimination
- Valery Khakhanyan (MIIT, Moscow, Russia): Functional algebraic models for intuitionistic
arithmetic: two examples
- Richard McKinley (University of Bern, CH): Polarization and proof nets for classical logic
- Valery Plisko (Moscow Lomonossov State University, RU): Varpakhovskii's calculus and Markov's arithmetic.
- Norbert Preining (Technical University of Vienna, A): Herbrand Disjunctions for the Disentangled Fragment of Gödel Logics
- Fabien Renaud (University Paris 7, FR): The cube of resources
- Dmitrij Skvortsov(Russian Academy of Sciences, Moscow, RU): Axiomatization of superintuitionistic predicate logic of Kripke frames with nested domains over the set of reals
- Lutz Strassburger (INRIA Futurs, Palaiseau, FR): Extension without Cut
- Benoît Valiron (LIX, Palaiseau, FR): A linear-non-linear model for duplication.
- Steffen van Bakel (Imperial College London, UK): Lambda-bar-mu-mutilde and intersection and union types
- Daniel Weller (Technical University of Vienna, A): Skolemization of sequent calculus proofs in higher-order logic (work in progress)
- Stéphane Zimmermann (University Paris 7, FR): Some operationnal properties of call-by-value lambda-calculus
Participants :
- Sergei Adian (Russian Academy of Sciences, Moscow, RU)
- Matthias Baaz (Technical University of Vienna, A)
- Lev Beklemishev (Russian Academy of Sciences, Moscow, RU)
- Stefano Berardi (University of Torino, IT)
- Kai Brünnler (University of Bern, CH)
Beniamino Accattoli (University La Sapienza, Rome, IT)
- Peter Chapman (St Andrews University, UK)
- Kaustuv Chaudhuri (INRIA Futurs, Palaiseau, FR)
- Pierre-Louis Curien (University Paris 7, FR)
- René David (University of Savoie, Chambéry, FR)
- Claudia Faggian (University Paris 7, FR)
- David Gabelaia (Razmadze Mathematical Institute, Tbilisi, GE)
- Revaz Grigolia (Tbilisi State University, GE)
- Nicolas Guenot (INRIA Futurs, Palaiseau, FR)
- Alessio Guglielmi (University of Bath, UK)
- Tom Gundersen (University of Bath, UK)
- Willem Bernard Heijltjes (University of Edinburgh, UK)
- Hugo Herbelin (INRIA Futurs, Palaiseau, FR)
- Stefan Hetzl (INRIA Futurs, Palaiseau, FR)
- Danko Ilik (LIX, Palaiseau, FR)
- Thierry Joly (University Paris 7, FR)
- Delia Kesner (University Paris 7, FR)
- Valery Khakhanyan (MIIT, Moscow, Russia)
- Jean-Louis Krivine (University Paris 7, FR)
- François Lamarche (INRIA Nancy, FR)
- Pascal Manoury (University Paris 6, FR)
- Damiano Mazza (University Paris 13, FR)
- Richard McKinley (University of Bern, CH)
- Paul-André Melliès (University Paris 7, FR)
- Dale Miller (INRIA Futurs, Palaiseau, FR)
- Alberto Naibo (University Paris 1, FR)
- Vivek Nigam (Ecole Polytechnique, Palaiseau, FR)
- Novak Novakovic (INRIA Nancy, FR)
- Michel Parigot (University Paris 7, FR)
- Mattia Petrolo (University Paris 7, FR)
- Valery Plisko (Moscow Lomonossov State University, RU)
- Francesca Poggiolesi (Vrije Universiteit Brussel, B)
- Anne-Laure Poupon (LIX, Palaiseau, FR)
- Norbert Preining (Technical University of Vienna, A)
- Matthias Puech (LIX, Palaiseau, FR)
- Fabien Renaud (University Paris 7, FR)
- Luca Roversi (University of Torino, IT)
- Paul Roziere (University Paris 7, FR)
- Khimuri Rukhaia (Tbilisi State University, GE)
- Vincent Siles (LIX, Palaiseau, FR)
- Dmitrij Skvortsov (Russian Academy of Sciences, Moscow, RU)
- Arnaud Spiwack (LIX, Palaiseau, FR)
- Lutz Strassburger (INRIA Futurs, Palaiseau, FR)
- Benoît Valiron (LIX, Palaiseau, FR)
- Steffen van Bakel (Imperial College London, UK)
- Silvia Vecchiato (University of Siena, IT)
- Daniel Weller (Technical University of Vienna, A)
- Stéphane Zimmermann (University Paris 7, FR)
Programme
Wednesday, November 19
Thursday, November 20
Friday, November 21
Location of the Workshop:
175, rue Chevaleret, 75013 PARIS, France
room 1C6 (first floor, part C)
The nearest metro station is "Chevaleret" (line 6). To get to
the building see
map
Organization:
Abstracts:
Sergei Adian (Moscow, RU): Estimation of derivation lengths in one particular string
rewriting system.
Abstract: We shall study a string rewriting (semi-Thue) system in the alphabet {a,b,c} given by three rules: {aa->bc, bb->ac, cc->ab}. Termination of this system was proved by D. Hofmann and J. Waldmann in 2006. From their
proof only an exponential upper bound on derivation lengths can be
inferred. We give a sharp quadratic upper and lower bounds on derivation
lengths for this system.
Matthias Baaz (Vienna, A): Proof Theory of Gödel Logics
Abstract: In this lecture we give an overview on the proof theory of Gödel logics,
the construction of hypersequent calculi and sequents of relation calculi
We discuss the status of Herbrand's Theorem for Gödel logics in connection
with Skolemization and the Mid-hypersequent theorem. We show that witnessed
Gödel logics do not admit complete analytic calculi under quite weak
assumptions. The lecture is concluded by discussing open proof-theoretic
problems in this area.
Lev Beklemishev (Moscow): On topological models for polymodal provability logic GLP
Abstract: The well-known system of provability GLP (introduced by
Japaridze) is known to be Kripke-incomplete. We study natural
topological models of GLP where modalities correspond to derived set
operators in a poly-topological space. We show topological completeness
for a bimodal fragment of GLP. On the other hand, for more than three
modalities, completeness w.r.t. ordinal spaces turns out to be dependent
on large cardinal axioms of ZFC and various facts on stationary sets and
reflection. In particular, it is consistent (relative to ZFC) that GLP
is incomplete. However, under the assumption of large cardinal axioms
one can establish at least some partial completeness results. Partly
joint work with Guram Bezhanishvili and Thomas Icard.
Stefano Berardi (University of Torino, IT): Pre-fixed points and Unwinding of classical proofs
Abstract: We introduce a research project aimining to find a frame
for all existing method of unwiding the constructive
content of a classical proof. In this frame, all
deductions are parametrized w.r.t. a knowledge base,
and the classical part of a proof is interpreted as a
set of operators on the knowledge base. The pre-fixed
points of these operators are the state of knowledge
in which the constructive part of the proof is correct.
Kai Brünnler (Bern,): An algorithmic
interpretation of a deep inference system
Abstract: We set out to find something that corresponds to deep inference in the same way that the lambda-calculus corresponds to natural deduction. Starting from natural deduction for the conjunction-implication fragment of intuitionistic logic we design a corresponding deep inference system together with reduction rules on proofs that allow a fine-grained
simulation of beta-reduction.
Peter Chapman (St Andrews University, UK): Syntactic Conditions for Invertibility in Sequent Calculi
Abstract: We present sufficient syntactic conditions for when a rule is invertible with respect to a calculus, which is important for guiding proof search. It must be noted we give purely syntactic criteria; no guarantees are given as to the sanity of the rules. The conditions are illustrated with examples.
Kaustuv Chaudhuri (INRIA Futurs, Palaiseau, FR): Focusing Strategies for Synthetic Connectives
Abstract: Ordinary focusing (rigid) and maximal multi-focusing (canonical) proofs are generated by two diametrically opposite strategies in a single sequent calculus of synthetic connectives. Among the technical features of this calculus are transparently correct proofs of (the synthetic forms of) cut-elimination, identity, and permutation. Indeed, the synthetic cut-elimination procedure can trivially be shown to preserve both forms of focused proofs.
Pierre-Louis Curien (Université Paris 7, FR): The duality of computation under focus
Abstract:
In 2000, in a joint work with Hugo Herbelin, we presented a syntax drawn from the sequent calculus and expressing in a manifest way the duality of call-by-name and call-by-value at the level of computation. We revisit this work by making the whole framework polarity-sensitive, like in more recent works of Noam Zeilberger.
This results in a more modular system, where call-by-value and call-by-name are now distinguished at the level of types.
René David (University of Savoie, Chambéry, FR) : Strong normalization results by translation.
Abstract: We prove the strong normalization of full classical natural
deduction (i.e. with conjunction, disjunction and permutative
conversions) by using a translation into the simply typed
lambda-mu-calculus. We also extend Mendler's result on recursive
equations to this system.
David Gabelaia (Razmadze Mathematical
Institute, Tbilisi, GE): Provability logic and related modal systems - semantical considerations
Abstract: In this talk we consider the standard modal provability logic GL and
various weaker modal systems motivated by provability interpretation.
We will present a semantical study of these logics in terms of
tree-like Kripke frames as well as their topological semantics when
the modal diamond is interpreted as the topological derived set
operator. Corresponding completeness results will be discussed.
This is a joint work with Leo Esakia.
Revaz Grigolia (Tbilisi State University, GE): "Unification in many valued logic"
Abstract: The unification problems are analysed for many valued logics: Basic Logic, Gödel Logic, Lukasiewicz Logic and Product Logic. It is shown that the logics have finitary unification type.
Alessio Guglielmi (University of Bath, UK): Quasipolynomial normalisation (joint work with P Bruscoli and T Gundersen).
Abstract:
Surprisingly, cut elimination in propositional logic can be achieved in quasipolynomial time, if we adopt a deep-inference system. This is a recent result by Jerabek, based on work by Atserias, Galesi and Pudlak, employing threshold functions. Jerabek's proof is indirect, via a detour through the monotone sequent calculus. We recently managed to get a direct proof in deep inference, and in doing so we simplified the technique and clarified the role of threshold functions. This opens up the possibility of generalising this normalisation result in several different directions, and forces us to reconsider the moral and computational standing of normalisation. This talk is an attempt to give a high level overview of these rather technical topics.
Tom Gundersen (Bath): Normalisation in Deep Inference
Abstract: We continue our work on normalisation in propositional classical logic
using `atomic flows'. In this talk we show a new normalisation
procedure based on ideas very different from traditional normalisation
techniques.
It works by defining a scheme, where copies of (most of) a derivation
is inserted to create a derivation in normal form.
We show how this normal form is a generalisation of cut-elimination
and mention how different schemes can give normalisation procedures
with different properties (in particular confluence or less than
exponential complexity).
Hugo Herbelin (INRIA Futurs, Palaiseau, FR): From classical logic to side-effects: the hidden exception handler of
Lambda-mu-calculus.
Abstract: We revisit the proofs-as-programs connection between classical logic
and control operators and show that de Groote and Saurin's
Lambda-mu-calculus variant of (untyped) Parigot's lambda-mu-calculus,
a calculus shown observationnally complete by Saurin, hides an
exception handler, and, more generally, finds its place as a canonical
call-by-name lambda-calculus of delimited control à la Danvy and
Filinski.
Stefan Hetzl (INRIA Futurs, FR): On the non-confluence of cut-elimination"
Abstract: This talk is about a recent result obtained jointly with M. Baaz on the
non-confluence of cut-elimination in first-order classical logic: it is possible
to construct a sequence of polynomial-size proofs s.t. a proof in this sequence
has non-elementarily many different cut-free normal forms (each of
non-elementary size). These normal forms are different in a strong sense: They
not only represent different Herbrand-disjunctions but also have different
propositional structures and hence are not substitution-instances of a single
general proof.
This result shows that the constructive content of a cut-free proof does not
only depend on the proof with cuts from which it was generated but also on the
way the cuts are eliminated.
Valery Khakhanyan (MIIT, Moscow, Russia): Functional algebraic models for intuitionistic
arithmetic: two examples
Abstract: When we study intuitionistic theories we use different kinds of models: realizability types, topological, algebraic. In 1979 A.G.Dragalin suggested to try to examine various types from a single algebraic standpoint. In my topic I will talk only about his approach to HA - Heyting arithmetic and about Dragalin's techniques for different models of realizability. I will demonstrate that not all realizability models can be presented in the form suggested by Dragalin.
François Lamarche (INRIA Nancy) : Proof nets for Intuitionistic Logic
Abstract: We present a class of proof
nets that are specifically geared for Intuitionistic Linear logic
(without the ``plus'' connector), with a novel correctness
criterion. This fragment has special deterministic properties, which
allows the definition of a class of paths that, unlike the paths used
by say Danos-Regnier, are oriented, always starting at the conclusion
formula. In particular this permits the encoding of !-boxes by totally
local means, meaning that only special ``box edge'' unary links are needed,
without additional information. The proof of normalization is
remarkably simple, once the behavior of paths in correct nets has been
established.
Richard McKinley (Bern): Polarization and proof nets for classical logic
Abstract: I will present a class of proof-nets for propositional classical logic in which the structural rules are
simplified by adopting a polarized approach to the classical connectives. These nets combine two
(to my knowledge) previously mutually exclusive properties:
1) The nets have a correctness critereon and sequentialization with respect to sequent calculus, and
2) Translation into nets identifes sequent proofs differing by the usual commuting conversions,
and also makes identifications based on natural interactions between structural rules.
These nets were developed in conjunction with a computational calculus (the alpha-epsilon
calculus), which can be seen as an analogue of lambda calculus for sequent systems.
Paul-André Melliès (Paris): Operadic ideas in proof theory
Abstract: The notion of operad was introduced by algebraic topologists
in order to describe the algebraic structure of a topological group
after topological deformation. In this introductory talk, I will indicate
how these ideas may be relevant to proof theory and semantics.
Valery Plisko (Moscow RU): Varpakhovskii's calculus and Markov's arithmetic.
Abstract: Varpakovskii introduced a calculus in an extended propositional language
for the purpose of describing the class of realizable propositional
formulas. All the known realizable propositional formulas are deducible
in Varpakhovskii's calculus. We prove that every propositional formula
deducible in Varpakhovskii's calculus has the property that every one of
its closed arithmetical instances is deducible in Markov's arithmetic
obtained by adding Markov's principle and extended Church's thesis to
the intuitionistic arithmetic.
Norbert Preining (Technical University of Vienna, A): Herbrand Disjunctions for the Disentangled Fragment of Gödel Logics
Abstract: While Herbrand disjunctions in the usual sense cannot be achieved for Gödel logics, the disentangled fragment serves as a test piece for developing alternative ways of defining Herbrand disjunctions.
Fabien Renaud (University Paris 7, FR): The cube of resources
Abstract: A lot of languages with explicit substitutions have been studied. Many of them lack an essential property that we expect from such a language. The Kesner and Lengrand lambda lxr calculus satisfy all of them but has, not only explicit substitutions but also explicit duplication and erasure. We would like to know what are the intermediate languages (if either one or two explicit operators are turned into an implicit one) between this one and the original lambda-calculus.
In this talk, I will present you a framework (the cube) where there are the eight possible languages. All those ones enjoy expected properties such as full composition, simulation, preservation of strong normalization, etc which are proved only once using known properties of lambda-calculus and a set of simulation functions.
Dmitrij Skvortsov(Russian Academy of Sciences, Moscow, RU): Axiomatization of superintuitionistic predicate logic of Kripke frames with nested domains over the set of reals
Abstract: The superintuitionistic predicate logic of all Kripke frames
(with nested domains) based over the set of real numbers
is just the predicate version of Dummett's logic, i.e.,
it is obtained by adding the Dummett's axiom
(axiom of linearity) to intuitionistic predicate logic.
Lutz Strassburger (INRIA Futurs, Palaiseau, FR): Extension without Cut
Abstract: In proof theory one distinguishes sequent proofs with cut and cut-free sequent proofs, while for proof complexity one distinguishes Frege-systems and extended Frege-systems. In this talk we show how deep inference can provide a uniform treatment for both classifications, such that we can define cut-free systems with extension, which is neither possible with Frege-systems, nor with the sequent calculus. We show that the propositional pigeon-hole principle admits polynomial-size proofs in a cut-free system with extension. We also define cut-free systems with substitution and show that the system with extension p-simulates the system with substitution. This yields a new proof that extended Frege-systems p-simulate Frege-systems with substitution. Finally, we exhibit new class of tautologies that has similar properties as the propositional pigeon-hole principle for comparing systems with and without extension.
Benoît Valiron (LIX, Palaiseau, FR): A linear-non-linear model for duplication.
Abstract: Abstract: Motivated by quantum computation, we study a computational lamda-
calculus with a type system inspired by linear logic. We develop an
axiomatic semantics and a categorical description of the language, and
show how this system compare with intuitionistic linear logic.
Steffen van Bakel (Imperial College London, UK): Lambda-bar-mu-mutilde and intersection and union types
Abstract: We discuss the intersection and union type assignment as first presented in [Dougherty-Ghilezan-Lescanne'ITRS'04] for the calculus Lambda-bar-mu-mutilde [Curien-Herbelin'00] a proof-term syntax for Gentzen's classical sequent calculus.
We show that this notion is not closed for subject-expansion, and show how to fix this. We also show that it needs to be restricted to satisfy subject-reduction as well, even when limiting reduction to (confluent) call-by-name or call-by-value reduction, making it unsuitable to define a semantics.
Daniel Weller (Technical University of Vienna, A): Skolemization of sequent calculus proofs in higher-order logic (work in progress)
Abstract: Proof skolemization is a proof transformation that removes strong
quantifiers from sequent calculus proofs in first-order logic. In
particular, by skolemizing a proof one obtains a proof of the skolemized
end-sequent where all strong quantifier rules operate on ancestors of
cuts. This property fails to hold for the obvious extension of the
transformation to higher-order logic.
This work-in-progress report presents a sequent calculus with modified
quantifier introduction rules (resulting in a built-in skolemization).
It is shown that this new calculus avoids the problems of explicit
skolemization and, in first-order logic, also admits the method of
cut-elimination by resolution.
Stéphane Zimmermann (University Paris 7, FR): Some operationnal properties of call-by-value lambda-calculus
Abstract: Plotkin's call-by-value lambda-calculus has difficulties to manage free
variables. By looking at sequent calculus, we can obtain a finer version
of call-by-value lambda-calculus free of these problems, and even recover
subformula and standardization properties.