{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:01:19Z","timestamp":1760079679805,"version":"3.40.4"},"reference-count":37,"publisher":"EDP Sciences","issue":"1","license":[{"start":{"date-parts":[[2013,1,10]],"date-time":"2013-01-10T00:00:00Z","timestamp":1357776000000},"content-version":"vor","delay-in-days":9,"URL":"https:\/\/www.edpsciences.org\/en\/authors\/copyright-and-licensing"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["RAIRO-Theor. Inf. Appl."],"accepted":{"date-parts":[[2012,9,28]]},"published-print":{"date-parts":[[2013,1]]},"abstract":"<jats:p>We describe a sequent calculus<jats:italic>\u03bcLJ<\/jats:italic>with primitives for inductive and coinductive datatypes and equip it with reduction rules allowing a sound translation of G\u00f6del\u2019s system T. We introduce the notion of a<jats:italic>\u03bc<\/jats:italic><jats:italic>-closed category<\/jats:italic>, relying on a uniform interpretation of open<jats:italic>\u03bcLJ<\/jats:italic>formulas as strong functors. We show that any<jats:italic>\u03bc<\/jats:italic>-closed category is a sound model for<jats:italic>\u03bcLJ<\/jats:italic>. We then turn to the construction of a concrete<jats:italic>\u03bc<\/jats:italic>-closed category based on Hyland-Ong game semantics. The model relies on three main ingredients: the construction of a general class of strong functors called<jats:italic>open functors<\/jats:italic>acting on the category of games and strategies, the solution of recursive arena equations by exploiting<jats:italic>cycles<\/jats:italic>in arenas, and the adaptation of the winning conditions of parity games to build initial algebras and terminal coalgebras for many open functors. We also prove a weak completeness result for this model, yielding a normalisation proof for<jats:italic>\u03bcLJ<\/jats:italic>.<\/jats:p>","DOI":"10.1051\/ita\/2012028","type":"journal-article","created":{"date-parts":[[2013,1,10]],"date-time":"2013-01-10T13:38:17Z","timestamp":1357825097000},"page":"25-68","source":"Crossref","is-referenced-by-count":5,"title":["Strong functors and interleaving fixpoints in game semantics"],"prefix":"10.1051","volume":"47","author":[{"given":"Pierre","family":"Clairambault","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"250","published-online":{"date-parts":[[2013,1,10]]},"reference":[{"key":"R1","doi-asserted-by":"crossref","unstructured":"A. Abel and T. Altenkirch, A predicative strong normalisation proof for a lambda-calculus with interleaving inductive types, in Selected Papers from Int. Workshop on Types for Proofs and Programs, TYPES \u201999 (L\u00f6keberg, June 1999), edited by T. Coquand, P. Dybjer, B. Nordstr\u00f6m and J.M. Smith, Springer. Lect. Notes Comput. Sci. 1956 (2000) 21\u201340.","DOI":"10.1007\/3-540-44557-9_2"},{"key":"R2","doi-asserted-by":"crossref","unstructured":"S. Abramsky, Semantics of interaction : an introduction to game semantics, in Semantics and Logics of Computation, edited by A. Pitts and P. Dybjer. Publications of the Newton Institute, Cambridge University Press 14 (1996) 1\u201331.","DOI":"10.1017\/CBO9780511526619.002"},{"key":"R3","unstructured":"Arnold A. and Niwi\u0144ski D., Rudiments of \u03bc-Calculus, Studies in Logic and the Foundations of Mathematics. North-Holland 146 (2001)."},{"key":"R4","doi-asserted-by":"crossref","unstructured":"D. Baelde and D. Miller, Least and greatest fixed points in linear logic, in Proc. of 14th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2007 (Yerevan, Oct. 2007), edited by N. Dershowitz and A. Voronkov, Springer. Lect. Notes Artif. Intell. 4790 (2007) 92\u2013106.","DOI":"10.1007\/978-3-540-75560-9_9"},{"key":"R5","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(90)90151-7","volume":"70","author":"Bainbridge","year":"1990","journal-title":"Theoret. Comput. Sci."},{"key":"R6","doi-asserted-by":"crossref","unstructured":"W. Belkhir and L. Santocanale, The variable hierarchy for the lattice \u03bc-calculus, in Proc. of 15th Int. Conf. on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2008 (Doha, Nov. 2008), edited by I. Cervesato, H. Veith and A. Voronkov, Springer. Lect. Notes Artif. Intell. 5330 (2008) 605\u2013620.","DOI":"10.1007\/978-3-540-89439-1_42"},{"key":"R7","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0168-0072(92)90073-9","volume":"56","author":"Blass","year":"1992","journal-title":"Ann. Pure Appl. Log."},{"key":"R8","doi-asserted-by":"crossref","unstructured":"P. Clairambault, Least and greatest fixpoints in game semantics, in Proc. of 12th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2009 (York, March 2009), edited by L. de Alfaro Springer. Lect. Notes in Comput. Sci. 5504 (2009) 16\u201331.","DOI":"10.1007\/978-3-642-00596-1_3"},{"key":"R9","doi-asserted-by":"crossref","unstructured":"P. Clairambault. Least and greatest fixpoints in game semantics 2: strong functors and interleaving types. Informal proceedings of the workshop on Fixed Points in Computer Science, Coimbra, Portugal, September 2009.","DOI":"10.1007\/978-3-642-00596-1_3"},{"key":"R10","unstructured":"P. Clairambault, Logique et interaction : une \u00e9tude s\u00e9mantique de la totalit\u00e9. Ph.D. thesis, Universit\u00e9 Paris Diderot, Paris 7 (2010)."},{"key":"R11","doi-asserted-by":"crossref","first-page":"673","DOI":"10.1016\/j.apal.2009.07.016","volume":"161","author":"Clairambault","year":"2010","journal-title":"Ann. Pure Appl. Log."},{"key":"R12","unstructured":"J.R.B. Cockett and T. Fukushima, About Charity, Technical report. University of Calgary (1992)."},{"key":"R13","unstructured":"J.R.B. Cockett and D. Spencer, Strong categorical datatypes I, in Proc. of Int. Summer Category Theory Meeting (Montr\u00e9al, June 1991), edited by R.A.G. Seely. Canadian Math. Soc. Conference Proceedings. Amer. Math. Soc. 13 (1992) 141\u2013169."},{"key":"R14","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)00099-5","volume":"139","author":"Cockett","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"R15","doi-asserted-by":"crossref","unstructured":"V. Danos, H. Herbelin and L. Regnier, Game semantics & abstract machines, in Proc. of 11th Ann. IEEE Symp. on Logic in Computer Science, LICS \u201996 (New Brunswick, NJ, July 1996). IEEE CS Press (1996) 394\u2013405.","DOI":"10.1109\/LICS.1996.561456"},{"key":"R16","doi-asserted-by":"crossref","unstructured":"P. Dybjer, Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics, in Logical Frameworks, edited by G. Huet and G. Plotkin. Cambridge University Press (1991) 280\u2013306.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"R17","doi-asserted-by":"crossref","unstructured":"P.J. Freyd, Algebraically complete categories, in Proc. of Int. Category Theory Conf., CT \u201990 (Como, July 1990), edited by A. Carboni and M.C. Pedicchio and G. Rosolini, Springer. Lect. Notes Math. 1488 (1990) 95\u2013104.","DOI":"10.1007\/BFb0084215"},{"key":"R18","doi-asserted-by":"crossref","unstructured":"P.J. Freyd, Recursive types reduced to inductive types, in Proc. of 5th IEEE Ann. Symp. on Logic in Computer Science, LICS \u201990 (Philadelphia, PA, June 1990). IEEE CS Press (1990) 498\u2013507.","DOI":"10.1109\/LICS.1990.113772"},{"key":"R19","doi-asserted-by":"crossref","unstructured":"P.J. Freyd, Remarks on algebraically compact categories, in Proc. of LMS Symp. on Applications of Categories in Computer Science (Durham, July 1991), edited by M.P. Fourman, P.T. Johnstone and A.M. Pitts. Cambridge University Press. London Math. Soc. Lect. Notes Ser. 177 (1992) 95\u2013106.","DOI":"10.1017\/CBO9780511525902.006"},{"key":"R20","unstructured":"J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and Types, Cambridge University Press. Cambridge Tracts in Theoret. Comput. Sci. 7 (1989)."},{"key":"R21","doi-asserted-by":"crossref","unstructured":"R. Harmer, J.M.E. Hyland and P.-A. Melli\u00e8s, Categorical combinatorics for innocent strategies, in Proc. of 22nd Ann. IEEE Symp. on Logic in Computer Science, LICS \u201907 (Wroc\u0142aw, July 2007). IEEE CS Press (2007) 379\u2013388.","DOI":"10.1109\/LICS.2007.14"},{"key":"R22","doi-asserted-by":"crossref","unstructured":"J.M.E. Hyland, Game semantics, in Semantics and Logics of Computation, edited by A. Pitts and P. Dybjer. Publications of the Newton Institute, Cambridge University Press 14 (1996) 131\u2013184.","DOI":"10.1017\/CBO9780511526619.005"},{"key":"R23","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"Hyland","year":"2000","journal-title":"Inf. Comput."},{"key":"R24","unstructured":"A. Joyal and R. Street, Braided monoidal categories, Math. Report 860081. Macquarie University (1986)."},{"key":"R25","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF01220868","volume":"21","author":"Kock","year":"1970","journal-title":"Arch. Math."},{"key":"R26","unstructured":"J. Lambek and P.J. Scott, Introduction to Higher Order Categorical Logic. Cambridge University Press. Cambridge Studies in Adv. Math. 7 (1988)."},{"key":"R27","doi-asserted-by":"crossref","first-page":"969","DOI":"10.1017\/S0960129505004895","volume":"15","author":"Laurent","year":"2005","journal-title":"Math. Struct. Comput. Sci."},{"key":"R28","doi-asserted-by":"crossref","unstructured":"T. Leinster, Higher Operads, Higher Categories, London Math. Soc. Cambridge University Press. Lect. Notes Ser. 298 (2004).","DOI":"10.1017\/CBO9780511525896"},{"key":"R29","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f, Hauptsatz for the intuitionistic theory of iterated inductive definitions, in Proc. of 2nd Scandinavian Logic Symp. (Oslo, June 1970), edited by J.E. Fenstad, North-Holland. Stud. Logic Found. Math. 63 (1971) 179\u2013216.","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"R30","doi-asserted-by":"crossref","unstructured":"G. McCusker, Games and full abstraction for a functional metalanguage with recursive types, Ph.D. thesis, Imperial College (1996). Also published in Springer\u2019s Distinguished Dissertations in Comput. Sci. ser. (1998).","DOI":"10.1007\/978-1-4471-0615-9_3"},{"key":"R31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1999.2845","volume":"160","author":"McCusker","year":"2000","journal-title":"Inf. Comput."},{"key":"R32","doi-asserted-by":"crossref","unstructured":"P.-A. Melli\u00e9s, Typed lambda-calculi with explicit substitutions may not terminate, in Proc. of 2nd Int. Conf. on Typed Lambda Calculi and Applications, TLCA \u201995 (Edinburgh, Apr. 1995), edited by M. Dezani-Ciancaglini and G. Plotkin, Springer. Lect. Notes Comput. Sci. 902 (1995) 328\u2013334.","DOI":"10.1007\/BFb0014062"},{"key":"R33","first-page":"47","volume":"6","author":"Okada","year":"1999","journal-title":"Theory. Appl. Categ."},{"key":"R34","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0304-3975(00)00341-8","volume":"278","author":"Power","year":"2002","journal-title":"Theoret. Comput. Sci."},{"key":"R35","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/S0022-4049(01)00098-6","volume":"168","author":"Santocanale","year":"2002","journal-title":"J. Pure Appl. Algebra"},{"key":"R36","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1051\/ita:2002010","volume":"36","author":"Santocanale","year":"2002","journal-title":"Theor. Inform. Appl."},{"key":"R37","doi-asserted-by":"crossref","unstructured":"W. Thomas, Languages, Automata, and Logic, in Handbook of Formal Languages, Beyond Words, edited by G. Rozenberg and A. Salomaa. Springer 3 (1997) 389\u2013455.","DOI":"10.1007\/978-3-642-59126-6_7"}],"container-title":["RAIRO - Theoretical Informatics and Applications"],"original-title":[],"link":[{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012028\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:46:23Z","timestamp":1745945183000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.rairo-ita.org\/10.1051\/ita\/2012028"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1]]},"references-count":37,"journal-issue":{"issue":"1"},"alternative-id":["ita120042"],"URL":"https:\/\/doi.org\/10.1051\/ita\/2012028","relation":{},"ISSN":["0988-3754","1290-385X"],"issn-type":[{"type":"print","value":"0988-3754"},{"type":"electronic","value":"1290-385X"}],"subject":[],"published":{"date-parts":[[2013,1]]}}}