Electronic Appendix

A Logical Framework for Systems Biology, Elisabetta de Maria, Joëlle Despeyroux, and Amy P. Felty, in Proceedings of the First International Conference Formal Methods in Macro-Biology (FMMB), Springer-Verlag LNCS, September 2014.

Appendices A and B

Extended Report

An extended version is available here. It contains the sequent proofs of all 4 properties.

Coq Files

The files run in Coq V8.4pl2. They must be compiled in the order they are listed.

Lambda Prolog Files

Tactic proof scripts for HyLL proofs of the 4 properties described in the paper. (These scripts are read in by the Lambda Prolog prover and translated to Coq script, which is imported and then fine-tuned to complete the above Coq proof development.) The prover is available as a zip file. It runs in the trunk version of the Teyjus implementation of Lambda Prolog.