{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:39:35Z","timestamp":1753889975932,"version":"3.41.2"},"reference-count":41,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,5,17]],"date-time":"2011-05-17T00:00:00Z","timestamp":1305590400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Ludics is peculiar in the panorama of game semantics: we first have the\ndefinition of interaction-composition and then we have semantical types, as a\nset of strategies which \"behave well\" and react in the same way to a set of\ntests. The semantical types which are interpretations of logical formulas enjoy\na fundamental property, called internal completeness, which characterizes\nludics and sets it apart also from realizability. Internal completeness entails\nstandard full completeness as a consequence. A growing body of work start to\nexplore the potential of this specific interactive approach. However, ludics\nhas some limitations, which are consequence of the fact that in the original\nformulation, strategies are abstractions of MALL proofs. On one side, no\nrepetitions are allowed. On the other side, the proofs tend to rely on the very\nspecific properties of the MALL proof-like strategies, making it difficult to\ntransfer the approach to semantical types into different settings. In this\npaper, we provide an extension of ludics which allows repetitions and show that\none can still have interactive types and internal completeness. From this, we\nobtain full completeness w.r.t. a polarized version of MELL. In our extension,\nwe use less properties than in the original formulation, which we believe is of\nindependent interest. We hope this may open the way to applications of ludics\napproach to larger domains and different settings.<\/jats:p>","DOI":"10.2168\/lmcs-7(2:13)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:17:26Z","timestamp":1316780246000},"source":"Crossref","is-referenced-by-count":2,"title":["Ludics with repetitions (Exponentials, Interactive types and Completeness)"],"prefix":"10.46298","volume":"Volume 7, Issue 2","author":[{"given":"Claudia","family":"Faggian","sequence":"first","affiliation":[]},{"given":"Michele","family":"Basaldella","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,5,17]]},"reference":[{"key":"10.2168\/LMCS-7(2:13)2011_Abr","unstructured":"Abramsky, S.: Axioms for definability and full completeness. In: Proof, Language, and Interaction (Essay in honor of Robin Milner) The MIT Press (2000) 55-76."},{"key":"10.2168\/LMCS-7(2:13)2011_AbrJagMac","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2930"},{"key":"10.2168\/LMCS-7(2:13)2011_AndreoliLP","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"10.2168\/LMCS-7(2:13)2011_thesisbas","unstructured":"Basaldella, M.: On Exponentials in Ludics. PhD Thesis (2008) University of Siena."},{"key":"10.2168\/LMCS-7(2:13)2011_BasFag","unstructured":"Basaldella, M., Faggian, C.: Ludics with Repetitions (Exponentials, Interactive Types and Completeness). In: LICS. (2009) 375-384."},{"key":"10.2168\/LMCS-7(2:13)2011_BasalTLCA09","unstructured":"Basaldella, M., Terui, K.: On the meaning of logical completeness. Logical Methods in Computer Science 6(4:11) (2010) 1-35."},{"key":"10.2168\/LMCS-7(2:13)2011_Coq","unstructured":"Coquand, T.: A semantics of evidence for classical arithmetic. J. Symb. Log. 60(1) (1995) 325-\u0096337."},{"key":"10.2168\/LMCS-7(2:13)2011_CurAbs","unstructured":"Curien, P.-L.: Abstract B\u00f6hm trees. Math. Struct. in Comp. Sci. 8(6) (1998) 559-591."},{"key":"10.2168\/LMCS-7(2:13)2011_CurLLL2","unstructured":"Curien, P.-L.: Introduction to Linear Logic and Ludics, part II. Advances of Mathematics (China) 35(1) (2006) 1-44."},{"key":"10.2168\/LMCS-7(2:13)2011_CurGS","unstructured":"Curien, P.-L.: Notes on game semantics. Manuscript (2006)."},{"key":"10.2168\/LMCS-7(2:13)2011_CurHerb","unstructured":"Curien, P.-L., Herbelin, H.: Abstract machines for dialogue games. Panoramas et Synth\u00e8ses 27 (2009) 231-275."},{"key":"10.2168\/LMCS-7(2:13)2011_FagTra","unstructured":"Faggian, C.: Travelling on designs. In: CSL. (2002) 427-441."},{"key":"10.2168\/LMCS-7(2:13)2011_introunif","unstructured":"Faggian, C., Fleury, M.-R., Quatrini, M.: An introduction to uniformity in Ludics. In: Linear logic in computer science, London Math. Soc. Lecture Note Ser., 316, Cambridge Univ. Press, Cambridge, (2004) 236-246."},{"key":"10.2168\/LMCS-7(2:13)2011_FP06","unstructured":"%Faggian, C., Piccolo, M: %A graph abstract machine describing event structure composition. %In: GT - VC, Graph Transformation for Verification and % Concurrency. ENTCS (2007) 21-36. Faggian, C., Piccolo, M.: Ludics is a model for the finitary linear pi-calculus. In: TLCA. (2007) 148-162."},{"key":"10.2168\/LMCS-7(2:13)2011_FagPic","unstructured":"Faggian, C., Piccolo, M.: Ludics is a model for the finitary linear pi-calculus. In: TLCA. (2007) 148-162."},{"key":"10.2168\/LMCS-7(2:13)2011_FP09","unstructured":"Faggian, C., Piccolo, M.: Partial Orders, Event Structures, and Linear Strategies. In: TLCA. (2009) 95-111."},{"key":"10.2168\/LMCS-7(2:13)2011_LinearLogic","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"10.2168\/LMCS-7(2:13)2011_GirGoI1","unstructured":"Girard, J.-Y.: Geometry of interaction I: Interpretation of System F. Logic Colloquium 88, In R. Ferro et al., (1989) 221-260."},{"key":"10.2168\/LMCS-7(2:13)2011_GirLC","unstructured":"Girard, J.-Y.: A New Constructive Logic: Classical Logic. Math. Struct. in Comp. Sci. 1(3) (1991) 255-296."},{"key":"10.2168\/LMCS-7(2:13)2011_meaning1","unstructured":"Girard, J.-Y.: On the meaning of logical rules I: syntax vs. semantics. Computational Logic (U. Berger and H. Schwichtenberg eds) Heidelberg Springer-Verlag (1999) 215 - 272."},{"key":"10.2168\/LMCS-7(2:13)2011_GirMeanII","unstructured":"Girard, J.-Y.: On the meaning of logical rules II : multiplicatives and additives. Foundation of Secure Computation (2000) 183-212."},{"key":"10.2168\/LMCS-7(2:13)2011_GirLoc","unstructured":"Girard, J.-Y.: Locus solum: From the rules of logic to the logic of rules. Math. Struct. in Comp. Sci. 11(3) (2001) 301-506."},{"key":"10.2168\/LMCS-7(2:13)2011_GirBook","unstructured":"Girard, J.-Y.: Le Point Aveugle, Cours de logique, Tome II: Vers l'imperfection. Visions des Sciences. Hermann (2007)."},{"key":"10.2168\/LMCS-7(2:13)2011_harthesis","unstructured":"Harmer, R. S.: Games and Full Abstraction for Nondeterministic Languages. PhD Thesis (1999) University of London."},{"key":"10.2168\/LMCS-7(2:13)2011_harGS","unstructured":"Harmer, R. S.: Innocent game semantics. Manuscript (2006)."},{"key":"10.2168\/LMCS-7(2:13)2011_Hy-On","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2000.2917"},{"key":"10.2168\/LMCS-7(2:13)2011_HylScha","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00241-9"},{"key":"10.2168\/LMCS-7(2:13)2011_KriRea","unstructured":"Krivine, J.-L.: Realizability in classical logic. Panoramas et Synth\u00e8ses 27 (2009) 197-229."},{"key":"10.2168\/LMCS-7(2:13)2011_LaurentThesis","unstructured":"Laurent, O.: \u00c9tude de la polarization en logique. PhD thesis, Universit\u00e9 Aix-Marseille II (2002)."},{"key":"10.2168\/LMCS-7(2:13)2011_LauPol","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.04.006"},{"key":"10.2168\/LMCS-7(2:13)2011_LauSvS","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.05.012"},{"key":"10.2168\/LMCS-7(2:13)2011_MauTh","unstructured":"Maurel, F.: Un cadre quantitatif pour la Ludique. PhD Thesis (2004) Universit\u00e9 Paris VII."},{"key":"10.2168\/LMCS-7(2:13)2011_MelTab","unstructured":"Melli\u00e8s, P.-A., Tabareau, N.: Resource modalities in game semantics. In: LICS. (2007) 389-398."},{"key":"10.2168\/LMCS-7(2:13)2011_MelvouRea","unstructured":"Melli\u00e8s, P.-A., Vouillon, J.: Recursive Polymorphic Types and Parametricity in an Operational Framework. In: LICS. (2005) 82-91."},{"key":"10.2168\/LMCS-7(2:13)2011_Nickau","unstructured":"Nickau, H.: Hereditarily Sequential Functionals: A Game-Theoretic Approach to Sequentiality. PhD thesis, Universit\u00e4t GH Siegen (1996)."},{"key":"10.2168\/LMCS-7(2:13)2011_paolini08tcs","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.021"},{"key":"10.2168\/LMCS-7(2:13)2011_Pittspoly","unstructured":"Pitts, A.M.: Parametric polymorphism and operational equivalence. Math. Struct. in Comp. Sci. 10(3) (2000) 321-359."},{"key":"10.2168\/LMCS-7(2:13)2011_alexis","unstructured":"Saurin, A.: Towards Ludics Programming: Interactive Proof Search. In: ICLP. (2008) 253-268."},{"key":"10.2168\/LMCS-7(2:13)2011_Terui","unstructured":"Terui, K.: Computational ludics. To appear in Theor. Comput. Sci. (2008)."},{"key":"10.2168\/LMCS-7(2:13)2011_yobeho","unstructured":"Yoshida, N., Berger, M., Honda, K.: Strong Normalisation in the pi-Calculus. In: LICS. (2001) 311-322."},{"key":"10.2168\/LMCS-7(2:13)2011_varyosh","unstructured":"Varacca, D., Yoshida, N.: Typed Event Structures and the it pi-Calculus: Extended Abstract. In: MFPS. (2006) 373-397."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1095\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1095\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:16Z","timestamp":1681243396000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1095"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,17]]},"references-count":41,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(2:13)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1104.0504","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1104.0504","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,5,17]]},"article-number":"1095"}}