JoŽlle Despeyroux

Researcher at INRIA and CNRS, I3S, UCA, in the MDSC team, Sophia Antipolis.
Projects: Types.
Seminars: LSV at ENS Cachan - Colloquium at UPMC - Colloquium at INRIA-Sophia - Forum Numerica at UCA.
Personal hotlist. Inria and I3S intranets.

Sciences en Marche
Sauvons la recherche
Une petite ONG en HaÔti
Research interests
- Formal Methods: semantics of programming languages, formal specifications.
- Proof theory, mechanization of proofs, certified software.
- Mathematical Logic, Logical frameworks, type theory.
- Logic for systems biology and biomedicine.


  • CMSB 2017: 15th Intl. Conference on Computational Methods in Systems Biology, 27-29 September 2017, Darmstadt, Germany (PC member).
  • CMSB 2016: 14th Intl. Conference on Computational Methods in Systems Biology, 21-23 September 2016, Cambridge, UK, (invited speaker and PC member).
  • TYPES 2015: 21st Intl. Conference on Types for Proofs and Programs, 18-21 May 2015, Tallinn, Estonia (PC member).

    Publications: list, bibtex

    Recent publications

  • Hybrid Linear Logics, revisited. Kaustuv Chaudhuri, JoŽlle Despeyroux, Carlos Olarte and Elaine Pimentel. Mathematical Structures in Computer Science (MSCS), 2018, to appear.
  • A Logical Framework for Modelling Breast Cancer Progression. JoŽlle Despeyroux, Amy Felty, Pietro Lio and Carlos Olarte. Intl. Symposium on Molecular Logic and Computational Synthetic Biology (MLCSB'2018), December 2018, to appear.
  • Hybrid and Subexponential Linear Logics. JoŽlle Despeyroux, Carlos Olarte and Elaine Pimentel. ENTCS 352, pages 95-111, June 2017. Extended version of the LSFA'2016 paper. A preliminary version is available as an HAL and arXiv report.
  • (Mathematical) Logic for Systems Biology. Invited paper. 14th Intl. Conference on Computational Methods in Systems Biology (CMSB'2016), Springer LNCS 9859, September 2016; slides.
  • Hybrid and Subexponential Linear Logics. JoŽlle Despeyroux, Carlos Olarte and Elaine Pimentel. 11th Workshop on Logical and Semantic Frameworks, with Applications (LSFA'2016). slides.
  • A Logical Framework for Systems Biology. Elisabetta De Maria, JoŽlle Despeyroux and Amy Felty. 1st Intl. Conference on Formal Methods in Macro-Biology (FMMB'2014), Springer LNCS 8738, September 2014, 20 pp., to appear; also accessible in HAL and arXiv hal-01285058; electronic appendix.
    Also presented at the intl. workshop on Logic for Systems Biology (LSB), FLOC'2014, July 2014; slides. INRIA-HAL and arXiv research report, April 2014.
  • A Hybrid Linear Logic for Constrained Transition Systems. JoŽlle Despeyroux and Kaustuv Chaudhuri. In Types for Proofs and Programs, post- proceedings of TYPES'2013, LIPIcs (Leibniz International Proceedings in Informatics), 2014.
  • A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology. Kaustuv Chaudhuri and JoŽlle Despeyroux. INRIA-HAL and arXiv research report; October 2013.

    Experiments in certified software: See here.

    - Master 2 at Nice: I've been giving a graduate course on secure software at the Master in CS, Nice Sophia Antipolis Univ. (UNS), in 2000-2002.
    A master on "formal methods and certified software was then created, which included a graduate course on mechanization of proofs.
    - Master 2 at Marseille: I've been giving a graduate course on "Natural Semantics: Specifications and Proofs", at the Master 2 MDFI ("Mathťmatiques DiscrŤtes et Fondements de l'Informatique") at Marseille, from December 1995 to 1999; lecture notes in french, 80 pages.
    The course have been followed by a graduate course on mechanization of proofs (rťsumť, in French) in the same Master.

    PhD students
    Some duties
    - Site leader of the Types projects from June 1994 to March 2006.
    - Member of the Evaluation Committee at Inria from March 1998 to August 2002.
    - Member of the "Commission de Spťcialistes" (evaluation committee) at Nice University from January 1999 to December 2001.

    Some past events: TYPES summer school '1999, LFM'2000, TYPES summer school '2002, POPL'07.
    Promising Proofs.
    Some pictures from conferences and summer schools.
    GeotargetGeo visitors

    JoŽlle Despeyroux is a researcher at INRIA-Sophia-Antipolis.
    She first worked in the semantics of programming languages area, proposing a pure logical view of Gordon Plotkin's Structural Operational Semantics (called "Natural Semantics"), well suited, for example, for proofs of correctness of compilers. She then worked in (mathematical) logic, at several levels: design of new type theories (unifying CCind and LF), proofs on the computer (mainly in Coq), and design and development of (a prototype of) a proof assistant (called "Theo").
    More recently, in joint work with Kaustuv Chaudhuri at INRIA-Saclay, she proposed a new (modal linear) logic as a Logical Framework for both specifying and analysing models of biological systems, viewed as transition systems. She is now working in this area, with several co-workers from Cambridge, Ottawa, and Brazil, using (linear) Logical Frameworks in various areas, from molecular biology to biomedicine.
    JoŽlle Despeyroux has a PhD in Mathematics from Paris University. She worked at INRIA-Roquencourt before moving to INRIA-Sophia-Antipolis.

    INRIA, 2004, route des Lucioles B.P.93, 06902 Sophia Antipolis Cedex, France.
    and CNRS (UMR 7271), I3S, Algorithmes-Euclide-B, 2000 route des Lucioles, B.P. 121, 06903 Sophia Antipolis, France.
    Joelle.Despeyroux aronbas/at - Phone: +33 (0)4 92 94 27 71

    Previously in the Parsifal team, at