Current Past Me Papers Talks Artifacts Extra HotPage
Contact Curriculum Vitae Scientific Bio Press Bio Business Card Pictures

Luca Cardelli • Scientific Biography • May 2012


Research Career

There are many intersecting and overlapping threads in my research over the years: denotational and operational semantics, concurrency, type theory, logic, compilers, user interfaces, systems biology, and molecular programming. However, these all center around aspects of formal languages: programming languages for computing, modeling languages for science, and engineering languages for nanotechnology. There are three main distinct areas of activity: from 1982 to 1996 in programming languages and type theory, from 1993 to 2005 in distributed systems and concurrency theory, and from 2001 on in computational biology and nanotechnology.

Programming Languages and Type Theory (1982-1996)

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

During my Ph.D. years in Edinburgh, I implemented the first compiler for the ML programming language (which was originally a part of Milner's LCF proof assistant). ML was the first of a popular family of languages that now includes F# from Microsoft. 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 [ 129 ].

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

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

At Bell Labs, Dave MacQueen was then working with Ravi Sethi and Gordon Plotkin on a semantic model for polymorphism and recursive types. I 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 [ 55 ] contains the first formal type systems for subtyping, along with a proof of typing soundness.

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. The implications of this notion have generated a whole software industry dedicated to ‘object-oriented’ programming, which was inspired largely at first from pragmatics rather than mathematics.

Generalizing subtyping from record types to other type structures found in programming languages became a theme of mine in the following years, and only at the end, with the book coauthored with Martin Abadi (discussed later), I 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 [ 54 ]: an ML-like language, with subtyping, for so-called "conceptual modeling" in database areas.

The generalization of subtyping to function types was at that time not a feature of any language, although there was a lot of discussion about the proper typing rules for "methods" in object-oriented languages. To investigate this issue, I designed and implemented a small functional language called Amber [ R ], which was the first to incorporate structural subtyping as an orthogonal feature in a type system. Not much of interest can be expressed without recursive types, and this led to implementing a subtyping algorithm for recursive types in Amber. 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 [ 55 ] is still my 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 I 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 my theoretical work in type theory [ 45 ], now inspired by early work by the logicians Per Martin-Loef and Jean-Yves Girard. This was interspersed with systems research in user interfaces [ 123 ], 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 abstraction (the dual of type quantification). A paper with Roberto Amadio [ 47 ] 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 [ 51 ], which was a possible alternative to subtyping. Another was an implementation of a programming language, Quest [ 48 ], which integrated subtyping and polymorphism in "the most orthogonal" possible way. Much progress in accurately modeling classes was made by colleagues, including more general forms of bounded quantification.

A book written with Martin Abadi [ A ] and published in 1996 collects, integrates, and extends much of my 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 significant technical 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 book has never been revised but is still (in 2012) in print.

The initial two papers on subtyping [ 52 , 55 ] 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 myself and coauthors, in various forms and permutations, formed the core of the study of object oriented languages, with dedicated sessions appearing regularly in mainstream systems conferences, as well as in programming language and theory conferences. Bounded quantification has now been integrated in mainstream commercial languages (Sun's Java, and Microsoft's C#). A direct descendent of ML, the F# language, is a Microsoft product developed by the group I manage in Cambridge.

Work on the type theory of object-oriented languages (and languages in general) was originally meant to prevent accidental programming errors, but it has recently become unexpectedly more important, because sound type systems are now a requirement for computer security.

Distributed Systems and Concurrency Theory (1993-2005)

At Digital's Systems Research Center (SRC), in 1985, I 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. There I participated in the design of the Modula-3 language [ P ], 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 Sun's 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 I implemented a scripting language called Obliq [ 40 ] that made it very easy to do network programming, and that was used extensively within 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. (It is also a fairly direct implementation of one of the object calculi in [ A ]).

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 small research project such as Obliq to failed industry-wide 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 operation that rarely fails. I embarked on a program to understand the new "programming model" underlying WANs, to understand how to program WANs effectively. This led to an informal description of the basic principles of global computation over WANs [ 91 ].

Around the time that I moved to Microsoft Research in Cambridge UK in 1997, I teamed up with Andy Gordon to try and develop more formal foundations of WAN computation based on process algebra (formal concurrent languages with a strong mathematical basis). Existing process algebras did not seem to capture directly some essential WAN features. So, a new one, the Ambient Calculus [ 32 ], was invented: it extends to the core of Milner's pi-calculus (the most studied process algebra) 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 quickly became very influential.

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) [ 86 ]. This constitutes a novel approach to logics for concurrency with intriguing connections to 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 [ 85 ]. 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 assertion is not supported by traditional logics for concurrency. Efforts were then dedicated to the semantics and proof theory of such assertions [ 83 , 80 ], together with Luis Caires. The goal was 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.

Computational Biology and Nanotechnology (2001 - current)

Systems Biology

In 2001, indirectly as a result of the work on the Ambient Calculus, I became involved in co-supervising the thesis of a Biologist (Aviv Regev) who wanted to model spatial compartments in cells. (This resulted in a paper in 2004 [ 25 ] that is already in my top-ten most cited publications.) I realized that I needed to get some basic understanding of cellular biology, and I quickly learned that the field was in the middle of a deep transformation: Systems Biology was being proposed to further the understanding of biological entities at a whole-systems (not components) level. This resonated strongly with concepts from Computer Science, to the point that I thought I could contribute to that area. And besides, biological systems are just fascinating from an information-processing point of view.

Aviv Regev pioneered using a quantitative flavor of process algebra, and I began to wonder about what kind of programming languages (i.e., modeling languages) were needed to capture the complexity of biological systems. A major problem in systems biology is just to capture in a formal notation the complex and highly combinatorial interactions between components. This is in fact the problem that programming languages solve: they allow the flexible and compact representation of huge and complex state spaces, and enable their study. The main difference from standard programming languages is the massive concurrency of biological systems. But concurrency is the main subject of process algebra: I started applying the theory I was familiar with to these problems, although it was clear that many refinements would be needed.

At Microsoft meanwhile there was a growing realization that Scientific Computing (as opposed to Business Computing) was a broad and important area to which we should contribute, both for business impact and for access to talent. Compatibly with that, I was instrumental in the initial contacts that led to the formation in 2005 of the Microsoft - University of Trento Centre for Computational and Systems Biology: I have been serving on the Board of Directors since then. The center started from a core competence in process algebra modeling, and has been branching out in all areas of biological modeling.

From 2005 on I have participated in a number of projects in Systems Biology in collaboration with external researches, leading to a number of publications about modeling specific biological systems by process algebra techniques, ranging from immune system response [ 6 ], signaling networks [ 8 , 14 ], and cell cycle networks [ 2 ].

Quantitative Semantics

In our initial efforts to model biological systems we were building precise quantitative mathematical models based on process algebra, and there was a clear connection between the process algebra 'compositional' approach of modeling systems by composing subsystems and the biologist's tendency to think about system components and their interactions (in contrast to the mathematician's approach to focus on the function of the whole system). But we came across a couple of 'social' problems. On a more superficial level, how could we explain our modeling languages to experimental biologists so that they would be motivated to help us in our modeling efforts, leading to closing the model-experiment scientific cycle. On a deeper level, how could we explain to theoretical biologists, physicists, and mathematicians that we were doing precise modeling, and not some vague form of software coding not clearly related to, e.g., standard differential equation models.

