Joëlle Despeyroux
Researcher at Inria Sophia-Antipolis and Saclay (LIX), in the Parsifal team.
Projects: Types, Mobius, Slimmer.
Seminars: Comète-Parsifal - Proval-Logical at LRI - LSV at ENS Cachan - PPS at Jussieu/Chevaleret.
Personal hotlist. gforge. [Inria, Saclay, and Sophia intranets.]

Sauvons la recherche
Une petite ONG en Haïti
Research interests
- Formal Methods: Semantics of programming languages, formal specifications, mechanization of proofs, certified software.
- Logical frameworks, type theory.
- More recently: Logic for systems biology.

Publications: list, bibtex

Recent publications and drafts

  • Metatheoretic results for a modal lambda-calcul (joint work with Pierre Leleu). Journal of Functional and Logic Programming (JFLP), the MIT Press, January 2000.
  • 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.
    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.
  • Primitive Recursion for Higher-Order Abstract Syntax(draft version, joint work with Frank Pfenning and Carsten Schürmann) Theoretical Computer Science, vol 266, 1-2, pages 1-57, September 2001.
    Extended and revised version of the TLCA'97 paper.
  • Recursion over Objects of Functional Type (joint work with 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. Extended and revised version of the TYPES'99 paper.
  • Draft for my "HDR" thesis ("Habilitation à Diriger des Recherches", in French, 53 pages, July 2003). ps file; with 2 pages per page.
  • A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology (joint work with Kaustuv Chaudhuri). INRIA-HAL research report inria-00402942; December 2010. (First draft version: May 2007.)
  • A Hybrid Linear Logic for Constrained Transition Systems (joint work with Kaustuv Chaudhuri); Submitted.

    Experiments in certified software: See here.

    Teaching

    Past:
    - "DEA" (Master 2) at Marseille: I've been giving a graduate course on "Natural Semantics: Specifications and Proofs", at the Dea 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 Dea.
    - "DEA" (Master 2) at Nice: I've been giving a graduate course on secure software at the Dea in CS, Nice Sophia-Antipolis Univ. (UNSA), in 2000-2002.
    A master on "formal methods and certified software was then created, which included a graduate course on mechanization of proofs.

    PhD students

    Members of the Types site at INRIA Sophia Antipolis

    Some duties

    Past:
    - Member of the "Commission de Spécialistes" at Nice University from January 1999 to December 2001.
    - Member of the Evaluation Committee at Inria from March 1998 to August 2002.
    - Site leader of the Types projects from June 1994 to March 2006.

    Miscellaneous

    Promising Proofs.
    Some pictures from conferences and summer schools.
    GeotargetGeo visitors

    Google:
    Dblp:
    CiteSeer:
    Contact:
    INRIA, 2004, route des Lucioles B.P.93, 06902 Sophia-Antipolis Cedex, France.
    and LIX, Ecole Polytechnique, Route de Saclay, F-91128 Palaiseau Cedex.
    Joelle.Despeyroux aronbas/at/@ inria.fr - Phone: +33 (0) 4 92 38 78 05 - at LIX: +33 (0) 1 69 33 40 34