Luca Cardelli has a Ph.D. in computer science from the University of Edinburgh. He worked at Bell Labs, Murray Hill, from 1982 to 1985, and at Digital Equipment Corporation, Systems Research Center in Palo Alto, from 1985 to 1997, before assuming a position at Microsoft Research, in Cambridge UK, where he was head of the Programming Principles and Tools and Security groups until 2012. Since 2014, he has also been a Royal Society Research Professor at the University of Oxford.

His main interests are in programming languages and concurrency, and more recently in programmable biology and nanotechnology. He is a Fellow of the Royal Society, a Fellow of the Association for Computing Machinery, an Elected Member of the Academia Europaea, and an Elected Member of the Association Internationale pour les Technologies Objets.


Modelling Immune System Processes

Established: June 1, 2009

Immunodominance lies at the heart of the immune system's ability to distinguish self from non-self. Understanding and possibly controlling the mechanisms that govern immunodominance will have profound consequences for the fight against several classes of diseases, including viral infections and cancer. We have been attempting to understand the computation performed by the immune system that gives rise to immunodominance, using techniques from computer science, applied mathematics and Bayesian statistics.    

Programming DNA Circuits

Established: February 7, 2009

Molecular devices made of nucleic acids show great potential for applications ranging from bio-sensing to intelligent nanomedicine. They allow computation to be performed at the molecular scale, while also interfacing directly with the molecular components of living systems. They form structures that are stable inside cells, and their interactions can be precisely controlled by modifying their nucleotide sequences. However, designing correct and robust nucleic acid devices is a major challenge, due to high system complexity…

Stochastic Pi Machine

Established: November 21, 2008

The Stochastic Pi Machine (SPiM) is a programming language for designing and simulating computer models of biological processes. The language is based on a mathematical formalism known as the pi-calculus, and the simulation algorithm is based on standard kinetic theory of physical chemistry. The language features a simple graphical notation for modelling a range of biological systems, and can be used to model large systems incrementally, by directly composing simpler models of subsystems


Established: April 8, 2004

Cω is a research programming language. It is pronounced "c" followed by " -mg, -mg". It can be written (and searched for) as Cw or the "Comega language". Cω is a strongly typed, data oriented programming language that bridges the gap between between semi-structured hierarchical data (XML), relational data (SQL), and the .NET Common Type System (CTS). In Cω, the seemingly different worlds of XML, SQL and CTS are bridged and connected through generalization, not…













Bioware Languages
Luca Cardelli, in Computer Systems: Theory, Technology, and Applications - A Tribute to Roger Needham, Springer, January 1, 2004, View abstract


Manipulating Trees with Hidden Labels
Luca Cardelli, Philippa Gardner, Giorgio Ghelli, in Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, Springer, January 1, 2003, View abstract


A Spatial Logic for Querying Graphs
Luca Cardelli, Philippa Gardner, Giorgio Ghelli, in Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, Springer, January 1, 2002, View abstract


A Spatial Logic for Concurrency
Luís Caires, Luca Cardelli, in Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings, Springer, January 1, 2001, View abstract


Wide Area Computation
Luca Cardelli, in V Jornadas Ingeniería de Software y Bases de Datos (JISBD 2000), 8, 9 y 10 de noviembre, Valladolid, Universidad de Valladolid, Departamento de Informática, January 1, 2000, View abstract, Download PDF


Foundations for Wide-Area Systems (Tutorial)
Luca Cardelli, in Formal Methods for Open Object-Based Distributed Systems, IFIF TC6/WG6.1 Third International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), February 15-18, 1999, Florence, Italy, Kluwer, January 1, 1999, View abstract



Mobile Computation
Luca Cardelli, in Mobile Object Systems: Towards the Programmable Internet, Springer-Verlag: Heidelberg, Germany, January 1, 1997, View abstract



On Binary Methods
Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, Benjamin Pierce, in Theory and Practice of Object Systems, John, Wiley and Sons, Inc., January 1, 1995, View abstract


Subtyping and Parametricity
Gordon Plotkin, Martin Abadi, Luca Cardelli, in Proc. of 9th Ann. IEEE Symp. on Logic in Computer Science, LICS'94, Paris, France, 4–7 July 1994, IEEE Computer Society Press, January 1, 1994, View abstract




An Extension of System F with Subtyping
Luca Cardelli, John C. Mitchell, Simone Martini, Andre Scedrov, in Information and Computation, Proc. of 1st Int. Symp. on Theor. Aspects of Computer Software, TACS'91, Sendai, Japan, 24–27 Sept 1991, Springer-Verlag, January 1, 1991, View abstract
Operations on records
Luca Cardelli, J. C. Mitchell, in Math. Structures in Computer Science, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, The MIT Press, January 1, 1991, View abstract


Explicit Substitutions
Martin Abadi, Luca Cardelli, Pierre-Louis Curien, Jean-Jacques Lèvy, in Journal of Functional Programming, Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, ACM, January 1, 1990, View abstract


The Modula-3 Type System
Luca Cardelli, Jim E. Donahue, Mick Jordan, Bill Kalsow, Greg Nelson, in Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, January 1, 1989, View abstract







FS2PV: A Cryptographic-Protocol Verifier for F#

February 2007

FS2PV is a verification tool that compiles cryptographic-protocol implementations in a first-order subset of F# to a formal pi-calculus model. This pi-calculus model then can be analyzed using ProVerif to prove the desired security properties or to find security flaws.

Size: 2 MB

    Click the icon to access this download

  • Website

TulaFale: A Security Tool for Web Services

May 2006

TulaFale is a new specification language for writing machine-checkable descriptions of SOAP-based security protocols and their properties. TulaFale is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals…

Size: 2 MB

    Click the icon to access this download

  • Website

Comega compiler preview

October 2004

Comega is an experimental language which extends C# with new constructs for relational and semi-structured data access and asynchronous concurrency.

Size: 4 MB

    Click the icon to access this download

  • Website