@misc(ZenonSite,
 note         = "\url {http://zenon-prover.org/}",
)
@misc(MaudeSite,
 note         = "\url {http://maude.cs.uiuc.edu/}",
)
@article(Ayrault:2009:DLC:1618874.1619017,
 author       = "Philippe Ayrault and Th{\'e}r\`{e}se Hardin and Fran\c {c}ois Pessaux",
 year         = "2009",
 title        = "Development Life-cycle of Critical Software Under FoCaL",
 journal      = "Electron. Notes Theor. Comput. Sci.",
 volume       = "243",
 pages        = "15--31",
 doi          = "10.1016/j.entcs.2009.07.003",
)
@inproceedings(Ayrault:2009:DGV:1575637.1575640,
 author       = "Philippe Ayrault and Th{\'e}r\`{e}se Hardin and Fran\c {c}ois Pessaux",
 year         = "2009",
 title        = "Development of a Generic Voter under FoCal",
 booktitle    = "TAP'09",
 series       = "LNCS",
 volume       = "5608",
 publisher    = "Springer-Verlag",
 pages        = "10--26",
 doi          = "10.1007/978-3-642-02949-3\_3",
)
@phdthesis(BoulmePhD00,
 author       = "S. Boulm\'e",
 year         = "2000",
 title        = "Sp\'ecification d'un environnement d\'edi\'e \`a la programmation certifi\'ee de biblioth\`eques de Calcul Formel",
 type         = "Th\`ese de doctorat",
 school       = "Universit\'e Paris 6",
)
@inproceedings(BoulmeCalc99,
 author       = "S. Boulm\'e and T. Hardin and D. Hirschkoff and V. M\'enissier-Morain and R. Rioboo",
 year         = "1999",
 title        = "On the way to certify Computer Algebra Systems",
 booktitle    = "Proceedings of the Calculemus workshop of FLOC'99",
 series       = "ENTCS",
 volume       = "23",
 publisher    = "Elsevier",
 doi          = "10.1016/S1571-0661(05)80609-7",
)
@manual(CC2,
 author       = "{Common Criteria}",
 year         = "2005",
 title        = "Common Criteria for Information Technology Security Evaluation, Norme {ISO} 15408 -- Version 3.0 Rev 2",
)
@(Johnsson85llifting,
 author       = "Thomas Johnsson",
 year         = "1985",
 title        = "Lambda Lifting: Transforming Programs to Recursive Equations",
 doi          = "10.1007/3-540-15975-4\_37",
)
@techreport(LamportProof,
 author       = "L. Lamport",
 year         = "1993",
 title        = "How to Write a Proof",
 type         = "Research report",
 institution  = "Digital Equipment Corporation",
)
@phdthesis(PrevostoPhD03,
 author       = "V. Prevosto",
 year         = "2003",
 title        = "Conception et Implantation du langage {FoC} pour le d\'eveloppement de logiciels certifi\'es",
 school       = "Universit\'e Paris 6",
)
@article(PrevostoJAR02,
 author       = "V. Prevosto and D. Doligez",
 year         = "2002",
 title        = "Algorithms and Proof Inheritance in the {Foc} language",
 journal      = "Journal of Automated Reasoning",
 volume       = "29",
 number       = "3-4",
 pages        = "337--363",
 doi          = "10.1023/A:1021979218446",
)
@inproceedings(PrevostoCalculemus03,
 author       = "V. Prevosto and M. Jaume",
 year         = "2003",
 title        = "Making Proofs in a hierarchy of Mathematical Structures",
 booktitle    = "Proceedings of the 11$^{th}$ Calculemus Symposium",
)
@inproceedings(PrevostoTPHOL02,
 author       = "Virgile Prevosto and Damien Doligez and Th\'er\`ese Hardin",
 year         = "2002",
 title        = "Algebraic Structures and Dependent Records",
 editor       = "Sofi\`ene Tahar C\'esar Mu\~noz and V\'ictor Carre\ eo",
 booktitle    = "Proceedings of TPHOLs 02",
 publisher    = "Springer-Verlag",
 doi          = "10.1007/3-540-45685-6\_20",
)
@manual(EN-50128,
 organization = "Standard Cenelec EN 50128",
 year         = "1999",
 title        = "Railway Applications - Communications, Signaling and Processing Systems - Software for Railway Control and Protection Systems",
)
@manual(IEC-61508,
 organization = "Standard IEC-61508, International Electrotechnical Commission",
 year         = "1998",
 title        = "Functional safety of electrical/electronic/programmable electronic safety-related systems",
)