Curriculum Vitae

Roberto Di Cosmo

ACADEMIC POSITIONS:

1er Septembre 1993 - now Maître de conférences (permanent, full time research and teaching position just below Associate Professor) at École Normale Supérieure in Paris,

1er Octobre 1992 - 31 Août 1993 ATER (temporary teaching and research position) at École Normale Supérieure in Paris^{1}.

BIRTHDATE: I was born in Parma, Italy, on 19 December 1963.

LANGUAGES: Besides my native language (Italian), I currently speak, read and write English, French and Spanish.

GRADUATION: ”Laurea” 110/110 cum laude in Computer Science at the University of Pisa, Italy, and at the Scuola Normale Superiore di Pisa, Italy, on the 24th of October 1986. At the same time, I had an intensive extra-academic activity which can be summarized as follows:

• August-September 1984 : 2 months summer stage in ITALSIEL, Rome, on Data Security and Protection.

• May 1985 : short internal memory on Robinson’s Unification Theorem and Type Assignment for pure λ−calculus, (this included an implementation of the unification algorithm for type inference both in Lisp and in C).

• August-September 1985 : 2 month summer stage in IBM-ITALY, Rome, on Natural Language Processing.

MILITARY HISTORY: Second Lieutenant in the Italian Army from April 1987 to June 1988.

POST-GRADUATE EDUCATION: From November 1988 to November 1992, graduate student at the Department of Computer science of the University of Pisa, Italy. I get my PhD with the thesis Iomorphisms of Types, the 25th of January 1993.

CONFERENCES ATTENDED:

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 Logic, Algebra and Computation, Marktoberdorf, (25/7/89 - 6/8/89)

1990 ACM Symposium on Principles of Programming Languages (POPL) (January 1990)

1École Normale Supérieure is one of the most prestigious academic institutions of France.

1990 4th Jumelage Meeting (Bari, June 1990, I give the talk Invertibility of terms in typed

lambda calculus with surjective pairing) 1990 CLICS 1990 (Paris, September 1990, I give the talks Provable Isomorphisms of Types,

Confluence for calculi with surjective pairing and terminal object.) 1991 UNIF 1991 (Barbizon, June 1991, I give the talk Provable Isomorphisms of Types.) 1991 ICALP 1991 (Madrid, July 1991, I present the paper [CDC91a].) 1991 LICS 1991 (Amsterdam, July 1991) 1991 MFCS 1991 (Warsaw, September 1991) 1992 POPL 1992 (Albuquerque, January 1992, I present the paper [DC92].) 1992 CADE 1992 (Saratoga Springs, June 1992) 1992 LICS 1992 (Santa Cruz, June 1992) 1993 ICALP 1993 (Lund, July 1993, I present the paper [DCK93a].) 1993 Typed Lambda Calculus (Roma, December 1993, I give the talk Confluence, Extension-

ality and Recursion in Typed Lambda Calculi). 1994 ICALP 1994 (Jerusalem, July 1994, I present the paper [DCK94a]). 1994 ALP-PLILP 1994 (Madrid, September 1994).

TALKS : 1990 Universitá di Torino Axiomatising Isomorphisms valid in every model. Invited by

Prof.M. Dezani-Ciancaglini. 1990 Ecole Normale Supérieure Provable Isomorphisms of Types. Invited by Prof.L. Fri-

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

reductions of typed lambda calculi. Visiting Scientist, 2/91. Invited by Prof.A. 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.

PROFESSIONAL CONSULTANT ACTIVITY: 1987 Three month as an industry consultant. I modified the operating system of an IBM PC

compatible to allow bootstrap from an EPROM card of my design, for use in embedded medical systems.

1988 During the military service, design and realization of an integrated system to handle the didactic activity at the Telecommunications School in Chiavari.

POST-GRADUATE STAGES: 1992 Three month with Peter Van Roy and Hassan Aït-Kaci at DEC-PRL (Digital Paris Re-

search Laboratory) to design and develop the kernel of a compiler for the logical-functional language LIFE.

TEACHING ACTIVITY: 1988 During the military service, I gave some introductory courses in programming to warrant

officers. 1991 Short course at the CIRM center of Marseille on Isomorphisms de types dans modeles de

langages fonctionnels et leur applications, invited by Prof. A. Preller. 1992 Course in Linear Logic at the University of Pisa (Italy). The course notes where written

in collaboration with Vincent Danos, of the University of Paris VII (France). 1992 -93

– Formal Languages: a 20 hours course given by Guy Cousineau at ENS for students

of the third year in Computer Science

1993 -94 – Introduction to Unix (Course and TA)

– Programming (TA) 1994 -95

– Introduction to Unix (Course and TA)

– Programming (TA)

– Semantics of Lambda Calculus (Part of the Course)

In this bibliography, an ∗ marks works that have been accepted, but did not appear yet.

References

Books, chapters of books, editorial works

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

International journals

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

Invited conferences

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

International conferences

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

Thesis

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

Course notes

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

Submitted or in progress papers

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

Technical reports in the 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.