A formal connection was needed between process algebra and the mainstream theory of dynamical systems. The former is concerned with representing interactions between components, and the latter with the dynamics of quantities over time. But there is a lingua franca between the two: the "programming language" of chemical reactions, which on one hand implicitly (phenomenologically) describes interactions between molecules, and on the other hand can be analyzed kinetically. That programming language has, in Computer Science parlance, two distinct (and in fact different) mathematical meanings: where the variables are interpreted as concentrations (mass-action / Ordinary Differential Equation (ODE) semantics) and where variables are interpreted as molecule counts (stochastic / Chemical Master Equation (CME) semantics).

I studied a simple process algebra that has the property of corresponding exactly, in terms of systems dynamics, to systems of chemical reactions. This established a precise and quantitative connection between process algebra and chemical descriptions of the same systems. Unlike chemical reactions, however, process algebra is compositional, which in practice means that it can avoid combinatorial explosions in system descriptions when modeling complex systems, purely via a different way of describing them. I showed that both the ODE and CME semantics of that simple algebra match classical chemistry, and that the algebra can be easily interpreted as "populations of interacting finite state automata".

In general, process algebra is much richer than that simplified chemical algebra, so there is scope for richer modeling. In fact, general process algebras can represent, by finite programs, systems that otherwise require an infinite set of chemical reactions or ODEs. Such systems are extremely common in Systems Biology, because they include all forms of complexation and regular and irregular polymerization. The reduction in descriptive complexity (potentially an infinite reduction!) is the main advantage that is gained by using process algebra and other computing-inspired formal language in the modeling of complex systems.

The next step needed to build on that foundation, which is still ongoing, is to fully develop a theory of quantitative process algebra, particularly the theory of quantitative approximation. This is the subject of much current research by a number of groups (particularly in the UK), who are now increasingly inspired by biological applications. There has been a rich related tradition in Computing, more often directed to probabilistic or hybrid (discrete-continuous) rather than stochastic systems. My contributions here have been to try to steer the area to consider stochastic systems more centrally, especially in collaboration with my co-author Radu Mardare [ 61 , 57 , 56 ].

Molecular Programming

Systems biology, like most of biology and science in general, is a discipline attempting in the first instance to understand how natural systems work. From an engineering viewpoint, its main aim is to reverse-engineer natural biological systems. But what about direct engineering of natural/physical/chemical systems? My natural inclination was always to think about compiling programming languages and process algebra models not only to software but also to physical matter: to active molecular structures like the ones found in biology. For a long time I could not see how that could be done, because there is relatively little 'predictive engineering' of molecular structures: e.g., we cannot flexibly engineer proteins.

All that changed for me when in 2008 I came across the Molecular Programming Project (an NSF “Expeditions in Computing” program) via a chance keynote invitation to the DNA'14 conference. In particular, Erik Winfree's group at Caltech was building upon an already long tradition of DNA computing to show how to use DNA to physically emulate arbitrary chemical systems (up to time scaling). The programming language there is the language of (arbitrary stochastic finite programs written as) chemical reactions, which is 'approximately' Turing-powerful in a precise sense [ 10 ], and the physical realization is DNA molecules that support any kinetics one may choose to program. There was a clear path from programming languages to executable matter, and I started working eagerly in the area: in 2009 I had a refereed paper in the DNA'15 conference, and in 2011 I was co-chair of the DNA'17 conference.

My goal then became to connect the theory of programming languages to this new 'target architecture' provided by molecular systems. There was a disconnect there, because the theory of programming languages has been largely qualitative: what can be computed, how it can be computed, and what is the meaning of a program (although the theory of algorithmic complexity is quantitative). Instead, the chemical and physical theories of molecular systems are quantitative, concerning dynamical systems, kinetics, and ultimately thermodynamics. Fortunately, there had already been a specialized thread of work in Computer Science to study stochastic systems, motivated by performance evaluation of real-time systems and networks: for the previous 10-15 years people had developed deep theories, methodologies, and analysis tools for stochastic and hybrid (discrete-continuous) computational systems. In the current phase of my work I am exploring the quantitative analysis of stochastic molecular systems via tools and theories, with collaborators at Microsoft, Oxford, and elsewhere [ 4 , 61 ].

Inventions

My work has normally led to publications rather than patents. 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 I devised an abstract machine that was well suited for functional language 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. [ 129 ]

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 has been introduced both in Java and in C#. I 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. [ 52 , 55 , 47 , 49 , A ]

Modula-3 Language Definition - Modula-3 was a very influential systems programming language until the advent of Java, which adopted 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 Digital Equipment Corporation. [ P ]

Distributed Lexical Scoping - Distributed lexical scoping, as embedded in the Obliq language, is a way to extend the notion of function "closure" to distributed environments. It extends the notions of Remote Procedure Call and code mobility. Obliq was widely used at Digital, and frequently cited, but was restricted to work within a network-based implementation of Modula-3 which was not easily exportable. [ 40 ]

Ambient Calculus - Ambient Calculus is 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". [ 91 , 32 ]

Spatial Logics - Arising from work on the Ambient Calculus, spatial logics 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 talking about distributed systems. The basic idea was initiated with Andy Gordon and Giorgio Ghelli (including a practical spinoff [ 27 ]), and was reapplied to standard process algebra with Luis Caires [ 83 , 80 ].

Modeling Languages for Dynamic Compartments - I introduced a formal language to model topological membrane transformation such as phagocytosis in a programmatic way [ 75 , 16 ]. This work is still far from applications, but the existing broad field of Membrane Computing quickly adopted these ideas, and we are beginning to use them in unexpected areas such as programming microfluidic devices that manipulate vesicles.

