JoŽlle Despeyroux

Researcher at INRIA and CNRS, I3S, in the MDSC - bioinfo team, Sophia Antipolis.
Projects: Types.
Seminars: ComŤte-Parsifal - Proval-Logical at LRI - LSV at ENS Cachan - PPS at university Paris Diderot.
Personal hotlist. [Inria, Saclay, Sophia, 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.
- Logic, Logical frameworks, type theory.
- Logic for systems biology.


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

    Publications: list, bibtex

    Recent publications, drafts, and talks

  • A Logical Framework for Systems Biology. Elisabetta de Maria, JoŽlle Despeyroux and Amy P. Felty. 1st International Conference on Formal Methods in Macro-Biology (FMMB), Springer LNCS 8738, September 2014, 20 pp., to appear; electronic appendix.
    Also presented at the international workshop Logic for Systems Biology (LSB), FLOC'2014, July 2014; slides. INRIA-HAL 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 research report inria-00402942; 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. Proc. of the IFIP International Conference on Theoretical Computer Science, IFIP TCS'2000, Sendai, Japan, August 17-19, 2000. JoŽlle Despeyroux.
    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.

    May June Summer Sept.

    INRIA, 2004, route des Lucioles B.P.93, 06902 Sophia Antipolis Cedex, France.
    and CNRS (UMR 7271), I3S, UNS, 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