About the Workshop
The Workshop on Proofs as Processes II is a continuation of last years Workshop on Proofs as Processes. It will be held with the support of the Kurt Gödel Society, and a Royal Society Daiwa Anglo-Japanese Foundation International Exchanges Award in Noto, Ishikawa, from 12‐14 July, 2015.
After the successful development of a Hypernatural deduction system (LICS 2015 etc) we will continue our long-term project on extending the classical Curry-Howard correspondence to hypersequent calculus and parallel processes. It will bring together scientists working on the various related fields who are interested in collaborating in the project.
Participants
- Arnold Beckmann (Swansea University, Wales, UK)
- Matthias Baaz (University of Technology, Vienna, Austria)
- Alexander Leitsch (University of Technology, Vienna, Austria)
- Norbert Preining (JAIST, Nomi, Japan)
- Giselle Reis (INRIA, France)
Program
- Matthias Baaz: Cut-elimination for prenex cuts in LJ is elementary
- Arnold Beckmann: Hyper Natural Deduction - confluence and term systems
- Alexander Leitsch: Algorithmic introduction of quantified cuts
- Giselle Reis: Linear Logic
- Matthias Baaz: Embarassing Proof Theory
Discussion and problems (post meeting)
by Giselle Reis on Linear Logic
- Is linear logic with 2 subexponentials decidable?
- Computational interpretation of linear logic: there is a work on interpreting linear propositions as session types in pi-calculus. More details at this paper.
- Invertibility of inference rules: Following our discussion and the induction proof of invertibility Arnold pointed out, I wrote some notes on the subject (it is mostly for my own reference, but I think it is worth clarifying some details. Link in the email or on request).
by Alexander Leitsch on Cut Elimination
Note that the problem is fully solved for $\Pi_1$-cuts. The generalization to $\Sigma_1$-cuts and mixtures of $\Pi_1$ and $\Sigma_1$-cuts is easy.- While the substitutions generated by cut-elimination of $\Pi_2$-cuts have been characterized by some type of grammar (in a recent publication of Afshari, Hetzl and Leigh), the cut-introduction problem remains open - even for a single $\Pi_2$-cut. In particular it is an open question whether there exists a canonic solution (for the second-order problem ) of the schematic extended Herbrand sequent (and if this is not always the case is there a decision procedure for solvability?).
- In the case of general $\Pi_n$-cuts even the syntactic characterization of the substitutions generated by cut-elimination remains an open problem. So far there is no decent grammar formalism known specifying the corresponding set of terms.
by Matthias Baaz on Proof Theory
- Is there an elementary bound for the complexity of the cut-free proofs wrt the complexity of LK-proofs with only one prenex cut? (Note that such a bound does not exist if the cut is infix.)
- There is an elementary bound for the complexity of cut-free proofs wrt the complexity of LJ-proofs not containing $v$ with prenex cuts only. Show that this result does not hold if $v$ is added.
Venue
Kinoura Village, 927-1446 Ishikawa, Suzu, Oritomachi Hobu-25木ノ浦ビレッジ 〒927-1446 石川県珠洲市折戸町ホ部25番1
Contributions and participants
Further participants are asked to contact the organizers.Organising Committee
- Arnold Beckmann beckmann at swansea dot ac dot uk
- Norbert Preining preining at jaist dot ac dot jp
