Curriculum Vitae

Roberto Di Cosmo

EMPLOIS DANS L’UNIVERSIT’E: 1er Septembre 1993 - Maître de conférences à l’École Normale Supérieure de Paris, 1er Octobre 1992 - 31 Août 1993 ATER à l’École Normale Supérieure de Paris.

DATE ET LIEU DE NAISSANCE: Je suis né à Parma, en Italie, le 19 Decembre 1963.

LANGUES: Je parle courramment l’ Italien (ma langue mère), le Français, l’Anglais et l’Espagnol. SERVICE MILITAIRE: Sous-lieutenant dans les Service des Transmission de l’Armée Italienne pour le period Avril 1987 - Juin 1988.

ETUDES DOCTORALES: Après le service militaire, j’ai reçu une bourse pour faire les études de doctorat en informatique au Departement d’Informatique de l’Université de Pise. Je soutiens ma thèse Isomorphismes de Types à Pisa le 25 Janvier 1993. PARTICIPATION A CONFERENCES: 1986 X Mathematical Logics meeting on Logics and Computer Science (Siena, 1986) 1986 Logics and Computer Science: new trends and applications (Torino, October 1986). 1989 International Summer School on Logiç Algebra and Computation, Marktoberdorf, (25/7/89

- 6/8/89) 1990 ACM Symposium on Principles of Programming Languages (POPL) (January 1990) 1990 4th Jumelage Meeting (Bari, June 1990, Je fais un seminaire intitule’ Invertibility of terms

in typed lambda calculus with surjective pairing) 1990 CLICS 1990 (Paris, September 1990, Je fais les seminaires intitule’s Provable Isomor-

phisms of Types, Confluence for calculi with surjective pairing and terminal object.) 1991 UNIF 1991 (Barbizon, June 1991, Je fais un seminaire intitule’ Provable Isomorphisms of

Types.) 1991 ICALP 1991 (Madrid, July 1991, Je presente le papier [CDC91a].) 1991 LICS 1991 (Amsterdam, July 1991) 1991 MFCS 1991 (Warsaw, September 1991) 1992 POPL 1992 (Albuquerque, January 1992, Je presente le papier [DC92].) 1992 CADE 1992 (Saratoga Springs, June 1992)

1992 LICS 1992 (Santa Cruz, June 1992) 1993 ICALP 1993 (Lund, July 1993, Je presente le papier [DCK93a].) 1993 Typed Lambda Calculus (Roma, December 1993, Je fais un seminaire intitule’ Confluence,

Extensionality and Recursion in Typed Lambda Calculi). 1994 ICALP 1994 (Jerusalem, July 1994, Je presente le papier [DCK94a]). 1994 ALP-PLILP 1994 (Madrid, September 1994).

SEMINAIRES: 1990 Universitá di Torino Axiomatising Isomorphisms valid in every model. Invite’ par

professeurM. Dezani-Ciancaglini. 1990 Ecole Normale Supérieure Provable Isomorphisms of Types. Invite’ par professeurL.

Fribourg. 1991 Cambridge University - England. Second Order Isomorphisms of Types and Confluent

reductions of typed lambda calculi. Visiting Scientist, 2/91. Invite’ par professeurA. Pitts. 1991 UNIF 91 Isomorphisms of Types: some results, some problems. 1992 INRIA Isomorphismes de Types: thèorie et pratique. 1992 DEC-PRL How to use Types, Number and Categories to find your function in the func-

tion library. 1993 DEC-PRL An Abstract Machine for LIFE. 1993 Object-Oriented Workshop, Stanford Which Types for the Objects? 1994 University of Pennsylvania - Philadelphia, USA. Confluence, extensionality and re-

cursion in typed lambda calculi: some results and applications. 1994 University of La Plata - Argentina. Teoria y practica de los isomorfismos de tipo. 1994 CIRM - Marseille. How to combine first order algebraic rewriting systems, recursion and

extensional lambda calculi 1994 GDR - Lille. Isomorphismes de types pour la composition dynamique de modules.

ACTIVITE DE CONSULTANT: STAGES DE RECHERCHE: ENSEIGNEMENT: ACTIVITES ADMINISTRATIVES ET RESPONSABILITES COLLECTIVES: ACTIVITE DE RECHERCHE:

Dans cette bibliographie, un ∗ designe les travaux acceptes mais pas encore parus.

References

Livres, chapitres de livres, édition d’ouvrages collectifs

[DC95] Roberto Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.

Articles dans des revues internationales avec comité de lecture

[BDCL92] Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 2(2):231–247, 1992. Proc. of Symposium on Symbolic Computation, ETH, Zurich, March 1990.

[CDC95] * Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ-calculus with surjective pairing and terminal object. Journal of Functional Programming, 1995. To appear. This is an extended and revised version of [CDC91a].

[DC93a] Roberto Di Cosmo. Deciding type isomorphisms in a type assignment framework. Journal of Functional Programming, 3(3):485–525, 1993. Special Issue on ML.

[DC94] * Roberto Di Cosmo. Second order isomorphic types. A proof theoretic study on second order ł-calculus with surjective pairing and terminal object. Information and Computation, 1994. To appear.

[DCK94b] Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4:1–48, 1994. A preliminary version is available as Technical Report LIENS-93-11/INRIA 1911.

Conférences invitées

[DCL91] Roberto Di Cosmo and Giuseppe Longo. Constuctively equivalent propositions and isomorphisms of objects (or terms as natural transformations). In Logic for Computer Science, volume 21 of Mathematical Sciences Research Institute Publications, pages 73–94. Springer Verlag, Berkeley, November 1991.

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

[CDC91a] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λ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.

[DC92] 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.

[DCK93a] Roberto Di Cosmo and Delia Kesner. A confluent reduction for the extensional typed λ−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.

[DCK94a] 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.

[DCP95] * Roberto Di Cosmo and Adolfo Piperno. Expandic extensional polymorphism. Typed Lambda Calculus and Applications, 1995. To appear.

Thèses

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

Notes de cours

[DDC92] Vincent Danos and Roberto Di Cosmo. Introduction to linear logic. Course Notes, June 1992.

Articles soumis ou en préparation

[DC93b] Roberto Di Cosmo. Extensional ML. Draft, November 1993.

Rapports du DMI

[BDCL90] Kim Bruce, Roberto Di Cosmo, and Giuseppe Longo. Provable isomorphisms of types. Technical Report 90-14, LIENS - Ecole Normale Supérieure, 1990. To appear in Proc. of Symposium on Symbolic Computation, ETH, Zurich, March 1990, Mathematical Structures in Computer Science, 2(2).

[CDC91b] Pierre-Louis Curien and Roberto Di Cosmo. A confluent reduction system for the λcalculus with surjective pairing and terminal object. Technical Report 91-11, LIENS - Ecole Normale Supérieure, 1991.

[DC91] Roberto Di Cosmo. Invertibility of terms and valid isomorphisms. a proof theoretic study on second order ł-calculus with surjective pairing and terminal object. Technical Report 91-10, LIENS - Ecole Normale Supérieure, 1991.

[DCK93b] Roberto Di Cosmo and Delia Kesner. Simulating expansions without expansions. Technical Report LIENS-93-11/INRIA 1911, LIENS-DMI and INRIA, 1993.