[TYPES] "Proofs of life"

[Rene Vestergaard]

"Proofs of life: molecular-biology reasoning simulates cell behaviors 
from first principles" is now available at http://arxiv.org/abs/1811.02478

The work springs from computer-verified reasoning and establishes wider 
utility by means of a reasoning-computation correspondence, including 
for long-standing critical problems in biology that have defied standard 
approaches.

Sincerely,
Rene

PS! The relevance to the types list is in "reasoning-computation 
correspondence". The work is non-standard type theory.

-----

ESSENCE
Mathematics-style correctness works for molecular biology and enables 
phenotype and life-cycle prediction from genotypes. Formally, 
reductionist science involves constructive reasoning, i.e., executable 
simulation.

SIGNIFICANCE
Axiomatic reasoning provides an alternative perspective that allows us 
to address long-standing open problems in biology. Our approach is 
supported by meta-theory and likely applies to any reductionist discipline.

ABSTRACT
Science relies on external correctness: statistical analysis and 
reproducibility, with ready applicability but inherent false 
positives/negatives. Mathematics uses internal correctness: conclusions 
must be established by detailed reasoning, with high confidence and deep 
insights but not necessarily real-world significance. Here, we formalize 
the molecular-biology reasoning style; establish that it constitutes an 
executable first-principle theory of cell behaviors that admits 
predictive technologies, with a range of correctness guarantees; and 
show that we can fully account for the standard reference: Ptashne, A 
Genetic Switch. Everything works for principled reasons and is presented 
within an open-ended meta-theoretic framework that seemingly applies to 
any reductionist discipline. The framework is adapted from a 
century-long line of work on mathematical reasoning. The key step is to 
not admit reasoning based on an external notion of truth but work only 
with what can be justified from considered assumptions. For molecular 
biology, the induced theory involves the concurrent running/interference 
of molecule-coded elementary processes of physiology change over the 
genome. The life cycle of the single-celled monograph organism is 
predicted in molecular detail as the aggregate of the possible 
sequentializations of the coded-for processes. The difficult question of 
molecular coding, i.e., the specific means of gene regulation, is 
addressed via a detailed modeling methodology. We establish a 
complementary perspective on science, complete with a proven correctness 
notion, and use it to make progress on long-standing and critical open 
problems in biology.