JoŽlle Despeyroux

Researcher at INRIA and CNRS, I3S, UCA, in the MDSC - formal bioinfo team, Sophia Antipolis.
Projects: Types.
Seminars: LSV at ENS Cachan - Colloquium at UPMC - Colloquium at INRIA-Sophia.
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, drafts, and talks

  • (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), to appear; slides. An extended version has been accepted to ENTCS, 2017; preliminary version available as an HAL and arXiv report, August 2016.
  • 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), 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.
  • Draft for my "HDR" thesis ("Habilitation ŗ Diriger des Recherches", in French, 53 pages, July 2003). ps file; with 2 pages per page.
  • Recursion over Objects of Functional Type. JoŽlle Despeyroux and Pierre Leleu. Special issue of MSCS (Mathematical Structures in Computer Science) on Intuitionistic Modal Logics and Applications, Cambridge Univ. Press, Vol. 11, No. 4, August 2001. Revised and extended version of the TYPES'99 paper.
  • Primitive Recursion for Higher-Order Abstract Syntax. Carsten Schürmann, JoŽlle Despeyroux and Frank Pfenning. Theoretical Computer Science, vol 266, 1-2, pages 1-57, September 2001. Revised and extended version of the TLCA'97 paper.
  • A Higher-order specification of the pi-calculus. JoŽlle Despeyroux. Proc. of the IFIP Intl. Conference on Theoretical Computer Science, IFIP TCS'2000, Sendai, Japan, August 17-19, 2000.
    Errata. Strangely enough, the typing rules presented here do not follow the usual way to formalize a list of hypothesis when using the hoas method. A better version has been implemented. This new version needs induction on functions principles, that we had to postulate in Coq. Several variants of these principles have been proposed and proved correct elsewhere. Unpublished draft of the revised version presented at the conference.
  • Metatheoretic results for a modal lambda-calcul. JoŽlle Despeyroux and Pierre Leleu. Journal of Functional and Logic Programming (JFLP), the MIT Press, January 2000.

    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 Dec. 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 this new framework 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