Joëlle Despeyroux
Researcher at INRIA, in the Kairos team, Sophia Antipolis.
Projects: Types.
Seminars: LSV at ENS Cachan - Colloquium at UPMC - Colloquium at INRIA-Sophia - Forum Numerica at UCA.
Personal hotlist. Inria intranet, agos-Sophia, and salsa.

Sauvons la recherche
Sauvons l'université
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.

Conferences

  • CSBio 2019-2021: 10th-12th Intl. Conf. on Computational Systems-Biology and Bioinformatics, 2019 Nice, 2020 Bangkok virtually, 2021 fully virtual (PC member).
  • 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

  • Computational Logic for Biomedicine and Neuroscience. Elisabetta De Maria, Joëlle Despeyroux, Amy Felty, Pietro Lio, Carlos Olarte, and Abdorrahim Bahrami. To appear as a chapter in a ISTE-Wiley book, 2022. A preliminary version is available as an HAL and arXiv report, October 2020. A French version of the ISTE book is available, July 2022.
  • Hybrid Linear Logics, revisited. Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte and Elaine Pimentel. Mathematical Structures in Computer Science (MSCS), 2019.
  • 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. Springer Nature, LNCS 11415:121-141, 2019.
  • 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.; 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.
  • 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.

    Teaching
    Past:
    - 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
    Past:
    - 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.

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

    Bio
    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 Paris, Cambridge, and Ottawa, 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.

    Google:
    Dblp:
    CiteSeer:
    Contact
    INRIA, 2004, route des Lucioles B.P.93, 06902 Sophia Antipolis Cedex, France.
    Joelle.Despeyroux aronbas/at inria.fr

    Previously in the team, at . Then CNRS, UCA, I3S, in the MDSC team.