JAIST Logic Workshop Series

Workshop on Proofs as Processes

20–21 January 2014

Kanazawa, Ishikawa, Japan

About the Workshop

poster 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.



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


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

JAIST logoJAIST mark Royal Society Daiwa Anglo-Japanese Foundation