Joëlle Despeyroux  -  Publications 

Bibtex source.

- Drafts:

Kaustuv Chaudhuri, Joëlle Despeyroux, Carlos Olarte and Elaine Pimentel.
Hybrid Linear Logics, revisited, Submitted to MSCS, 2017.

- Journals:

Joëlle Despeyroux, Carlos Olarte and Elaine Pimentel.
Hybrid and Subexponential Linear Logics. 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.

Joëlle Despeyroux and Pierre Leleu,
Recursion over Objects of Functional Type. 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.

Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning,
Primitive Recursion for Higher-Order Abstract Syntax (draft version) Theoretical Computer Science, vol 266, 1-2, pages 1-57, September 2001. Revised and extended version of the TLCA'97 paper.

Joëlle Despeyroux and Pierre Leleu,
Metatheoretic results for a modal lambda-calcul Journal of Functional and Logic Programming (JFLP), the MIT Press, January 2000.

Joëlle Despeyroux,
Theo: An Interactive Proof Development System,
Special issue on programming logic, the Scandinavian Journal on Computer Science and Numerical Analysis, BIT (32), pp 15-29, 1992.

Joëlle Despeyroux,
An algebraic specification of a Pascal Compiler,
ACM Sigplan Notices , vol. 18, nb 12, Dec. 83, pages 34-48. Also available as an INRIA research report RR-209, May 1983.

- Invited Papers:

Joëlle Despeyroux.
(Mathematical) Logic for Systems Biology, invited paper. 14th Intl. Conference on Computational Methods in Systems Biology (CMSB'2016), Springer LNCS 9859, September 2016; slides.

- Refereed International Conferences and Workshops:

Joëlle Despeyroux, Carlos Olarte and Elaine Pimentel.
Hybrid and Subexponential Linear Logics. 11th Workshop on Logical and Semantic Frameworks, with Applications (LSFA'2016); slides.

Elisabetta de Maria, Joëlle Despeyroux and Amy P. Felty,
A Logical Framework for Systems Biology. 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. slides. INRIA-HAL research report, April 2014.

Joëlle Despeyroux and Kaustuv Chaudhuri,
A Hybrid Linear Logic for Constrained Transition Systems. In Types for Proofs and Programs, post- proceedings of TYPES 2013, LIPIcs (Leibniz International Proceedings in Informatics), 2014.

Joëlle Despeyroux,
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.

Joëlle Despeyroux and Pierre Leleu,
Primitive recursion for higher-order abstract syntax with dependant types. Int. Workshop on Intuitionistic Modal Logics and Applications (IMLA), LICS'99 affiliated workshop, June 30 - July 12, 1999, Trento, Italy.

Joëlle Despeyroux and Pierre Leleu,
A modal lambda-calcul with iteration and case constructs. Proc. of the TYPES'98 workshop, Kloster Irsee, Allemagne, 27-31 March, 98, LNCS 1657, 1999.

Joëlle Despeyroux, Frank Pfenning and Carsten Schürmann,
Primitive Recursion for Higher-Order Abstract Syntax,
3rd int. conf. on Typed Lambda-Calculi and Applications, TLCA'97, Nancy, France, April, 1997. Springer-Verlag LNCS 1210. An extended version is available as CMU Technical Report CMU-CS-96-172 (121 pages).

Joëlle Despeyroux, Amy Felty, and André Hirschowitz,
Higher-order abstract syntax in Coq,
2nd int. conf. on Typed Lambda-Calculi and Applications, TLCA'95, Edinburgh, April 1995. Springer-Verlag LNCS 902. Also appears as INRIA research report RR-2556, April 1995.

Joëlle Despeyroux and André Hirschowitz,
Higher-order Syntax and Induction in Coq,
Fifth Int. Conf. on Logic Programming and Automated Reasoning, LPAR, Kiev, July 1994. Springer-Verlag LNAI 822. Also appears as INRIA research report RR-2292, June 1994.

D. Clement, J. Despeyroux, Th. Despeyroux and G. Kahn,
A Simple Applicative Language: Mini-ML,
the ACM conference Lisp and Functional Programming, L&FP, Cambridge, Ma, USA, August 1986. Also available as an INRIA research report RR-529, May 1986.

Joëlle Despeyroux,
Proof of translation in Natural Semantics,
first Symp. on Logic In Computer Science, LICS, Cambridge, Ma, USA, June 1986. Also appears as INRIA research report RR 514, April 1986.

- Unrefereed International Conferences and Workshops:

Joëlle Despeyroux and Thierry Despeyroux,
Current experiments in Natural Semantics,
the MCC-INRIA conference on the Resolution of Equations in Algebraic Structures, Lakeway, Texas, May 1987.

- National Workshops:

Joëlle Despeyroux,
A higher-order specification of the pi-calculus. The Modelisation and Verification seminar, Marseille, Dec 1998.

- Lecture notes :

Joëlle Despeyroux,
Sémantique Naturelle: Spécifications et Preuves,
INRIA research report RR-3359, February 1998. Lecture notes of a graduate course in the "DEA" "Mathématiques Discrètes et Fondements de l'Informatique" (MDFI), Marseille, 1995-1999 (85 pages, in french).

- Misc.:

Kaustuv Chaudhuri and Joëlle Despeyroux,
A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology. INRIA-HAL research report, October 2013.

Joëlle Despeyroux and André Hirschowitz,
Higher-Order Syntax and Induction. Informal proceedings of the technical workshop of the ESPRIT BRA "Types" project: "On proving properties of programming languages", INRIA Sophia-Antipolis, September 1993, Ed.: J. Despeyroux.

Joëlle Despeyroux,
Natural Semantics in Coq. First experiments. Informal proceedings of the TYPES'92 workshop, annual workshop of the ESPRIT BRA "TYPES for proofs and programs" project, Bastad, Sweden, June 1992.

Joëlle Despeyroux,
Theo: An Interactive Proof Development System. User's manual,
INRIA technical report RT-116, February 1990.

D. Clement, J. Despeyroux, Th. Despeyroux and G. Kahn,
Natural Semantics on the Computer,
INRIA research report RR-416, June 1985.

Joëlle Despeyroux,
Une sémantique algébrique de Pascal et application à la spécification d'un compilateur Pascal-P-Code. PhD thesis, Paris IX University, Orsay, October 1982 (in french).

Joëlle Despeyroux,
Une sémantique formelle du P-Code basée sur les types abstraits algébriques. INRIA report {RR}-158, Sept. 1982 (in french).

- Development of Systems:

Joëlle Despeyroux,
Theo: Development of the Theo system from January 1988 to December 1991. This prototype has been distributed to the Centaur users interested in proof construction (ap. 10 sites at that time).