About the Workshop
The Workshop on Proofs as Processes will be held
with the support of
the School of Information Science, Logic Group,
Japan Advanced Institute of Science
and Technology (JAIST) and a
Royal Society
Daiwa Anglo-Japanese
Foundation International Exchanges Award,
at
the building of the Modern Literature Museum
(石川四高記念文化交流館)
in Kanazawa on 20th and 21st January, 2014.
The workshop's aim is to function as a kick-off meeting for a 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)
- (cancelled) Agata Ciabattoni (University of Technology, Vienna, Austria)
- Christian Fermüller (University of Technology, Vienna, Austria)
- (cancelled) Faron Moller (Swansea University, Wales, UK)
- Michel Parigot (University Paris VII, Paris, France)
- Norbert Preining (JAIST, Nomi, Japan)
- Kazushige Terui (RIMS, Kyoto, Japan)
Program
Monday 20 January
| 14:00-14:30 | Opening - Presentation of current project:
Hypersequents and Communication
Arnold Beckmann, Norbert Preining |
| 14:30-15:30 | First-order proofs in Gödel logics: hypersequents, Herbrand disjunctions, computational content
Matthias Baaz We concentrate in this lecture on the prenex fragment of first order Gödel logics and investigate the computational content derivable from hypersequent (natural deduction) proofs and Herbrand disjunctions. |
| – Break – | |
| 15:45-16:45 | The Curry-Howard isomorphism between proofs and programs
Michel Parigot |
Tuesday 21 January
| 10:00-11:00 | Parallel Dialogue Games and Hypersequents
Christian Fermüller Motivated by the problem to find an interpretation for hypersequent systems that illuminates their supposed relation to parallel programs we revisit Lorenzen's dialogue game semantics for intuitionistic logic. A correspondence between winning strategies for the proponent of a formula F and cut-free sequent proofs of F is described and then lifted to the level of hypersequents by considering parallel dialogues and different forms of synchronization between such dialogues. This leads to a specific game based and thus computational interpretation of some well known intermediary logics, including of course intuitionistic and classical logics as extremal points of this important family of logics. |
| – Break – | |
| 11:15-12:15 | Some topics on linear logic, processes and hypersequents
Kazushige Terui |
| – Lunch Break – | |
| 13:45-14:45 | BOF talks, discussion |
| – Break – | |
| 15:00-16:00 | Funding, network, organizational |
| 16:00-16:15 | Closing |
| 19:00- | Workshop Dinner |
Venue
The venue will be the Modern Literature Museum (石川四高記念文化交流館) right in the center of Kanazawa. A map with further details will be provided soon.The following map collects the conference location (marked with a big warning triangle) plus some other points of interest, like restaurants (Fork-Knife icon), bars (Cocktail glass icon), hotels (bed icon), museums (mask icon), etc. Neither guarantee for correctness, nor completeness included.
View Proofs as Processes 2014 in a larger map
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
