Document Open Access Logo

Inductive and Functional Types in Ludics

Author Alice Pavaux

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2017.34.pdf
  • Filesize: 0.64 MB
  • 20 pages

Document Identifiers

Subject Classification

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

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.

Cite As Get 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

Author Details

Alice Pavaux

References

  1. 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.
  2. 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.
  3. Michele Basaldella and Claudia Faggian. Ludics with repetitions (exponentials, interactive types and completeness). Logical Methods in Computer Science, 7(2), 2011. Google Scholar
  4. 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. Google Scholar
  5. Pierre-Louis Curien. Introduction to linear logic and ludics, part II. CoRR, abs/cs/0501039, 2005. Google Scholar
  6. Claudia Faggian and Martin Hyland. Designs, disputes and strategies. In CSL, pages 442-457, 2002. Google Scholar
  7. Christophe Fouqueré and Myriam Quatrini. Incarnation in ludics and maximal cliques of paths. Logical Methods in Computer Sciences, 9(4), 2013. Google Scholar
  8. Christophe Fouqueré and Myriam Quatrini. Study of behaviours via visitable paths. CoRR, abs/1403.3772v3, 2016. URL: https://arxiv.org/abs/1403.3772v3.
  9. Jean-Yves Girard. Geometry of interaction. I. Interpretation of system f. In Proc. Logic Colloquium 1988, pages 221-260, North-Holland, Amsterdam, 1989. Google Scholar
  10. 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. Google Scholar
  11. Martin Hyland and Luke Ong. On full abstraction for PCF: I, II, and III. Information and Computation, 163(2):285-408, 2000. Google Scholar
  12. Jean-Louis Krivine. Realizability in classical logic. Panoramas et synthèses, 27:197-229, 2009. URL: https://hal.archives-ouvertes.fr/hal-00154500.
  13. 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.
  14. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978. Google Scholar
  15. Eugenia Sironi. Types in Ludics. PhD thesis, Aix-Marseille Université, January 2015. Google Scholar
  16. Kazushige Terui. Computational ludics. Theor. Comput. Sci., 412(20):2048-2071, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact