Livres

    1. Di Cosmo (Roberto). -- Isomorphisms of types: from lambda-calculus to information retrieval and language design. -- Birkhauser, 1995. ISBN-0-8176-3763-X. (ABSTRACT)

    1. Di Cosmo (Roberto) et Nora (Dominique). -- Le Hold-Up planétaire.. -- Calmann-Levy, octobre 1998.

      Édition d'ouvrages collectifs

    1. Di Cosmo (Roberto) et Soloviev (Sergei) (édité par). -- Special Issue on Type Isomorphisms. -- Mathematical Structures in Computer Science, 2005. To appear.

      Articles invités

    1. Di Cosmo (Roberto). -- A brief history of rewriting with extensionality. In,: International Summer School on Type Theory and Rewriting, éd. par Kamareddine (Fairouz). -- Glasgow, septembre 1996. A set of slides on the subject is available as http://www.dicosmo.org/Slides/GLA96.ps.gz.

      Articles dans des revues internationales avec comité de lecture

    1. Bruce (Kim), Di Cosmo (Roberto) et Longo (Giuseppe). -- Provable isomorphisms of types. Mathematical Structures in Computer Science, vol. 2, n. 2, 1992, pp. 231-247. (DVI) (ABSTRACT)

    2. Di Cosmo (Roberto). -- Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, vol. 3, n. 3, 1993, pp. 485-525. -- Special Issue on ML. (DVI) (ABSTRACT)

    3. Di Cosmo (Roberto) et Kesner (Delia). -- Simulating expansions without expansions. Mathematical Structures in Computer Science, vol. 4, 1994, pp. 1-48. (ABSTRACT)

    4. Di Cosmo (Roberto). -- Second order isomorphic types. A proof theoretic study on second order lambda-calculus with surjective pairing and terminal object. Information and Computation, juin 1995, pp. 176-201.

    5. Curien (Pierre-Louis) et Di Cosmo (Roberto). -- A confluent reduction system for the lambda-calculus with surjective pairing and terminal object. Journal of Functional Programming, vol. 6, n. 2, 1996, pp. 299-327. -- This is an extended and revised version of this. (ABSTRACT)

    6. Di Cosmo (Roberto) et Kesner (Delia). -- Combining algebraic rewriting, extensional lambda calculi and fixpoints. Theoretical Computer Science, vol. 169, n. 2, 1996, pp. 201-220. (ABSTRACT)

    7. Di Cosmo (Roberto), Kesner (Delia) et Polonovski (Emmanuel). -- Proof nets and explicit substitutions. Mathematical Structures in Computer Science, vol. 13, n. 3, juin 2003, pp. 409-450.

    8. Di Cosmo (Roberto) et Pelagatti (Susanna). -- A calculus for dense array distributions. Parallel Processing Letters, vol. 13, n. 3, 2003, pp. 377-388.

    9. Di Cosmo (Roberto). -- A short survey of isomorphisms of types. Mathematical Structures in Computer Science, 2005. -- To appear.

    10. Di Cosmo (Roberto), Li (Zheng) et Pelagatti (Susanna). -- A calculus for parallel computations over multidimensional dense arrays. Computer Languages, Systems and Structures, 2005.

      Conférences invitées

    1. Di Cosmo (Roberto) et Longo (Giuseppe). -- Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). em In,: Logic from Computer Science, éd. par Moschovakis, pp. 73-94. -- Berkeley, Springer Verlag, 1991, Mathematical Sciences Research Institute Publications, volume 21. (ABSTRACT)

      Communications dans des conférences internationales avec comité de lecture

    1. Curien (Pierre-Louis) et Di Cosmo (Roberto). -- A confluent reduction system for the lambda-calculus with surjective pairing and terminal object. em In,: Intern. Conf. on Automata, Languages and Programming (ICALP), éd. par Leach, Monien et Artalejo. Lecture Notes in Computer Science, volume 510, pp. 291-302. -- Springer-Verlag, juillet 1991. (ABSTRACT)

    2. Di Cosmo (Roberto). -- Type isomorphisms in a type assignment framework. In,: 19th Ann. ACM Symp. on Principles of Programming Languages (POPL). pp. 200-210. -- ACM, 1992. (DVI) (ABSTRACT)

    3. Di Cosmo (Roberto) et Kesner (Delia). -- A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object. In,: Intern. Conf. on Automata, Languages and Programming (ICALP), éd. par Lingas (Andrzej). Lecture Notes in Computer Science, volume 700, pp. 645-656. -- Springer-Verlag, juillet 1993. (ABSTRACT)

    4. Di Cosmo (Roberto) et Kesner (Delia). -- Combining first order algebraic rewriting systems, recursion and extensional lambda calculi. In,: Intern. Conf. on Automata, Languages and Programming (ICALP), éd. par Abiteboul (Serge) et Shamir (Eli). Lecture Notes in Computer Science, volume 820, pp. 462-472. -- Springer-Verlag, juillet 1994. (PS) (DVI) (ABSTRACT)

    5. Di Cosmo (Roberto) et Piperno (Adolfo). -- Expanding extensional polymorphism. em In,: Typed Lambda Calculus and Applications, éd. par Dezani-Ciancaglini (Mariangiola) et Plotkin (Gordon), Lecture Notes in Computer Science, volume 902, pp. 139-153. -- avril 1995. (PS) (DVI) (ABSTRACT)

    6. Aponte (Maria-Virginia) et Di Cosmo (Roberto). -- Type isomorphisms for module signatures. In,: Programming Languages Implementation and Logic Programming (PLILP). Lecture Notes in Computer Science, volume 1140, pp. 334-346. -- Springer-Verlag, 1996. (ABSTRACT)

    7. Di Cosmo (Roberto). -- On the power o le diagrams. In,: Rewriting Techniques and Applications, Lecture Notes in Computer Science, pp. 200-214. -- juillet 1996. (PS) (DVI) (ABSTRACT)

    8. Di Cosmo (Roberto) et Kesner (Delia). -- Rewriting with polymorphic extensional lambda-calculus. In,: CSL'95. Lecture Notes in Computer Science, volume 1092, pp. 215-232. -- Springer-Verlag, 1996. Extended abstract presented in Paderborn, septembre 1995. (DVI) (ABSTRACT)

    9. Di Cosmo (Roberto) et Ghani (Neil). -- Combining algebraic rewriting with higher order extensional lambda calculi. In,: Intern. Conf. on Automata, Languages and Programming (ICALP)24, éd. par Degano (Pierpaolo), Gorrieri (Roberto) et Marchetti-Spaccamela (Alberto), Lecture Notes in Computer Science, pp. 237-247. -- 1997.

    10. Di Cosmo (Roberto) et Kesner (Delia). -- Strong normalization of explicit substitutions via cut elimination in proof nets (extended abstract). In,: Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, pp. 35-46. -- Warsaw, Poland, 29 juin- 2juillet 1997. (Gzipped PS)

    11. Di Cosmo (Roberto), Loddo (Jean-Vincent) et Nicolet (Stéphane). -- A game semantics foundation for logic programming. In,: PLILP'98, éd. par Palamidessi (Catuscia), Glaser (Hugh) et Meinke (Karl), Lecture Notes in Computer Science, volume 1490, pp. 355-373. -- 1998.

    12. Balat (Vincent) et Di Cosmo (Roberto). -- A linear logical view of linear type isomorphisms. In,: Computer Science Logic. Lecture Notes in Computer Science, volume 1683, pp. 250-265. -- Springer-Verlag, 1999.

    13. Di Cosmo (Roberto) et Guerrini (Stefano). -- Strong normalization of proof nets modulo structural congruences. In,: Rewriting Techniques and Applications. -- 1999.

    14. Di Cosmo (Roberto), Kesner (Delia) et Polonovski (Emmanuel). -- Proof nets and explicit substitutions. em In,: Foundation of Software Science and Computation Structure. Lecture Notes in Computer Science, volume 1784, pp. 63-81. -- Springer-Verlag, 2000.

    15. Di Cosmo (Roberto) et Loddo (Jean-Vincent). -- Playing logic programs with the alpha-beta algorithm. In,: LPAR'00, éd. par Parigot (Michel) et Voronkov (Adrei), Lecture Notes in Computer Science, volume 1955, pp. 207-224. -- 2000.

    16. Balat (Vincent), Di Cosmo (Roberto) et Fiore (Marcelo). -- Remarks on isomorphisms in typed lambda calculi with empty and sum type. In,: LICS. -- IEEE, juillet 2002. (Gzipped PS)

    17. Clément (F.), Martin (V.), Vodicka (A.), Di Cosmo (R.) et Weis (P.). -- Domain decomposition for flow simulation around a waste disposal site: direct computation versus code coupling using ocamlp3l. International Conference on Supercomputing in Nuclear Applications (SNA'2003), septembre 2003.

    18. Balat (Vincent), Di Cosmo (Roberto) et Fiore (Marcelo). -- Extensional normalisation and type-directed partial evaluation for typed lamda calculus with sums. In,: 31st Ann. ACM Symp. on Principles of Programming Languages (POPL). pp. 64-76. -- ACM, 2004.

    19. Di Cosmo (Roberto) et Dufour (Thomas). -- The equational theory of n,0,1,+,cdot,uparrow is decidable, but not finitely axiomatisable. In,: LPAR'05, Lecture Notes in Computer Science, p. 240. -- 2005.

    20. Di Cosmo (Roberto), Pottier (François) et Rémy (Didier). -- Subtyping recursive types modulo associative commutative products. Typed Lambda Calculus and Applications, 2005.

      Autres conférences

    1. Delahaye (D.), Di Cosmo (Roberto) et Werner (B.). -- Recherche dans une bibliothèque de preuves Coq en utilisant le type et modulo isomorphismes. In,: PRC/GDR de programmation, P^ole Preuves et Spécifications Algébriques. -- November 1997.

    2. Danelutto (Marco), Di Cosmo (Roberto), Leroy (Xavier) et Pelagatti (Susanna). -- Parallel functional programming with skeletons: the ocamlp3l experiment. The ML Workshop, 1998.

    3. Di Cosmo (Roberto). -- Legal tools to protect software: Choosing the right one. Upgrade, vol. 4, n. 3, juin 2003, pp. 21-23. -- Available as urlhttp://www.upgrade-cepis.org/issues/2003/3/up4-3DiCosmo.pdf.

    4. Di Cosmo (Roberto) et Pelagatti (Susanna). -- A calculus for dense array distributions. Second International Workshop on High-Level Parallel Programming and Applications, 2003.

    5. Di Cosmo (Roberto). -- E-duquons l'e-citoyen!. Bulletin de Specif, décembre 2004. -- Available as urlhttp://www.dicosmo.org/Papers/Specif-3-3.pdf.

      Thèses

    1. Di Cosmo (Roberto). -- Isomorphisms of Types. -- 40, Corso Italia - 56100 Pisa - Italy, Tesi di dottorato, Dipartimento di Informatica, Universitá di Pisa, janvier 1993.

    2. Di Cosmo (Roberto). -- Réécriture avec axiomes extensionnels et isomorphismes de types. -- 2, place Jussieu - 75005 Paris, Habilitation à diriger des recherches, Université de Paris VII, avril 1998.

      Notes de cours

    1. Danos (Vincent) et Di Cosmo (Roberto). -- Introduction to linear logic. -- juin 1992. Course Notes, very preliminary version of this. (DVI) (ABSTRACT)

    2. Di Cosmo (Roberto). -- A brief history of rewriting with extensionality. -- septembre 1996. Lecture notes. tt http://www.dicosmo.org/.

    3. Di Cosmo (Roberto). -- Sémantique dénotationnelle. -- 1996. Course Notes. tt http://www.dicosmo.org/CourseNotes.

    4. Di Cosmo (Roberto). -- Une panoramique de conceptes et langages orientés objets. -- 1996. Course Notes. tt http://www.dicosmo.org/CourseNotes/OO.

    5. Di Cosmo (Roberto). -- Compilation (pour la ma^itrise). -- 1999. Course Notes. tt http://www.dicosmo.org/CourseNotes/Compilation.

    6. Di Cosmo (Roberto). -- Introduction à l'informatique pour le deug. -- 2000. Course Notes. http://www.dicosmo.org/IF121.

      Articles soumis ou en préparation

    1. Aponte (Maria-Virginia), Di Cosmo (Roberto) et Dubois (Catherine). -- Signature subtyping modulo type isomorphisms. -- 1997. submitted. (Gzipped PS)

    2. Danos (Vincent) et Di Cosmo (Roberto). -- The Linear Logic Primer. -- 1997. In preparation: preliminary version available from verb|http://www.dicosmo.org|.

    3. Clément (F.), Li (A.), Martin (V.), Vodicka (A.), Di Cosmo (R.) et Weis (P.). -- Parallel programming with the ocamlp3l system, with applications to coupling numerical codes. Journal of Functional Programming, septembre 2003. -- Submitted.

      Rapports du DMI

    1. Bruce (Kim), Di Cosmo (Roberto) et Longo (Giuseppe). -- Provable isomorphisms of types. -- Rapport technique n. 90-14, LIENS - Ecole Normale Supérieure, 1990. (ABSTRACT)

    2. Curien (Pierre-Louis) et Di Cosmo (Roberto). -- A confluent reduction system for the lambda-calculus with surjective pairing and terminal object. -- Rapport technique n. 91-11, LIENS - Ecole Normale Supérieure, 1991. (Compressed DVI) (ABSTRACT)

    3. Di Cosmo (Roberto). -- Invertibility of terms and valid isomorphisms. A proof theoretic study on second order lambda-calculus with surjective pairing and terminal object. -- Rapport technique n. 91-10, LIENS - Ecole Normale Supérieure, 1991. (Compressed DVI) (ABSTRACT)

    4. Di Cosmo (Roberto) et Kesner (Delia). -- Simulating Expansions without Expansions. -- Rapport technique n. LIENS-93-11/INRIA 1911, LIENS-DMI and INRIA, 1993. (ABSTRACT)

    5. Danelutto (Marco), Di Cosmo (Roberto), Leroy (Xavier) et Pelagatti (Susanna). -- OcamlP3l: a functional parallel programming system. -- Rapport technique n. 98-01, LIENS - DMI, Ecole Normale Supérieure, 1998. (ABSTRACT)

      Rapports non publiés

    1. Aït-Kaci (Hassan) et Di Cosmo (Roberto). -- Compiling Order-Sorted Feature Term Unification. -- TN n. 7, Digital Equipment Corporation, décembre 1993. (Compressed PS)

    2. Clément (François), Vodicka (Arnaud), Di Cosmo (Roberto) et Weis (Pierre). -- Couplage de codes numériques, parallélisme et langages de haut niveau. -- RR n. 4825, INRIA, 2003. urlhttp://www.inria.fr/rrrt/rr-4825.html.

    3. Cosmo (Roberto Di). -- Isomorfismi di Tipi. -- Thèse, Università di Pisa, 1986.

    1. Di Cosmo (Roberto). -- An extensional operational and axiomatic semantics for type-inference with recursion and algebraic data types. -- octobre 1995. (ABSTRACT)

    2. Di Cosmo (Roberto) et Kesner (Delia). -- Strong normalization of explicit substitutions via cut elimination in proof nets, 1996. Available from tt http://www.dicosmo.org/Publications.

      Oeuvres de vulgarisation scientifique

    1. Di Cosmo (Roberto). -- Piège dans le Cyberespace. Multimédium, 17 mars 1998.

      makeatletterif@fileswimmediatewrite@auxoutstringbibcitedmiconfigurationfakefimakeatother