Algebras and Languages for Molecular Programming

Luca Cardelli - Microsoft Research, Cambridge UK

Abstract: Nucleic acids (DNA/RNA) encode information digitally, and are currently the only truly 'user-programmable' entities at the molecular scale. They can be used to manufacture nano-scale structures, produce physical forces, act as sensors and actuators, and do computation in between. Eventually we will be able to interface then with biological machinery to detect and cure diseases at the cellular level under program control. The technology to create and manipulate them has existed for many years, but the imagination necessary to exploit them has been evolving slowly. Recently, some very simple computational schemes have been developed that are autonomous (run on their own once started) and involve only short (easily synthesizable) DNA strands with no other complex molecules.

We need programming abstractions and tools that are suitable for molecular programming. Low-level molecular design is required to produce molecules that interact in the desired controllable ways. On that basis one can then design various kinds of 'logic gates' and 'computational architectures', which is where much of the imagination is currently needed. Then one needs programming languages both at the level of gate implementation (Andrew Phillips in Cambridge has built a strand-level DNA language and simulator), and at the level of circuit implementation (I will describe a Strand Algebra for implementing e.g. automata and Petri nets). Since DNA computation is massively concurrent, some tricky and yet familiar issues arise, like having to formally verify gate designs to avoid subtle deadlocks and race conditions, and having to design high-level languages that exploit concurrency and stochasticity.

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

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 Ambient Calculus and Spatial Logics, which indirectly led to a current interest in Systems Biology and stochastic systems.

He is a Fellow of the Royal Society, an ACM Fellow, and an Elected Member of the Academia Europaea.