Formal molecular biology

A language of formal proteins, the K-calculus, is introduced. Interactions are modeled at the domain level, bonds are represented by means of shared names, and reactions are required to satisfy a causality requirement of monotonicity. An example of a simplified signalling pathway is introduced to illustrate how standard biological events can be expressed in our protein language. A, more comprehensive example, the lactose operon, is also developed, bringing some confidence in the formalism considered as a modeling language. Then a finer-grained concurrent model, the mk-calculus, is considered, where interactions have to be at most binary. We show how to embed the coarser-grained language in the latter, a property which we call self-assembly. Finally we show how the finer-grained language can itself be encoded in pi-calculus, a standard foundational language for concurrency theory. (C) 2004 Published by Elsevier B.V.