Two-domain DNA Strand Displacement - My main contribution to DNA nanotechnology has been a new architecture for synthetic DNA circuits [ 60 ]. It is structurally simpler than previous proposals, and hence is potentially more robust (this is currently being demonstrated by experiments). Secondly, it enables an entirely new manufacturing technology. Being the first circuit architecture that relies exclusively on double-stranded DNA (i.e., with no extra secondary structure), the DNA material can be produced by bacterial cloning, instead of by (artificial) DNA synthesis. The former leads to high quality natural DNA of practically arbitrary length, while the latter is technologically limited in the quality and the length of the DNA strands that can be obtained, and hence limits the complexity of the circuits.

Top-Ten Publications


i.       Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471-522, 1985. Cited by 2235
http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf

ii.       Luca Cardelli and Andrew D. Gordon. Mobile Ambients.Theoretical Computer Science. Vol 240/1, June 2000. pp 177-213. Cited by 1187 + Cited by 697
http://lucacardelli.name/Papers/MobileAmbients.A4.pdf

·       Most Influential ETAPS 1998 Paper Award (Awarded in 2007).

iii.       Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76(2/3): 138-164, 1988. Cited by 1212
http://lucacardelli.name/Papers/Inheritance.A4.pdf

iv.       Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.Cited by 836
http://lucacardelli.name/Papers/ExplicitSub.pdf

v.       Luca Cardelli. A language with distributed scope. Computing Systems, 8(1):27-59, January 1995. Cited by 720
http://lucacardelli.name/Papers/Obliq.A4.pdf

·       Most Influential POPL Paper Award 2005 (for POPL 1995)

vi.       Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, 1993. Cited by 551
http://lucacardelli.name/Papers/SRT.A4.pdf

vii.       Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, Ehud Shapiro. BioAmbients: An Abstraction for Biological Compartments. Theoretical Computer Science. Volume 325, Issue 1 , 28 September 2004, Pages 141-167. Elsevier. Cited by 435
http://lucacardelli.name/Papers/BioAmbients An Abstraction for Biological Compartments.pdf

viii.       Antonio Albano, Luca Cardelli, and Renzo Orsini. Galileo: a strongly typed, interactive, conceptual language. ACM Transactions on Database Systems (TODS), 10(2):230-260, 1985. Cited by 441
http://lucacardelli.name/Papers/Galileo.A4.pdf

ix.       Luca Cardelli. Brane Calculi - Interactions of Biological Membranes. V.Danos, V.Schachter Eds.: Computational Methods in Systems Biology. Lecture Notes in Computer Science, Vol 3082, Springer, 2005. ISBN 3-540-25375-0. pp 257-280. Cited by 392
http://lucacardelli.name/Papers/Brane Calculi CMSB LNCS.pdf

x.       Luca Cardelli and Andrew D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. Proceedings of the 27th ACM Symposium on Principles of Programming Languages, 2000. pp 365-377. Cited by 382
http://lucacardelli.name/Papers/AnytimeAnywhere.A4.pdf

·         Most Influential POPL Paper Award 2010 (for POPL 2000)


Publications


Books


Technical Monographs

A.       Martín Abadi and Luca Cardelli. A Theory of Objects. Springer, 1996.


Edited Collections

B.       Luca Cardelli, William Shih (Eds). DNA Computing and Molecular Programming. (Proceedings) Lecture Notes in Computer Science 6937, Springer, 2011.

C.       Luca Cardelli, Marcelo Fiore, Glynn Winskel (Eds.). Computation Meaning and Logic: Articles dedicated to Gordon Plotkin. Electronic Notes in Theoretical Computer Science 172, 2007.

D.       Luca Cardelli (Ed.). ECOOP 2003 - Object-Oriented Programming. (Proceedings) 17th European Conference, Lecture Notes in Computer Science 2743, Springer, 2003.

E.        Henri E. Bal, Boumediene Belkhouche, and Luca Cardelli (Eds.). Internet Programming Languages. Lecture Notes in Computer Science 1686, Springer, 1999.

F.        Luca Cardelli (Ed.). POPL'98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. (Proceedings) ACM Press, 1998.


Book Chapters

G.       Luca Cardelli, Corrado Priami. Visualization in Process Algebra Models of Biological Systems. In: Tony Hey, Stewart Tansley, Kristin Tolle, Eds. The Fourth Paradigm: Data Intensive Scientific Discovery. Creative Commons Attribution Share Alike License, pp 99-105, October 2009.

H.       Luca Cardelli. Can a Systems Biologist Fix a Tamagotchi? In: Yves Bertot, Gérard Huet, Jean-Jacques Lévy, Gordon Plotkin (Eds.). From Semantics to Computer Science - Essays in Honour of Gilles Khan, Chapter 23, pp 517-528. Cambridge University Press, 2009. ISBN 978-0-521-51825-3.

I.         Luca Cardelli. Artificial Biochemistry. In: A.Condon, D.Harel, J.N.Kok, A.Salomaa, E.Winfree (Eds.). Algorithmic Bioprocesses. Springer 2009. DOI: 10.1007/978-3-540-88869-7_22. ISBN: 978-3-540-88868-0.

J.         Luca Cardelli. Bioware Languages. In: Andrew Herbert, Karen Sparck Jones (Eds.). Computer Systems: Theory, Technology, and Applications - A Tribute to Roger Needham, Monographs in Computer Science. Springer 2004. ISBN 0-387-20170-X. pp 59-65.

K.       Luca Cardelli. Type systems. In: Allen B. Tucker (Ed.). The Computer Science and Engineering Handbook. CRC Press, 2004. Chapter 97. Allen B. Tucker (Ed.). The Computer Science and Engineering Handbook. CRC Press, 1997, ISBN: 0-8493-2909-4. Chapter 103.

L.        Luca Cardelli. Mobility and Security. In: Friedrich L. Bauer and Ralf Steinbrggen (Eds.). Foundations of Secure Computation. Proceedings of the NATO Advanced Study Institute on Foundations of Secure Computation. IOS Press, 2000. ISBN 1 58603 015 9. pp. 3-37.

M.     Luca Cardelli. Mobile Computation. In: J. Vitek and C. Tschudin (Eds.). Mobile Object Systems - Towards the Programmable Internet. Lecture Notes in Computer Science, Vol. 1222, Springer, 1997. pp 3-6.

N.       Krishna Bharat and Luca Cardelli. Migratory Applications. In: J. Vitek and C. Tschudin E(Eds.). Mobile Object Systems - Towards the Programmable Internet. Lecture Notes in Computer Science, Vol. 1222, Springer, 1997. pp 131-148.

O.      Luca Cardelli. Extensible records in a pure calculus of subtyping. In: C.A. Gunter and J.C. Mitchell (Eds.). Theoretical Aspects of Object-Oriented Programming. MIT Press, 1994. pp 373-425.

