The Coq mailing list

[Rene Vestergaard <renevestergaard AT acm.org>]

> On 11/7/18 10:37 AM, Rene Vestergaard wrote:
> "Proofs of life: molecular-biology reasoning simulates cell behaviors
> from first principles" is now at http://arxiv.org/abs/1811.02478

> accompanying video, with proof visualization and more:
>         http://ceqea.sourceforge.net/extras/instructionalPoL.mp4

I've been unable to find a venue that's prepared to take on the task of 
reviewing the work. The little feedback I've been able to obtain seems 
to indicate that the desk/chief editors were unwilling to go ahead with 
work that does not fit within their prior experiences. Of course, this 
leaves no room for multi- and antedisciplinary[*] efforts like Proofs of 
Life. My suggestions of an editor group have been roundly ignored.

Does anyone know of places with a proven record for mixed work?

Outside-the-box thoughts?


[The arXiv version is up to v3. The changes have mostly been about 
background and, in particular, about translating axiomatic reasoning and 
its meta-theory-carried implications into the languages of the other 
naturally-involved subjects. The manuscript is slightly too big for most 
wide-audience venues as it stands.]


Cheers,
Rene

[*] Sean R. Eddy. “Antedisciplinary” science. PLoS Computational 
Biology, 1(1), 2005.

---

ABSTRACT
We axiomatize the molecular-biology reasoning style, show compliance of 
the standard reference: Ptashne, A Genetic Switch, and present 
proof-theory-induced technologies to help infer phenotypes and to 
predict life cycles from genotypes. The key is to note that 
`reductionist discipline' entails constructive reasoning: any proof of a 
compound property can be decomposed to proofs of constituent properties. 
Proof theory makes explicit the inner structure of the axiomatized 
reasoning style and allows the permissible dynamics to be presented as a 
mode of computation that can be executed and analyzed. Constructivity 
and execution guarantee simulation when working over domain-specific 
languages. Here, we exhibit phenotype properties for genotype reasons: a 
molecular-biology argument is an open-system concurrent computation that 
results in compartment changes and is performed among processes of 
physiology change as determined from the molecular programming of given 
DNA. Life cycles are the possible sequentializations of the processes. A 
main implication of our construction is that formal correctness provides 
a complementary perspective on science that is as fundamental there as 
for pure mathematics. The bulk of the presented work has been verified 
formally correct by computer.