Baelde, David ;
Doumane, Amina ;
Saurin, Alexis
Least and Greatest Fixed Points in Ludics
Abstract
Various logics have been introduced in order to reason over (co)inductive specifications and, through the CurryHoward correspondence, to study computation over inductive and coinductive data. The logic muMALL is one of those logics, extending multiplicative and additive linear logic with least and greatest fixed point operators.
In this paper, we investigate the semantics of muMALL proofs in (computational) ludics. This framework is built around the notion of design, which can be seen as an analogue of the strategies of game semantics. The infinitary nature of designs makes them particularly well suited for representing computations over infinite data.
We provide muMALL with a denotational semantics, interpreting proofs by designs and formulas by particular sets of designs called behaviours. Then we prove a completeness result for the class of "essentially finite designs", which are those designs performing a finite computation followed by a copycat. On the way to completeness, we investigate semantic inclusion, proving its decidability (given two formulas, we can decide whether the semantics of one is included in the other's) and completeness (if semantic inclusion holds, the corresponding implication is provable in muMALL).
BibTeX  Entry
@InProceedings{baelde_et_al:LIPIcs:2015:5437,
author = {David Baelde and Amina Doumane and Alexis Saurin},
title = {{Least and Greatest Fixed Points in Ludics}},
booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
pages = {549566},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897903},
ISSN = {18688969},
year = {2015},
volume = {41},
editor = {Stephan Kreutzer},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5437},
URN = {urn:nbn:de:0030drops54374},
doi = {10.4230/LIPIcs.CSL.2015.549},
annote = {Keywords: proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems}
}
07.09.2015
Keywords: 

proof theory, fixed points, linear logic, ludics, game semantics, completeness, circular proofs, infinitary proof systems 
Seminar: 

24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Issue date: 

2015 
Date of publication: 

07.09.2015 