P.       Luca Cardelli, James Donahue, Lucille Glassman, Mick Jordan, Bill Kalsow, and Greg Nelson. [Modula-3] Language definition. In: Greg Nelson (Ed.). System Programming with Modula-3. Prentice Hall, ISBN 0-13-590464-1.1991. Chapter 2, pp 11-66.

Q.      Luca Cardelli. Typeful programming. E. J. Neuhold and M. Paul, Editors. Formal Description of Programming Concepts, IFIP State of the Art Reports Series. Springer-Verlag, February 1989.

R.       Luca Cardelli. Amber. In: Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet (Eds.). Combinators and Functional Programming Languages, Lecture Notes in Computer Science, Vol. 242, pp 21-70. Springer-Verlag, 1986.

S.        Luca Cardelli. The amber machine. In: Guy Cousineau, Pierre-Louis Curien, and Bernard Robinet (Eds.). Combinators and Functional Programming Languages, Lecture Notes in Computer Science, Vol. 242, pp 21-70. Springer-Verlag, 1986.


Journal ARTICLES


1.       Luca Cardelli, Philippa Gardner. Processes in Space. Theoretical Computer Science, Volume 431, 2012, pp. 40-55. DOI: 10.1016/j.tcs.2011.12.051.

2.       Alessandro Romanel, Lars Juhl Jensen, Luca Cardelli, Attila Csikász-Nagy. Transcriptional Regulation is a Major Controller of Cell Cycle Transition Dynamics. PLoS ONE 7(1): e29716. doi:10.1371/journal.pone.0029716. 2012.

3.       Ozan Kahramanoğulları, Luca Cardelli, Emmanuelle Caron.An Intuitive Modelling Interface for Systems Biology. International Journal of Software and Informatics, ISSN 1673-7288. 2012. (In press.)

4.       Matthew R. Lakin, David Parker, Luca Cardelli, Marta Kwiatkowska, Andrew Phillips. Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking.Journal of the Royal Society Interface, J R Soc Interface 2012;9 1470-1485, doi: 10.1098/rsif.2011.0800.

5.       Luca Cardelli. Two-Domain DNA Strand Displacement. Mathematical Structures in Computer Science. In press. 2012.

6.       Neil Dalchau, Andrew Phillips, Leonard D. Goldstein, Mark Howarth, Luca Cardelli, Stephen Emmott, Tim Elliott, Joern M. Werner. A Peptide Filtering Relation Quantifies MHC Class I Peptide Optimization. PLoS Computational Biology 7(10): e1002144. doi:10.1371/journal.pcbi.1002144. 2011.

7.       Luca Cardelli. Strand Algebras for DNA Computing. Natural Computing 10(1) p. 407-428, 2011. DOI: 10.1007/s11047-010-9236-7.

8.       Attila Csikász-Nagy, Luca Cardelli, Orkun S Soyer. Response Dynamics of Phosphorelays Suggest Their Potential Utility in Cell Signaling. Journal of the Royal Society Interface. 6 April 2011 vol. 8 no. 57 480-488. Published Online August 11, 2010. doi: 10.1098/rsif.2010.0336.

9.       Luca Cardelli, Cosimo Laneve. Reversibility in Massive Concurrent Systems. Scientific Annals of Computer Science 21(2) 175-198, A.I. Cuza University Press, 2011.

10.    Luca Cardelli, Gianluigi Zavattaro. Turing Universality of the Biochemical Ground Form. Mathematical Structures in Computer Science, 20(1):45-73, February 2010. DOI 10.1017/S0960129509990259.

11.    Dennis Y.Q. Wang, Luca Cardelli, Andrew Phillips, Nir Piterman, Jasmin Fisher. Computational Modeling of the EGFR Network Elucidates Control Mechanisms Regulating Signal Dynamics. BMC Systems Biology 2009, 3:118. doi:10.1186/1752-0509-3-118.

12.    Andrew Phillips, Luca Cardelli. A Programming Language for Composable DNA Circuits.Journal of the Royal Society Interface, August 6, 2009 6:S419-S436. Published Online 17 June 2009 DOI: 10.1098/rsif.2009.0072.focus.

13.    Luca Cardelli, Emmanuelle Caron, Philippa Gardner, Ozan Kahramanoğulları, Andrew Phillips. A Process Model of Actin Polymerisation. Electronic Notes in Theoretical Computer Science (ENTCS) 229(1) February 2009, 127-144.

14.    Luca Cardelli, Emmanuelle Caron, Philippa Gardner, Ozan Kahramanoğulları, Andrew Phillips. A Process Model of Rho GTP-binding Proteins. Theoretical Computer Science. DOI 10.1016/j.tcs.2009.04.029. 2009.

15.    Luca Cardelli. On Process Rate Semantics. Theoretical Computer Science 391(3) 190-215, Elsevier, 2008. DOI: <http://dx.doi.org/10.1016/j.tcs.2007.11.012>

16.    Luca Cardelli. Bitonal Membrane Systems - Interactions of Biological Membranes. Theoretical Computer Science 404(1-2), Elsevier, September 2008, pp. 5-18. DOI: <http://dx.doi.org/10.1016/j.tcs.2008.04.016>

17.    Ralf Blossey, Luca Cardelli, Andrew Phillips. Compositionality, Stochasticity and Cooperativity in Dynamic Models of Gene Regulation. HFSP Journal, 2(1):17–28 February 2008.

18.    Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. L.Cardelli. Manipulating Trees with Hidden Labels. M.Fiore, G.Winskel (Eds.) ENTCS Electronic Notes in Theoretical Computer Science, Vol 172, 2007. pp. 177-201.

19.    Andrew Phillips, Luca Cardelli, Giuseppe Castagna. A Graphical Representation for Biological Processes in the Stochastic Pi-calculus. Transactions on Computational Systems Biology VII - Lecture Notes in Computer Science, Vol 4230, Springer 2006, ISBN: 978-3-540-48837-8, pp 123-152.

20.    Ralf Blossey, Luca Cardelli, Andrew Phillips. A Compositional Approach to the Stochastic Dynamics of Gene Networks. Transactions on Computational Systems Biology IV - Lecture Notes in Computer Science, Vol 3939, Springer 2006, ISBN: 3-540-33245-6, pp 99-122.

21.    Luca Cardelli, Gheorghe Păun.A Universality Result for a (Mem)Brane Calculus Based on Mate/Drip Operations. International Journal of Foundations of Computer Science, 17(1), pp 49-68. World Scientific Publishing Company. 2006.

22.    Luca Cardelli. Abstract Machines of Systems Biology. Transactions on Computational Systems Biology. III, LNBI 3737, pp 145-168, Springer 2005.

