ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 15:00 - 15:30 at S3 - III

Various kinds of game semantics have been introduced to characterize computational features of substructural logics, in particular fragments and variants of linear logic (LL) [5]. This line of research can be traced back to Lorenzen’s dialogues for intuitionistic logic [6] and to the works of Blass [2,3], Abramsky and Jagadeesan [1], among several others.

We look at substructural calculi from a game semantic point of view, guided by certain intuitions about resource conscious and, more specifically, cost conscious reasoning. To this aim, we start with a game for affine intuitionistic linear logic, where player I defends a claim corresponding to a (single-conclusion) sequent, while player II tries to refute that claim. Branching rules for additive connectives are modeled by choices of II, while branching for multiplicative connectives leads to splitting the game into parallel subgames, all of which have to be won by player I to succeed. The game comes into full swing by using subexponentials ([4][7]) for representing two types of options - volatile and permanent - for purchasing resources. This leads to a new type of subexponential calculus where costs are attached to sequents. Different proofs are interpreted as more or less expensive strategies to obtain a certain resource from a bunch of resources (priced options). We also generalize the concept of costs and option’s prices in proofs by using a semiring structure. This allows for the interpretation a wider range of subexponential systems, giving meaning to resources in proofs in a more flexible way. We conclude by studying some proof-theoretical properties of the proposed systems, justifying our intended meaning for costs and resources.

[1] Samson Abramsky and Radha Jagadeesan. Games and full completeness for multiplicative linear logic. J. Symb. Log., 59(2):543–574, 1994.

[2] Andreas Blass. A game semantics for linear logic. Ann. Pure Appl. Logic, 56(1-3):183–220,1992.

[3] Andreas Blass. Some semantical aspects of linear logic. Logic Journal of the IGPL, 5(4):487–503, 1997.

[4] Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. The structure of exponentials: Uncovering the dynamics of linear logic proofs. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Kurt Gödel Colloquium, volume 713 of Lecture Notes in Computer Science, pages 159–171. Springer, 1993.

[5] Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1–102, 1987.

[6] Paul Lorenzen. Logik und agon. Atti Del XII Congresso Internazionale di Filosofia, 4:187–194, 1960.

[7] Vivek Nigam and Dale Miller. Algorithmic specifications in linear logic with subexponentials. In António Porto and Francisco Javier López-Fraguas, editors, PPDP, pages 129–140. ACM,2009.

Sat 6 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:30
IIIGaLoP at S3
13:30
60m
Talk
Model checking games: the recent advances on parity games
GaLoP
I: Nathanaël FijalkowCNRS, LaBRI, and Alan Turing Institute
14:30
30m
Talk
A Framework for Compositional Model Checking
GaLoP
Yu-Yang LinQueen Mary University of London, Nikos TzevelekosQueen Mary University of London
15:00
30m
Talk
Modalities as prices: a game model of intuitionistic linear logic with subexponentials
GaLoP
Timo LangVienna University of Technology, Chris FermüllerVienna University of Technology, Elaine PimentelFederal University of Rio Grande do Norte, Brazil, Carlos OlarteFederal University of Rio Grande do Norte, Brazil