Inductive and Functional Types in Ludics

Pavaux, Alice

doi:10.4230/LIPIcs.CSL.2017.34

File

LIPIcs.CSL.2017.34.pdf

Filesize: 0.64 MB
20 pages

Document Identifiers

DOI: 10.4230/LIPIcs.CSL.2017.34
URN: urn:nbn:de:0030-drops-77035

Author Details

Alice Pavaux

Cite AsGet BibTex

Alice Pavaux. Inductive and Functional Types in Ludics. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 34:1-34:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.34

Abstract

Ludics is a logical framework in which types/formulas are modelled by sets of terms with the same computational behaviour. This paper investigates the representation of inductive data types and functional types in ludics. We study their structure following a game semantics approach. Inductive types are interpreted as least fixed points, and we prove an internal completeness result giving an explicit construction for such fixed points. The interactive properties of the ludics interpretation of inductive and functional types are then studied. In particular, we identify which higher-order functions types fail to satisfy type safety, and we give a computational explanation.

Keywords

Ludics
Inductive types
Fixed point
Linear logic
Game semantics

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

References

David Baelde. Least and greatest fixed points in linear logic. ACM Trans. Comput. Logic, 13(1):2:1-2:44, January 2012. URL: http://dx.doi.org/10.1145/2071368.2071370.
David Baelde, Amina Doumane, and Alexis Saurin. Least and greatest fixed points in ludics. In Stephan Kreuzer, editor, Proceedings of the 24th Annual EACSL Conference on Computer Science Logic (CSL'15), pages 549-566, Berlin, Germany, September 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2015.549.
Michele Basaldella and Claudia Faggian. Ludics with repetitions (exponentials, interactive types and completeness). Logical Methods in Computer Science, 7(2), 2011.
Pierre Clairambault. Least and greatest fixpoints in game semantics. In Foundations of Software Science and Computational Structures, 12th International Conference (FOSSACS 2009). Proceedings, pages 16-31, 2009.
Pierre-Louis Curien. Introduction to linear logic and ludics, part II. CoRR, abs/cs/0501039, 2005.
Claudia Faggian and Martin Hyland. Designs, disputes and strategies. In CSL, pages 442-457, 2002.
Christophe Fouqueré and Myriam Quatrini. Incarnation in ludics and maximal cliques of paths. Logical Methods in Computer Sciences, 9(4), 2013.
Christophe Fouqueré and Myriam Quatrini. Study of behaviours via visitable paths. CoRR, abs/1403.3772v3, 2016. URL: https://arxiv.org/abs/1403.3772v3.
Jean-Yves Girard. Geometry of interaction. I. Interpretation of system f. In Proc. Logic Colloquium 1988, pages 221-260, North-Holland, Amsterdam, 1989.
Jean-Yves Girard. Locus solum: From the rules of logic to the logic of rules. Mathematical Structures in Computer Science, 11(3):301-506, 2001.
Martin Hyland and Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000.
Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. URL: https://hal.archives-ouvertes.fr/hal-00154500.
Paul-André Melliès and Jerome Vouillon. Recursive polymorphic types and parametricity in an operational framework. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 82-91, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.42.
Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.
Eugenia Sironi. Types in Ludics. PhD thesis, Aix-Marseille Université, January 2015.
Kazushige Terui. Computational ludics. Theor. Comput. Sci., 412(20):2048-2071, 2011.