23.    Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon. Deciding Validity in a Spatial Logic for Trees. Journal of Functional Programming, Vol 15, pp 543-572. Cambridge University Press, 2005.

24.    Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon.Secrecy and Group Creation. Information and Computation, Volume 196, Issue 2, January 2005, Pages 127-155.

25.    Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, Ehud Shapiro. BioAmbients: An Abstraction for Biological Compartments. Theoretical Computer Science. Volume 325, Issue 1 , 28 September 2004, Pages 141-167. Elsevier.

26.    Luis Caires and Luca Cardelli. A Spatial Logic for Concurrency (Part II). Theoretical Computer Science, 322(3) pp. 517-565, September 2004.

27.    Luca Cardelli, Giorgio Ghelli.TQL: A Query Language for Semistructured Data Based on the Ambient Logic. Mathematical Structures in Computer Science. Vol 14. Cambridge University Press. 2004. pp 285-327.

28.    Nick Benton, Luca Cardelli, Cedric Fournet. Modern Concurrency Abstractions for C#. ACM Transactions on Programming Languages and Systems (TOPLAS) 26(5), 2004. pp.269-804.

29.    Luis Caires and Luca Cardelli. A Spatial Logic for Concurrency (Part I). Information and Computation, Vol 186/2 November 2003. pp 194-235.

30.    Andrew D. Gordon and Luca Cardelli. Equational Properties of Mobile Ambients. Mathematical Structures in Computer Science 13(3):371-408, June 2003.

31.    Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Types for the Ambient Calculus. Information and Computation, 177(2), 2002. pp. 160-194.

32.    Luca Cardelli and Andrew D. Gordon. Mobile Ambients. Theoretical Computer Science. Vol 240/1, June 2000. pp 177-213.

33.    Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. Comparing Object Encodings. Information and Computation.Vol. 155, No. 1/2, Dec 1999, pp. 108-133.

34.    Luca Cardelli and Rowan Davies. Service Combinators for Web Computing. IEEE Transactions on Software Engineering, Vol 25, No 3, May-June 1999. pp 309-316.

35.    Luca Cardelli. Bad engineering properties of object-oriented languages. ACM Computing Surveys, 28(4es), Article 150. 1996.

36.    Martín Abadi and Luca Cardelli. On subtyping and matching. ACM Transactions on Programming Languages and Systems, 18(4):401-423, 1996.

37.    Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. Information and Computation, 125(2):78-102, March 1996.

38.    Luca Cardelli. Type systems. ACM Computing Surveys, 28(1):263-264, 1996.

39.    Luca Cardelli. Global computation. ACM Computing Surveys, 28(4es), Article 163. 1996.

40.    Luca Cardelli. A language with distributed scope. Computing Systems, 8(1):27-59, January 1995.

41.    Kim Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221-242, 1995.

42.    Martín Abadi and Luca Cardelli. An imperative object calculus. Theory and Practice of Object Systems, 1(3):151-166, 1995.

43.    Martín Abadi and Luca Cardelli. A theory of primitive objects: Second-order systems. Science of Computer Programming, 25(2-3):81-116. December 1995.

44.    Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. Dynamic typing in polymorphic languages. Journal of Functional Programming, 5(1):111-130, January 1995.

45.    Luca Cardelli, John C. Mitchell, Simone Martini, and Andre Scedrov. An extension of system F with subtyping. Information and Computation, 109(1/2):4-56, February 1994.

46.    Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. Formal parametric polymorphism. Theoretical Computer Science, 121(1-2):9-58: 1993.

47.    Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575-631, 1993.

48.    Luca Cardelli and Giuseppe Longo. A semantic basis for Quest. Journal of Functional Programming, 1(4):417-458, October 1991.

49.    Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, October 1991.

50.    Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon D. Plotkin. Dynamic typing in a statically-typed language. ACM Transactions on Programming Languages and Systems, 13(2):237-268, April 1991.

51.    Luca Cardelli and John C. Mitchell. Operations on records. Mathematical Structures in Computer Science, 1(1):3-48, 1991.

52.    Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76(2/3): 138-164, 1988.

53.    Luca Cardelli. Basic polymorphic typechecking. Science of Computer Programming, 8(2): 147-172, 1987.

54.    Antonio Albano, Luca Cardelli, and Renzo Orsini. Galileo: a strongly typed, interactive, conceptual language. ACM Transactions on Database Systems (TODS), 10(2):230-260, 1985.

55.    Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471-522, 1985.


Refereed-Conference ARTICLES

In Computer Science many articles first appear in refereed conference proceedings. Many workshops (including all the ones listed below) are also formally refereed. Extended versions of those articles are then published in journals. These extended versions contain ‘significant’ new material (a requirement of the journals), are independently re-refereed, and are subject to a separate copyright; hence they are technically separate publications while often bearing the same title.

Conference articles later extended and published in journals (which are listed above) are indicated below in parentheses.

56.    Luca Cardelli, Kim Larsen, Radu Mardare. Modular Markovian Logic. ICALP '11. Proceedings of the 38th international conference on Automata, languages and programming. Vol II, 380-391. Springer 2011. ISBN: 978-3-642-22011-1.

57.    Luca Cardelli, Radu Mardare. Continuous Markovian Logic. Computer Science Logic: 25th International Workshop / 20th Annual Conference of the EACSL (CSL 2011). Schloss Dagstuhl Leibniz-Zentrum für Informatik 2011. pp 144-158. ISBN (print) 978-3-939897-32-3. ISBN (electronic) 978-3-939897-32-3.

58.    Luca Cardelli, Cosimo Laneve. Reversible Structures. Proceedings of 9th Int. Conf. on Computational Methods in Systems Biology (CMSB 2011), ACM Digital Library, 2011. 131-140. Doi:10.1145/2037509.2037529.

59.    Luca Cardelli, Philippa Gardner. (Processes in Space.) F.Ferreira, B.Löwe, E.Mayordomo, L.M.Gomes (Eds.). Programs, Proofs, Processes: 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June/July 2010, Proceedings. LNCS 6158, pp. 78-87, Springer 2010.

60.    Luca Cardelli. (Two-Domain DNA Strand Displacement.) In S. B. Cooper, E. Kashefi, P. Panangaden (Eds.): Developments in Computational Models (DCM 2010). EPTCS 26, 2010, pp. 47-61, doi:10.4204/EPTCS.26.5. June 2010.

61.    Luca Cardelli, Radu Mardare. The Measurable Space of Stochastic Processes. Seventh International Conference on the Quantitative Evaluation of Systems, QEST 2010, Williamsburg, VA, USA September 15-18. IEEE Publishing, ISBN: 978-0-7695-4188-4, pp 171-180, 2010.

