Libri

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

    1. Roberto Di Cosmo and Dominique Nora. Le Hold-Up planétaire.. Calmann-Levy, October 1998.

      Edizione di opere collettive

    1. Roberto Di Cosmo and Sergei Soloviev, editors. Special Issue on Type Isomorphisms. Mathematical Structures in Computer Science, 2005. To appear.

      Articoli invitati

    1. Roberto Di Cosmo. A brief history of rewriting with extensionality. In Fairouz Kamareddine, editor, International Summer School on Type Theory and Rewriting, Glasgow, September 1996. Kluwer. A set of slides on the subject is available as tt http://www.dicosmo.org/Slides/GLA96.ps.gz.

      Articoli in riviste internazionali

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

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

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

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

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

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

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

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

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

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

      Conferenze invitate

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

      Congressi internazionali

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

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

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

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

    5. Roberto Di Cosmo and Adolfo Piperno. Expanding extensional polymorphism. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculus and Applications, volume 902 of Lecture Notes in Computer Science, pages 139-153, April 1995. (PS) (DVI) (ABSTRACT)

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

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

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

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

    10. Roberto Di Cosmo and Delia Kesner. 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), pages 35-46, Warsaw, Poland, 29 June- 2July 1997. IEEE Computer Society Press. (Gzipped PS)

    11. Roberto Di Cosmo, Jean-Vincent Loddo, and Stéphane Nicolet. A game semantics foundation for logic programming. In Catuscia Palamidessi, Hugh Glaser, and Karl Meinke, editors, PLILP'98, volume 1490 of Lecture Notes in Computer Science, pages 355-373, 1998.

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

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

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

    15. Roberto Di Cosmo and Jean-Vincent Loddo. Playing logic programs with the alpha-beta algorithm. In Michel Parigot and Adrei Voronkov, editors, LPAR'00, volume 1955 of Lecture Notes in Computer Science, pages 207-224, 2000.

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

    17. F. Clément, V. Martin, A. Vodicka, R. Di Cosmo, and P. Weis. 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), September 2003.

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

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

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

      Altri Congressi

    1. D. Delahaye, Roberto Di Cosmo, and B. Werner. 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. Marco Danelutto, Roberto Di Cosmo, Xavier Leroy, and Susanna Pelagatti. Parallel functional programming with skeletons: the ocamlp3l experiment. The ML Workshop, 1998.

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

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

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

      Tesi

    1. Roberto Di Cosmo. Isomorphisms of types. Tesi di dottorato, Dipartimento di Informatica, Universitá di Pisa, 40, Corso Italia - 56100 Pisa - Italy, January 1993.

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

      Corsi

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

    2. Roberto Di Cosmo. A brief history of rewriting with extensionality. Lecture notes. http://www.dicosmo.org/, September 1996.

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

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

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

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

      Articoli in preparazione o sottomessi

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

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

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

      Rapporti tecnici del DMI

    1. Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report 90-14, LIENS - Ecole Normale Supérieure, 1990. (ABSTRACT)

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

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

    4. Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Technical Report LIENS-93-11/INRIA 1911, LIENS-DMI and INRIA, 1993. (ABSTRACT)

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

      Rapporti tecnici non pubblicati

    1. Hassan Aït-Kaci and Roberto Di Cosmo. Compiling order-sorted feature term unification. TN 7, Digital Equipment Corporation, December 1993. (Compressed PS)

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

    3. Roberto Di Cosmo. Isomorfismi di Tipi. Master's thesis, Università di Pisa, 1986.

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

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

      Diffusione scientifica

    1. Roberto Di Cosmo. Piège dans le Cyberespace. Multimédium, 17 March 1998.

      makeatletterif@fileswimmediatewrite@auxoutstringbibcitedmiconfigurationfakefimakeatother