Me

Luca Cardelli • Short Biography

Luca Cardelli was born near Montecatini Terme, Italy, studied at the University of Pisa (until 1978-07-12), and has a Ph.D. in computer science from the University of Edinburgh (1982-04-01). He worked at Bell Labs, Murray Hill, from 1982-04-05 to 1985-09-20, and at Digital Equipment Corporation, Systems Research Center in Palo Alto, from 1985-09-30 to 1997-10-31, before assuming a position on 1997-11-03 at Microsoft Research, in Cambridge UK, where he is currently Principal Researcher and head of the Programming Principles and Tools and Security groups.

His main interests are in type theory and operational semantics (for applications to language design, semantics, and implementation), and in concurrency theory (for applications to computer networks and to modeling biological systems). He implemented the first compiler for ML (one of the most popular typed functional language, whose recent incarnations are Caml and F#) and one of the earliest direct-manipulation user-interface editors. He was a member of the Modula-3 design committee, and has designed a few experimental languages, including Obliq: a distributed higher-order scripting language (voted most influential POPL'95 paper 10 years later), and Polyphonic C#, a distributed extension of C#. His more protracted research activity has been in establishing the semantic and type-theoretic foundations of object-oriented languages, resulting in the 1996 book "A Theory of Objects" with Martin Abadi. More recently he has focused on modeling global and mobile computation, via the Ambient Calculus and Spatial Logics, which indirectly led to a current interest in Systems Biology and stochastic systems.

He has published over 100 papers, 1 book, and 2 proceedings as chair/editor (POPL'98 and ECOOP'03). He has served in over 80 Program Committees, and as editor of Theoretical Computer Science - Natural Computing (Elsevier 2008..), Foundations and Trends in Theoretical Computer Science (Now Publishers, 2005..), Transactions in Computational Systems Biology (Springer 2004+), Mathematical Structures in Computer Science (CUP 2001..2007), Science of Computer Programming (North Holland 1999..2006), Journal of Functional Programming (CUP 1995..2004), and Theory and Practice of Object Systems (Wiley 1994..1999).

He is a Fellow of the Royal Society, an ACM Fellow, an Elected Member of the Academia Europaea, an Elected Member of AITO, and a long-standing member of EATCS. In terms of unreliable statistics, he has a Hirsch index of ~58, he is the ~45th most cited computer scientist, and the 3rd most acknowledged computer scientist. His web page is at lucacardelli.name.

Luca Cardelli • Long Biography

Short Bio

Luca Cardelli was born near Montecatini Terme, Italy, studied at the University of Pisa (until 1978-07-12), and has a Ph.D. in computer science from the University of Edinburgh (1982-04-01). He worked at Bell Labs, Murray Hill, from 1982-04-05 to 1985-09-20, and at Digital Equipment Corporation, Systems Research Center in Palo Alto, from 1985-09-30 to 1997-10-31, before assuming a position on 1997-11-03 at Microsoft Research, in Cambridge UK, where he is currently Principal Researcher and head of the Programming Principles and Tools and Security groups.
His main interests are in type theory and operational semantics (for applications to language design, semantics, and implementation), and in concurrency theory (for applications to computer networks and to modeling biological systems). He implemented the first compiler for ML (one of the most popular typed functional language, whose recent incarnations are Caml and F#) and one of the earliest direct-manipulation user-interface editors. He was a member of the Modula-3 design committee, and has designed a few experimental languages, including Obliq: a distributed higher-order scripting language (voted most influential POPL'95 paper 10 years later), and Polyphonic C#, a distributed extension of C#. His more protracted research activity has been in establishing the semantic and type-theoretic foundations of object-oriented languages, resulting in the 1996 book "A Theory of Objects" with Martin Abadi. More recently he has focused on modeling global and mobile computation, via the Ambient Calculus and Spatial Logics, which indirectly led to a current interest in Systems Biology and stochastic systems.
He has published over 100 papers, 1 book, and 2 proceedings as chair/editor (POPL'98 and ECOOP'03). He has served in over 80 Program Committees, and as editor of Theoretical Computer Science - Natural Computing (Elsevier 2008..), Foundations and Trends in Theoretical Computer Science (Now Publishers, 2005..), Transactions in Computational Systems Biology (Springer 2004..),Mathematical Structures in Computer Science (CUP 2001..2007), Science of Computer Programming (North Holland 1999..2006), Journal of Functional Programming (CUP 1995..2004), and Theory and Practice of Object Systems (Wiley 1994..1999).
He is a Fellow of the Royal Society, an ACM Fellow, an Elected Member of the Academia Europaea, an Elected Member of AITO, and a long-standing member of EATCS. His web page is at lucacardelli.name.

Education

PhD in Computer Science, Edinburgh University (1982-04-01).
"Laurea" in Computer Science, University of Pisa (1978-07-12).

Employment

Microsoft Research, Cambridge UK (1997-11-03..Present). Researcher (1997-11-03), Assistant Director(2000-07-19), Principal Researcher (2006-11-23).
Univesity of Trento, Department of Information and Communication Technology (2005..2007). Visiting Professor.
Imperial College London, Department of Computing (2004..2012-12-31). Visiting Professor.
Digital Equipment Corporation, Systems Research Center, Palo Alto (1985-09-30..1997-10-31). Member of Research Staff.
Department of Computer and Information Science, University of Pennsylvania, Philadelphia (1984-01..1984-12). Adjunct Professor.
AT&T Bell Laboratories, Murray Hill (1982-04-05..1985-09-20). Member of Technical Staff.

Research Interests

Programming Languages and Type Theory
- Polymorphism, subtyping, objects, modularization, typechecking, semistructured data.
Distributed Systems and Concurrency
- Concurrent programming, distribution, mobility, global computation, process calculi, logics for concurrency.
Systems and Synthetic Biology
- Languages and notations for biochemical processes, membrane interactions, DNA computing.

Publications

Associations and Awards

Fellow of The Royal Society
ACM Fellow.
Academia Europaea Elected Member (Informatics)
AITO Elected Member.

Most Influential POPL Paper Award 2010 (for 2000) [for "Anytime, Anywhere. Modal Logics for Mobile Ambients" ].
AITO Dahl-Nygaard Senior Prize 2007 [Talk: ]
Most Influential ETAPS 1998 Paper Award (Awarded 2007) [for "Mobile Ambients" ].
Most Influential POPL Paper Award 2005 (for 1995) [for "A Language with Distributed Scope" ].

Visiting Professor at Imperial College London, Department of Computing (2004..2012-12-31).
Visiting Professor at Trento, Department of Information and Communication Technology (2005..2007).
Member of EATCS (European Association for Theoretical Computer Science).
Member of ISCB (International Society for Computational Biology).
Fellow of Girton College (1998..2004).

Courses, Tutorials, and Lecture Series

"Molecular Programming" Tutorial, Microsoft Research Cambridge, February 11, 2010.
"Molecules as Automata" Graduate Course, University of Warsaw, March 12-13 and May 7-8, 2009.
"Molecules as Automata" International Summer School on Natural Computing, Bertinoro, September 21, 2008.
"Artificial Biochemistry" Graduate Course, University of Trento, May 22-26, 2006.
"Abstract Machines of Systems Biology" Summer School on Biology Computation and Information, Dobbiaco, September 12-16, 2005.
"Mobility and Spatial Logic", Lecture Series, 5th International School on Formal Methods for the Design of Computer, Communication and Software Systems: Mobile Computing, Bertinoro, April 26-30, 2005.
"Membrane Interactions", Lecture Series, International School on Computational Sciences for Complex Systems in Biology, Rovereto, April 17-24 2004.
"Mobility and Spatial Logic", Lecture Series, 30eme Ecole de Printemps, Agay, March 24-29, 2002.
"Computation on Wide Area Networks", Lecture Series, Lipari Summer School, July 1-14 2001.
"Computation on Wide Area Networks", Cambridge University Minicourse Lectures, May 8,9,15,16 2001
"Mobility and Security", Lecture Series, Marktoberdorf Summer School, July 27 - Aug 6 1999.
"A Theory of Objects", Lecture Series, University of Technology Sydney, August 4-15 1997.
"A Theory of Objects", ECOOP Tutorial (with Martín Abadi), Jyväskylä, June 9-13, 1997.
"A Theory of Objects", OOPSLA Tutorial (with Martín Abadi), San Jose October 6-10, 1996.
"Object-Oriented Features", Lecture Series, ACM School on Functional and Object-Oriented Programming (with Martín Abadi), Sobotka, Poland, September 8-14, 1996.
"Class-based vs. Object-based Languages", PLDI Tutorial, 1996.
"Type-Driven Language Design", PLDI Tutorial, 1995.
"Typed Foundations of Object-Oriented Programming", POPL Tutorial, 1992.
"Typeful Programming", Lecture Series, IFIP State of the Art Seminar on Formal Description of Programming Concepts, Bombay, Feb 21-27, 1992.
"Typeful Programming", Lecture Series, IFIP State of the Art Seminar on Formal Description of Programming Concepts, CEDAV Serpro, Petropolis, Rio de Janeiro, Brazil, 18-28 April 1989.
"Semantic methods for object-oriented languages", OOPSLA Tutorial (with John Mitchell), 1988.
"Data Abstraction, Modularization, and Reusability", Lecture Series, University of Texas Year of Programming, 1986.
"Advanced Topics in Programming Languages", One-semester Course (with Dave MacQueen), University of Pennsylvania, Department of Computer and Information Science, 1984.

Editorial Boards

(2008..) Member of the Editorial Board, Theoretical Computer Science journal, series C - Theory of Natural Computing (TCSC), Elsevier.
(2005..) Member of the Editorial Board, Foundations and Trends in Theoretical Computer Science (Models and Systems), Now Publishers.
(2004..) Member of the Editorial Board, Transactions on Computational Systems Biology, Springer.
(2001..2007) Member of the Scientific Board, Mathematical Structures in Computer Science (MSCS), Cambridge University Press.
(1999..2006) Member of the Editorial Board, Science of Computer Programming (SCP), North Holland.
(1995..2004) Member of the Editorial Board, Journal of Functional Programming (JFP), Cambridge University Press.
(1994..1999) Associate Editor, Theory and Practice of Object Systems (TAPOS), Wiley.

Scientific Boards

(Jan2010..Dec2012) Member of the Royal Society Dorothy Hodgkin Fellowship Selection Panel - A Side.
(Aug2009..) Member of the Steering Committee for the annual conference on DNA Computing and Molecular Programming.
(2009..) Member of the Scientific Advisory Board for CSBE (BBSRC EPSRC Centre for Systems Biology at Edinburgh)
(2009..) Member of the Advisory Board for CRISP Consortium (BBSRC Combinatorial Responses in Stress Pathways)
(May2007..Dec2009) Member of the Royal Society Industry Fellowship Scheme Joint Panel.
(Jan2007..Mar2009) Member of the Royal Society Sectional Committee 1.
(Jan2006..Dec2008) Member of the Royal Society and Académie des Sciences Microsoft European Science Award Committee.
(Jan2006..Jul2007) Member of the Royal Society Research Grants Board A.
(2004..) Member of the PhD Thesis External Review Committee of the ICT Graduate School, University of Trento.

Program Committees

AlgebraicNumericBiology'10, CS2Bio'10, CONCUR'10, UnconventionalComputation'10, DNA16, FBTC'10, Static Analysis in Systems Biology'10 WS, ICSB'10 (Scientific Committee), Developments in Computational Models'09 WS, EXPRESS'09 WS, UnconventionalComputation'09, MeCBIC'08, FBTC'08, ECCB'08, AlgebraicBiology'08, CMSB'08, CMSB'07, NETTAB'07, AlgebraicBiology'07, QALP'07, FBTC'07, CONCUR'07, CMSB'06, ECOOP'06, FOSSACS'06, BioConcur'05, CMSB'05, ECOOP'05, COORD'05, PLAN-X'05, FM'05, TGC'05, ESOP'05, NETTAB'04 WS, BioConcur'04 WS, Express'04 WS, TCS'04, CMSB'04, ECOOP'04, EDBT'04, ASIAN'03, OOPSLA'03, BioConcur'03 WS, CSMB'03, ECOOP'03 (Chair), Web Dynamics WS'02, TCS'02, MA'01, PDCIWNMC WS'01 (in IPDPS'01), PODS'01, SAINT'01, FOOL'01, FOSSACS'01, CONCUR'00, TCS'00, ECOOP'00, DBPL WS'99, ASAP'99, WESTAPP WS'99, FOOL'99 (Chair), ESOP'99, PLILP/ALP'98, HLCL'98, ECOOP'98, ESOP'98, POPL'98 (Chair), DSL'97, ECOOP'97, Types in Compilation WS '97, Domain Specific Languages WS '97, Nomadic Computing WS '97, ICDE'97, FASE'97, COORD'97, FOOL'97, Agents WS ECOOP'96, ICFP'96, COORD'96, OOPSLA'95, COOTS'95, MFPS'95, POPL'94, FPCA'91, OOPSLA'91, ECOOP'91, ECOOP-OOPLSA'90, POPL'90, L&FP'88, LICS'87, FPCA'87

Working Groups

Founding Member, IFIP WG2.8 (Functional Programming), 1988..2000.
Member, IFIP WG2.2 (Formal Description of Programming Concepts), 1986..1995.

Statistics

Hirsch index ~58.
No. ~45 most cited computer scientist.
No. 3 most acknowledged computer scientist.
~800 pages pointing to www.luca.demon.co.uk and lucacardelli.name
Web site statistics for lucacardelli.name (~100,000 PDFs downloaded between Aug'06 and Jun'07)

International Business Card

Front

Back

Luca Cardelli • Scientific Biography • 2001-10

There are many intersecting and overlapping threads to Cardelli's research: denotational and operational semantics, concurrency, type theory, logic, compilers, and user interfaces. However, these all center around understanding aspects of programming languages. There are two main distinct areas of activity: from 82 to 96 in programming languages and type theory, and from 93 on in distributed systems and concurrency.

Programming Languages and Type Theory

As an undergraduate in Pisa, he was exposed to various programming systems, and to works in the semantics, the pragmatics, the type theory, and the design of programming languages. These were to be strong influences on his later work, both separately and jointly. His favorite programming language at the time was Simula 67, and he spent some effort trying to describe, unsuccessfully, the semantics of Simula classes: this issue would come back again later.

During his Ph.D. years in Edinburgh, he implemented [19]^(*) the first stand-alone compiler for the ML programming language (which was originally a part of Milner's LCF proof assistant). This was the first system to be widely used in teaching ML as a programming language. The system included a then novel abstract machine for lexically-scoped functional languages [19].

In Edinburgh he also studied early process calculi (Milner's CCS and SCCS), and proposed some new ones [12], but this activity would come to fruition only much later. His thesis advisor was Gordon Plotkin, from whom he learned advanced concepts in denotational and operational semantics.

After graduation, he was attracted to AT&T Bell Laboratories by Dave MacQueen, to keep working on languages and semantics. As a result, however, he found himself working in the original Unix operating system group, where he wrote several thousand lines of user-interface C code and where, because of the unpredictable behavior of C programs, he gained a much greater appreciation for the strongly typed languages he had been previously been using: Simula and ML. Within the Unix group, he cooperated with Rob Pike to design a language for more easily programming concurrent user interfaces, which was based on ideas from process calculi [17]. Rob Pike continued independently to develop and design related languages in following years, to support research in operating systems.

At Bell Labs, Dave MacQueen was then working with Ravi Sethi and Gordon Plotkin on a semantic model for polymorphism and recursive types. Cardelli noticed that, somewhat accidentally, this was a very good model for subtyping, particularly for describing the subtyping relationships between Simula-style record types (i.e. objects). Further, the model supported generalizations of subtyping to variant types (i.e. discriminated unions) and to function types. Out of this realization were coined the now widespread terms of "subsumption" (the notion of a uniform subtyping property that applies to all different kinds of types), "contravariance" (the basis for the correct subtyping rule for function types - not unknown to category theorists, but the subject of great confusion in object-oriented programming), and "structural subtyping" (the notion that only the structure of types, and not their names, determines their subtyping properties - unlike Simula). The early paper on this work [11] contains the first formal type systems for subtyping, along with a proof of typing soundness.

[Note. Subtyping in computer science is subtly different from ordinary set inclusion (although it can be modeled as such, if done appropriately). For example, integers are usually considered to be a subset of the reals, but this is not true on computers, which use different representations for integers and reals. Conversely, it is common in computer science to consider a record with 3 fields also as a valid record with 2 fields, while in math a 3-tuple is not a 2-tuple.]

Generalizing subtyping from record types to other type structures became a theme in the following years, and only at the end, with the book coauthored with Martin Abadi (discussed later), it came back full circle to the object types of Simula.

The generalization of subtyping to variant types turned out to be important in database areas, where a lot of attention must be paid to missing or varying information. The proper way to capture this in schemas (i.e. types) was the subject of debate at the time. Collaborating with former teachers and colleagues from Pisa, this resulted in the design of the Galileo language [18]: an ML-like language, with subtyping, for so called "conceptual modeling" in database areas.

The generalization of subtyping to function types was then not a feature of any language, although a lot was discussed about the proper typing rules for "methods" in object-oriented languages. To investigate this option, Cardelli designed and implemented a small functional languages called Amber [16], which was the first to incorporate structural subtyping as an orthogonal feature in a type system. Since not much of any interest can be expressed without recursive types, this led to implementing subtyping algorithms for recursive types. A proper understanding of this topic would wait until later.

The generalization of subtyping to polymorphic types resulted in the notion of "bounded quantification". [Quantification over types is used to model polymorphic function, i.e., functions that can operate uniformly on a variety of types.] A paper written with Peter Wegner on the topic [10] is still Cardelli's most-cited paper: it details the notion of bounded quantification, its use in programming, and an early collection of type rules that is still popular because it leads to decidable typecheckers.

In 1985 Cardelli moved to Palo Alto, California, to join a newly established research lab, the Digital Systems Research Center (SRC), founded by former members of Xerox PARC. The first few years at SRC saw a continuation and strengthening of theoretical work in type theory [7], now inspired by early work by the logicians Per Martin-Loef and Jean-Yves Girard. This was interspersed with systems research in user interfaces [20], and a return to the daily use of object-oriented languages.

One topic that took considerable effort was understanding the interaction between subtyping and recursive types. Recursive types can describe inductively defined types such as list and trees, but can also describe types needed for modeling the objects and classes of object-oriented languages. The latter requires the use of "negative" (or coinductive) recursion, that is, recursion interacting with function types, with bounded quantified types, and with type abstractions (the dual of type quantification). A paper with Roberto Amadio [8] provided a first and lasting investigation on subtyping for recursive types, connecting type systems, semantics, and typechecking algorithms. This was an indispensable foundation for much work to follow.

From 1985 to 1993 a number of projects were dedicated to understanding the interaction of subtyping with polymorphism, which is still the most difficult topic in the area. It was becoming clear, from a number of sources, that even modeling the "simple" notion of Simula classes required some very powerful type theory. One of the projects was the investigation of "row polymorphism", with John Mitchell [9], which was a possible alternative to subtyping. Another was an implementation of a programming language, Quest [15], which integrated subtyping and polymorphism in "the most orthogonal" possible way. Much progress in accurately modeling classes was made by colleagues, including novel and more general forms of bounded quantification.

A book written with Martin Abadi [6] and published in 1996 collects, integrates, and extends much of Cardelli's previous work in the area, as well as compatible work from other sources. This book is a focused monograph, rather than a survey. As a first new contribution, the book begins by developing an "object calculus" as a foundation for object-oriented languages, in much the same way that Church's lambda-calculus is a foundation for procedural languages. (Building directly on object calculi bypasses some annoying typing problems with using lambda calculi as a foundation.) A progression of increasingly sophisticated type systems, all with subtyping built-in, leads to precise type systems for a spectrum of object-oriented languages, from simple Simula-like languages, to the more sophisticated ones that appeared later. One of the final technical contributions is to show that by extending subtyping to the level of type operators ("higher-order subtyping"), one can be as expressive as the more interesting variations on the original idea of bounded quantification. The book has been used in many advanced courses, with the object calculus and related type systems providing a new foundation for much recent work.

The initial two papers on subtyping [11, 10] and the following work stimulated many other investigators from very early on. Through the 80's and 90's a combination of features pioneered by Cardelli and coauthors, in various forms and permutations, formed the core of the study of object oriented languages, with sessions appearing regularly in mainstream systems conferences, as well as in programming language and theory conferences. In particular, bounded quantification, often featured in research languages, is now about to officially debut in commercial languages as an extension of Sun's Java, and of Microsoft's C#. Moreover, work on the type theory of object-oriented languages (and languages in general) has recently become unexpectedly important, because sound type systems are now a requirement for computer security.

Distributed Systems and Concurrency

At SRC, in 1985, Cardelli found a Xerox-style programming environment based on multiprocessor workstations and local area networks. This meant that programming languages had to deal with concurrency, both on single processors, on multiprocessors, and on the network. Cardelli participated in the design of the Modula-3 language [14], which was used as the main programming language at SRC through the 90's. Modula-3 became part of a new generation of safe object-oriented languages for systems programming. It was the basis of many research projects outside of SRC, and it ended up inspiring the design of Java in many direct and indirect ways.

The Modula-3 environment supports the remote access of objects over the network. Building on top of this feature Cardelli implemented a scripting language called Obliq [13] that made it very easy to do network programming, and that was used extensively withing SRC. Obliq's main novel feature is "distributed lexical scoping", meaning that an active computation can migrate over the network and maintain a well-defined behavior, even if it refers to non-local resources. Obliq is still studied and referenced as a prime example of a simple network language. (Obliq is also a fairly direct implementation of one of the object calculi in [6]).

Obliq works very well as a scripting language over local area networks (LANs). But in 1995, web browsers began exposing people (and programmers) to Wide Area Networks (WANs). Computing models that were developed with LANs in mind, simply fall apart on a WAN -- from research project such as Obliq to industrial-strength endeavors such as CORBA. That's because WANs are asynchronous: there is no telling how long something will take, nor whether something has failed. Instead, the basis for LAN programming has always been Remote Procedure Call: a synchronous (bounded-delay) operation that rarely fails. Cardelli embarked on a program to understand the new "programming model" underlying WANs, in order to understand how to program WANs effectively. This lead to an informal description of the basic principles of global computation over WANs [3].

Around the time that Cardelli moved to Microsoft Research in Cambridge UK in 1997, he teamed up with Andy Gordon to try and develop more formal foundations of WAN computation. Existing process calculi did not seem to capture directly some essential WAN features. So, a new process calculus, the Ambient Calculus [4], was invented: it extends to core of Milner's pi-calculus with a hierarchy of locations and with mobility operations. The Ambient Calculus basically enables the formal analysis of mobile and wide-area systems, in part by taking advantage of a decade of previous work on pi-calculi. Because of a good compromise of generality (modeling ability) and compactness (formal tractability) it has quickly become very influential: over 400 citations to papers on "Ambients" written by various authors are reported on CiteSeer <http://citeseer.ist.psu.edu/> since 1998.

Once a plausible notion of WAN computation was defined, in the form of the Ambient Calculus, the goal became to specify properties of such computations, e.g. for theorem-proving, modelchecking, or bytecode verification purposes. Various approaches were attempted; the one that prevailed was a "spatial" modal logic where one could make location-aware assertions of the kind "here something is true" or "there something is true" or "somewhere something is true" (as well as routine "temporal" assertions) [2]. This constitutes a novel approach to logics for concurrency that has intriguing and rather unexpected connections with foundational logics such as linear logic.

The ambient logic gave rise, rather unexpectedly, to an application in a very different domain, as a query language for semistructured databases [5]. The connection is that, as predicate logic can be seen as a query language for relational databases, so the ambient logic (a logic for tree-structured locations) can be seen as a query language for tree-structured data (a.k.a. semistructured data, or XML).

In retrospect, the "spatial" or "location-aware" approach to logical descriptions makes sense also for most process calculi, where one may want to say "the system is made of two distinct parts such that..." or "the system owns a private resource such that...". This kind of assertions are not supported by traditional logics for concurrency. Cardelli's current efforts are in the semantics and proof theory of such assertions [1], together with Luis Caires. The goal is to be able to describe concurrent systems to the fine level of detail of how they are constructed and of what resources they use, and not just of how they behave abstractly.

Summary

Working Environment

Cardelli's work has been carried out in forward-looking industrial research labs, first for AT&T, then Digital Equipment, and now Microsoft. Each one is (or was) one of the main computing industry research labs of its era, with each having a stable population of about 50 researchers. The general goal of such labs is to inspire the next generation of products, without which no technology company can survive. However, it is generally recognized that the lack of "unfocused" research will necessarily lead to missed opportunities. As a consequence, work at these labs can be more focused and more directly motivated, but not altogether different from academic research. Work is publication-driven, or at least design-document-driven. Implementation is required for internal credibility, but "real implementation" is done by professional developers. Cardelli has worked in world-renown teams, cooperating with at most one or two people on each projects (which is common in such environments), and frequently supervising summer interns. His collaborators have included people from the same research lab, from academia, and from other research labs.

Style of Work

Partially because of the working environment, Cardelli's research has always alternated between theoretical work and practical implementation. These two activities have different quality-assessment measures, so it would not be appropriate to attempt straightforward transfers between the two. However, it is often fruitful to let each influence, without distortion, the other. Often, also, it is necessary to implement an idea to see how it works in practice, and conversely it is necessary to develop a theory to make sense of some complex practical situation. Cardelli's work has frequently proceeded along the lines of real-life complexity, to abstract simplifying theory, and back to simplified real-life systems. In computer science this path works unusually well because it is possible to pretty much define what "real-life" is.

Inventions

Cardelli's work has led to publications rather than patents (it is still not possible to patent a type system!). However, the following could count as inventions or devices in a broad sense:

Abstract Machines for Functional Languages
- An abstract machine is an abstract target assembly language for a compiler. The notion was not new, but Cardelli devised an abstract machine that was well suited for ML compilers (or any higher-order lexically scoped language), particularly for the implementation of function closures. Much practical and theoretical research was dedicated to this topic in following years. All functional language compilers now use abstract machines, although of different natures. [19]
Type Systems with Subtyping
- Although the initial focus of object-oriented languages was on "code inheritance" and "subclassing", it is now recognized that subtyping is ultimately a more flexible and important concept. Subtyping has been widely adopted by modern object-oriented languages such as Java and C# for mediating the relations between interfaces, in contrast with subclassing. Bounded quantification will soon be introduced both in Java and in C#. Cardelli pioneered the formal description of type systems with subtyping. Such formal descriptions are necessary to establish type soundness, which is ultimately necessary for security. After the first paper, this work was developed with a number of coauthors. [11, 10, 7, 8, 6]
Modula-3 Language Definition
- Modula-3 was a very influential systems programming language, until the advent of Java, which adopts most of Modula-3's unique features. Modula-3's type system is carefully defined via a subtyping relation. This was a team effort at SRC. [14]
Distributed Lexical Scoping
- As embedded in the Obliq language, it is a way to extend the notion of function "closure" to distributed environments. It extends Remote Procedure Call and code mobility. Obliq was widely used at SRC, and frequently cited, but was restricted to work within a network-based implementation of Modula-3 which was not easily exportable. [13]
Ambient Calculus
- A process-calculus model for mobile computation over wide-area networks. Developed with Andy Gordon, it is probably the most popular such model due to its generality and relative simplicity. This was directly motivated by industrial concerns about how to use "the web as a computer". [3, 4]
Spatial Logics
- Arising from work on the Ambient Calculus, these are modal logics where the modality is: "a certain property holds here (and now)". Their intent is to provide a logic that is inherently well-suited to talk about distributed systems. The basic idea can be applied to virtually any process calculus, but was previously overlooked, probably because of the accidental history of development of such calculi. It was initiated with Andy Gordon and Giorgio Ghelli (including a practical spinoff leading to an implemented system [5]), and is now being redirected to the pi-calculus and much refined with Luis Caires.