62.    Luca Cardelli. (Strand Algebras for DNA Computing.)DNA Computing and Molecular Programming. 15th International Conference, DNA 15, Fayetteville, AR, USA, June 2009, Revised Selected Papers. LNCS 5877, Springer, October 2009, pp 12-24.

63.    Ozan Kahramanoğulları, Luca Cardelli, Emmanuelle Caron. (An Intuitive Modelling Interface for Systems Biology.) Developments in Computational Models 2009. EPTCS 9, pp. 73-86, 2009. http://arxiv.org/abs/0911.2327.

64.    Luca Cardelli. Molecules as Automata (Extended Abstract). In: A.Corradini, U.Montanari (Eds.). Recent Trends in Algebraic Development Techniques, 19th International Workshop, WADT 2008, Pisa 13-16 June 2008. Lecture Notes in Computer Science 5486, Springer, June 2009.

65.    Luca Cardelli, Emmanuelle Caron, Philippa Gardner, Ozan Kahramanoğulları, Andrew Phillips. (A Process Model of Actin Polymerisation.) From Biology to Concurrency and back, FBTC 2008, Satellite Workshop of ICALP 2008, July 2008, Reykjavik.

66.    Gianluigi Zavattaro, Luca Cardelli. Termination Problems in Chemical Kinetics. In F.van Breugel, M.Chechik (Eds.) CONCUR 2008 - Concurrency Theory, 19th International Conference, Toronto, Canada, August 2008. LNCS 5201, pp 477-491, Springer 2008.

67.    Luca Cardelli, Gianluigi Zavattaro. On the Computational Power of Biochemistry. Third International Conference on Algebraic Biology, AB 2008, July 2008, Linz.

68.    Luca Cardelli, Philippa Gardner, Ozan Kahramanoğulları. A Process Model of Rho GTP-binding Proteins in the Context of Phagocytosis. Proc. From Biology To Concurrency and back, Lisbon 8 Sep 2007 in conjunction with Concur 2007. ENTCS 194(3):87-102, Elsevier, 2008. <doi:10.1016/j.entcs.2007.12.007>

69.    S. van Bakel, L. Cardelli and M.G. Vigliotti.From X to Pi: Representing Classical Sequent Calculus in Pi-calculus. International Workshop on Classical Logic and Computation (CL&C'08), Reykjavik, Iceland, July 2008.

70.    Luca Cardelli. From Processes to ODEs by Chemistry. Fifth IFIP International Conference on Theoretical Computer Science, TCS 2008, 261-281, Milan, September 2008. ISBN: 978-0-387-09679-7. DOI: <http://dx.doi.org/10.1007/978-0-387-09680-3_18>

71.    Andrew Phillips, Luca Cardelli. Efficient, Correct Simulation of Biological Processes in Stochastic Pi-calculus. Proc. Computational Methods in Systems Biology, CMSB 2007, Edinburgh, September 2007. LNBI 4695, 184-199, Springer 2007.

72.    Luca Cardelli. A Process Algebra Master Equation. Fourth International Conference on the Quantitative Evaluation of Systems, QEST 2007, Edinburgh, September 2007. IEEE Publishing, ISBN: 978-0-7695-2883-0, pp 219-224, 2007.

73.    Andrew Phillips, Luca Cardelli. A Graphical Representation for the Stochastic Pi-calculus. Proceedings of Concurrent Models in Molecular Biology (Bioconcur'05), affiliated with CONCUR'05. 2005.

74.    Luca Cardelli, Sylvain Pradalier. Where Membranes Meet Complexes. Proceedings of Concurrent Models in Molecular Biology (Bioconcur'05), affiliated with CONCUR'05. 2005.

75.    Luca Cardelli. Brane Calculi - Interactions of Biological Membranes. V.Danos, V.Schachter Eds.: Computational Methods in Systems Biology. International Conference CMSB 2004, Paris, France, May 2004, Revised Selected Papers. Lecture Notes in Computer Science, Vol 3082, Springer, 2005. ISBN 3-540-25375-0. pp 257-280.

76.    Alain Frisch and Luca Cardelli. Greedy Regular Expression Matching. Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 12-16, 2004. Lecture Notes in Computer Science 3142. Springer 2004.ISBN 3-540-22849-7. pp. 618-629.

77.    Andrew Phillips, Luca Cardelli. A Correct Abstract Machine for the Stochastic Pi-calculus. Proceedings of Concurrent Models in Molecular Biology (Bioconcur'04), affiliated with CONCUR'04. 2004.

78.    Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. (Manipulating Trees with Hidden Labels.) Andrew D. Gordon (Ed.) Foundations of Software Science and Computational Structures. 6th International Conference, FOSSACS 2003. Lecture Notes in Computer Science 2620. Springer, 2003. ISBN 3-540-00897-7. pp 216-232.

79.    Cristiano Calcagno, Luca Cardelli, Andrew D. Gordon. (Deciding Validity in a Spatial Logic for Trees.) ACM Workshop on Types in Language Design and Implementation, TLDI'03, New Orleans, January 2003, ACM Press. pp 62-73.

80.    Luis Caires and Luca Cardelli. (A Spatial Logic for Concurrency (Part II)). Lubos Brim, Petr Jancar, Mojmir Kretinsky Antonin Kucera (Eds.). CONCUR 2002 - Concurrency Theory, 13th International Conference, Brno, Czech Republic, August 2002, Proceedings. Lecture Notes in Computer Science 2421, Springer, 2002, ISBN 3-540-44043-7. pp 209-225.

81.    Nick Benton, Luca Cardelli, Cedric Fournet. Modern Concurrency Abstractions for C#. Boris Magnusson (Ed.): ECOOP 2002 - Object-Oriented Programming, 16th European Conference. Lecture Notes in Computer Science 2374, Springer, 2002. ISBN 3-540-43759-2. pp. 415-440.

82.    Luca Cardelli, Philippa Gardner, and Giorgio Ghelli. A Spatial Logic for Querying Graphs. Peter Widmayer, Francisco Triguero, Rafael Morales, Matthew Hennessy, Stephan Eidenbenz, Ricardo Conejo (Eds.). Automata, Languages, and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 2002, Proceedings. Lecture Notes in Computer Science, Vol 2380, Springer, 2002. ISBN 3-540-43864-5. pp 597-610.

83.    Luis Caires and Luca Cardelli. (A Spatial Logic for Concurrency (Part I)). Naoki Kobayashi and Benjamin C. Pierce (Eds.). Theoretical Aspects of Computer Software; 4th International Symposium, TACS 2001, Sendai, Japan, October 2001, Proceedings. Lecture Notes in Computer Science 2215. Springer, 2001. ISBN 3 540 42736 8. pp 1-37.

84.    Luca Cardelli and Andrew D. Gordon. Logical Properties of Name Restriction. Samson Abramsky (Ed.). Typed Lambda Calculi and Applications. 5th International Conference, TLCA 2001, Krakow, Poland, May 2001, Proceedings. Lecture Notes in Computer Science, Vol. 2044, Springer, 2001. ISBN 3-540-41960-8. pp 46-60.

85.    Luca Cardelli, Giorgio Ghelli. A Query Language Based on the Ambient Logic. David Sands, Editor: Programming Languages and Systems, 10th European Symposium on Programming, ESOP 2001. Lecture Notes in Computer Science 2028, Springer, 2001. ISBN 3-540-41862-8. pp. 1-22.

86.    Luca Cardelli and Andrew D. Gordon. Anytime, Anywhere. Modal Logics for Mobile Ambients. Proceedings of the 27th ACM Symposium on Principles of Programming Languages, 2000. pp 365-377.

87.    Luca Cardelli. Semistructured Computation. Richard C. H. Connor, Alberto O. Mendelzon (Eds.): Research Issues in Structured and Semistructured Database Programming, 7th International Workshop on Database Programming Languages, DBPL'99. Lecture Notes in Computer Science 1949. Springer, 2000. ISBN 3-540-41481-9. pp. 1-16.

88.    Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Ambient Groups and Mobility Types. In Jan van Leeuwen, Osamu Watanabe, Masami Hagiya, Peter D. Mosses, Takayasu Ito (Eds.). Theoretical Computer Science, International Conference IFIP TCS 2000. Lecture Notes in Computer Science, Vol. 1872, Springer, 2000. ISBN 3-540-67823-9. pp. 333-347.

89.    Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon. (Secrecy and Group Creation.) Catuscia Palamidessi (Ed.). CONCUR 2000 - Concurrency Theory. 11th International Conference. Lecture Notes in Computer Science, Vol. 1877, Springer, 2000. ISBN 3-540-67897-2. pp. 365-379.

90.    Andrew D. Gordon and Luca Cardelli. (Equational Properties of Mobile Ambients.) Wolfgang Thomas, Editor. Foundations of Software Science and Computational Structures, Second International Conference, FOSSACS'99. Lecture Notes in Computer Science, Vol. 1578. Springer, 1999. ISBN 3-540-65719-3. pp 212-226.

91.    Luca Cardelli. Wide Area Computation. In: Jiri Wiedermann, Peter van Emde Boas, and Mogens Nielsen, Editors. Automata, Languagese and Programming, 26th International Colloquium, ICALP'99 Proceedings. Lecture Notes in Computer Science, Vol. 1644, Springer, 1999. ISBN 3-540-66224-3. pp. 10-24.

92.    Luca Cardelli, Giorgio Ghelli, and Andrew D. Gordon. Mobility Types for Mobile Ambients. Jiri Wiedermann, Peter van Emde Boas, and Mogens Nielsen, Editors. Automata, Languagese and Programming, 26th International Colloquium, ICALP'99. Lecture Notes in Computer Science, Vol. 1644, Springer, 1999. ISBN 3-540-66224-3. pp. 230-239.

93.    Luca Cardelli and Andrew D. Gordon. Types for Mobile Ambients. Proceedings of the 26th ACM Symposium on Principles of Programming Languages, 1999. pp 79-92.

94.    Luca Cardelli. Abstractions for Mobile Computation. Jan Vitek and Christian Jensen, Editors. Secure Internet Programming: Security Issues for Mobile and Distributed Objects. Lecture Notes in Computer Science, Vol. 1603, Springer, 1999. ISBN 3-540-66130-1. pp. 51-94.

95.    Luca Cardelli and Andrew D. Gordon. (Mobile Ambients.) Foundations of Software Science and Computational Structures, Maurice Nivat (Ed.), Lecture Notes in Computer Science, Vol. 1378, Springer, 1998. pp. 140-155.

96.    Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. (Comparing Object Encodings.) Martín Abadi, Takayasu Ito (Eds.): Theoretical Aspects of Computer Software, Third International Symposium, TACS '97. Lecture Notes in Computer Science, Vol. 1281, Springer, 1997, ISBN 3-540-63388-X. pp 415-438.

97.    Luca Cardelli and Rowan Davies. (Service Combinators for Web Computing.) First Usenix Conference on Domain Specific Languages, Santa Barbara, California, October 15-17, 1997.

98.    Luca Cardelli. Program fragments, linking, and modularization. POPL'97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1997, ISBN 0-89791-853-3. pp 266-277.

99.    Martín Abadi, Luca Cardelli, Ramesh Viswanathan. An interpretation of objects and object types. POPL'96: The 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1996, ISBN 0-89791-769-3. pp 396-409.

100. Martín Abadi and Luca Cardelli. (On subtyping and matching.) Walter G. Olthoff (Ed.): ECOOP'95 - Object-Oriented Programming, 9th European Conference. Lecture Notes in Computer Science, Vol. 952, Springer, 1995, ISBN 3-540-60160-0. pp 145-167.

101. Martín Abadi and Luca Cardelli. (An imperative object calculus.) Peter D. Mosses, Mogens Nielsen, Michael I. Schwartzbach: TAPSOFT'95: Theory and Practice of Software Development, 6th International Joint Conference CAAP/FASE. Lecture Notes in Computer Science, Vol. 915, Springer, 1995, ISBN 3-540-59293-8. pp 471-485.

102. Martín Abadi and Luca Cardelli. An imperative object calculus: Basic typing and soundness. SIPL '95 - Proceedings of the Second ACM SIGPLAN Workshop on State in Programming Languages. Department of Computer Science, University of Illinois at Urbana-Champaign, 1995.

103. Krishna Bharat and Luca Cardelli. (Migratory Applications.) ACM Symposium on User Interface Software and Technology '95, Pittsburgh, PA, November 1995. pp 133-142.

104. Krishna Bharat and Luca Cardelli. Distributed applications in a multimedia setting. First International Workshop on Hypermedia Design (IWHD'95), Montpellier, France, 1-2 June 1995. pp 185-192.

105. Luca Cardelli. (A language with distributed scope.) POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1995, ISBN 0-89791-692-1. pp 286-297.

106. Luca Cardelli, Florian Matthes, and Martín Abadi. Extensible grammars for language specialization. Catriel Beeri, Atsushi Ohori, Dennis Shasha(Eds.): Database Programming Languages (DBPL-4), Proceedings of the Fourth International Workshop on Database Programming Languages - Object Models and Languages. Springer 1994, ISBN 3-540-19853-9. pp 11-31.

107. Martín Abadi and Luca Cardelli. (A theory of primitive objects: Untyped and first-order systems.) Masami Hagiya, John C. Mitchell (Eds.): Theoretical Aspects of Computer Software, International Conference TACS '94. Lecture Notes in Computer Science, Vol. 789, Springer, 1994, ISBN 3-540-57887-0. pp 296-320.

108. Martín Abadi and Luca Cardelli. (A theory of primitive objects: Second-order systems.) Donald Sannella (Ed.): Programming Languages and Systems - ESOP'94, 5th European Symposium on Programming. Lecture Notes in Computer Science, Vol. 788, Springer 1994, ISBN 3-540-57880-3. pp 1-25.

109. Martín Abadi and Luca Cardelli. A semantics of object types. Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press, ISBN 0-8186-6310-3. pp 332-341.

110. Gordon D. Plotkin, Martín Abadi, and Luca Cardelli. Subtyping and parametricity. Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 1994. IEEE Computer Society Press, ISBN 0-8186-6310-3. pp 310-319.

111. Martín Abadi, Luca Cardelli, and Pierre-Louis Curien. (Formal parametric polymorphism.) Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, 1993. pp 157-170.

112. Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Didier Rémy. (Dynamic typing in polymorphic languages.) Proceedings of the ACM SigPlan Workshop on ML and its Applications, June 1992.

113. Luca Cardelli, John C. Mitchell, Simone Martini, and Andre Scedrov. (An extension of system F with subtyping.) Takayasu Ito, Albert R. Meyer (Eds.): Theoretical Aspects of Computer Software, TACS '91. Lecture Notes in Computer Science, Vol. 526, Springer, 1991, ISBN 3-540-54415-1. pp 750-770.

114. Roberto M. Amadio and Luca Cardelli. (Subtyping recursive types.) Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, January 1991. pp 104-118.

115. Luca Cardelli. A pure calculus of subtyping, and applications (outline). Paris C. Kanellakis, Joachim W. Schmidt (Eds.): Database Programming Languages: Bulk Types and Persistent Data. 3rd International Workshop. Morgan Kaufmann,1991. ISBN 1-55860-242-9. pp 185-187.

116. Luca Cardelli and Giuseppe Longo. (A semantic basis for Quest.) ACM Conference on LISP and Functional Programming. ACM Press. 1990.

117. Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. (Explicit substitutions.) Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, January 1990. pp 31-46.

118. Luca Cardelli and Xavier Leroy. Abstract types and the dot notation. Programming Concepts and Methods, IFIP State of the Art Reports. TC2 Working Conference. North Holland, 1990. pp 479-504.

119. Martín Abadi, Luca Cardelli, Benjamin C. Pierce, and Gordon D. Plotkin. (Dynamic typing in a statically-typed language.) Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989. pp 213-227.

120. Luca Cardelli and John C. Mitchell. (Operations on records.) Mathematical Foundations of Programming Semantics, 5th International Conference. Lecture Notes in Computer Science, Vol. 442, Springer, 1990.

121. Luca Cardelli, James Donahue, Mick Jordan, Bill Kalsow, and Greg Nelson.The Modula-3 Type System. Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, January 1989. pp 202-212.

122. Luca Cardelli. Types for data-oriented languages. Joachim W. Schmidt, Stefano Ceri, Michele Missikoff (Eds.): Advances in Database Technology - EDBT'88. Proceedings of the International Conference on Extending Database Technology. Lecture Notes in Computer Science, Vol. 303, Springer, 1988, ISBN 3-540-19074-0 and 0-387-19074-0. pp 1-15.

123. Luca Cardelli. Building user interfaces by direct manipulation. ACM SIGGRAPH Symposium on User Interface Software, Banff, Alberta, Canada, October 17-19, 1988. ACM Press, ISBN 0-89791-283-7. pp 152-166.

124. Luca Cardelli. Structural subtyping and the notion of power type. Fifteenth Annual ACM Symposium on Principles of Programming Languages. ACM Press, 1988. pp 70-79.

125. Luca Cardelli, David B. MacQueen. Persistence and Type Abstraction. Malcolm P. Atkinson, Peter Buneman, Ronald Morrison (Eds.): Data Types and Persistence. Edited Papers from the Proceedings of the First Workshop on Persistent Objects. Springer 1988, ISBN 3-540-18785-5. pp 31-41.

126. Luca Cardelli. Typechecking dependent types and subtypes. Workshop on Foundations of Logic and Functional Programming. Lecture Notes in Computer Science, Vol. 306, pp 45-57. Springer-Verlag, December 1986.

127. Luca Cardelli and Rob Pike. Squeak: a language for communicating with mice. Twelfth ACM Annual Conference on Computer Graphics and Interactive Techniques (SIGGRAPH), 1985.

128. Luca Cardelli. An implementation model of rendezvous communication. S.D. Brookes, A.W. Roscoe and G. Winskel. Seminar on Concurrency. Lecture Notes in Computer Science, Vol. 197, Springer-Verlag, 1985, ISBN 3-540-15670-4. pp 449-457.

129. Luca Cardelli. Compiling a functional language. ACM Symposium on Lisp and Functional Programming, 1984.

130. Luca Cardelli. (A semantics of multiple inheritance.) G. Kahn, D.B. MacQueen and G. Plotkin Eds. Semantics of Data Types, International Symposium. Lecture Notes in Computer Science, Vol. 173, Springer-Verlag, 1984, ISBN 3-540-13346-1. pp 51-67.

131. Luca Cardelli. Two-dimensional syntax for functional languages.Pierpaolo Degano and Erik Sandewall, editors, Integrated Interactive Computing Systems. Proceedings of the European Conference on Integrated Interactive Computing Systems, ECICS 82. North Holland, ISBN 0-444-86595-0, 1983. pp 139-151.

132. Luca Cardelli. Real time agents. Mogens Nielsen, Erik Meineche Schmidt (Eds.): Automata, Languages and Programming, 9th Colloquium. Lecture Notes in Computer Science, Vol. 140, Springer, 1982, ISBN 3-540-11576-5. pp 94-106.

133. Luca Cardelli and Gordon D. Plotkin. An algebraic approach to VLSI design. John P. Gray (Ed.). VLSI 81, First International Conference on Very Large Scale Integration, University of Edinburgh, August 18-21, 1981. Academic Press, ISBN 0-12-296860-3. pp 173-182.

134. Luca Cardelli. Analog processes. P. Dembinski (Ed.): Mathematical Foundations of Computer Science (MFCS'80), Proceedings of the 9th Symposium. Lecture Notes in Computer Science, Vol. 88, Springer 1980, ISBN 3-540-10027-X. pp 181-193.