Selected publications by Jean Goubault-Larrecq

Books

GM97

J. Goubault-Larrecq and I. Mackie.  Proof Theory and Automated Deduction, Applied Logic Series 6. Kluwer Academic Publishers, 1997. ( BibTeX )

Chapters in Books

Gou06a

J. Goubault-Larrecq.  Preuve et vérification pour la sécurité et la sûreté.  In Encyclopédie de l'informatique et des systèmes d'information, chapter I.6, pages 683-703. Vuibert, 2006. ( Web page | BibTeX + Abstract )

Edited Books

Gou03

J. Goubault-Larrecq (ed.).  Proceedings of the 1st Workshop on Logical Aspects of Cryptographic Protocol Verification (LACPV 2001), Paris, France, July 2001, ENTCS 55(1). Elsevier Science Publishers, 2003. ( BibTeX )

Gou02a

J. Goubault-Larrecq (ed.).  Special Issue on Models and Methods for Cryptographic Protocol Verification.  Journal of Telecommunications and Information Technology 4/2002, 2002. ( Web page | BibTeX )

Gou02b

J. Goubault-Larrecq (ed.).  Actes du 1er Workshop International sur la Sécurité des Communications sur Internet (SECI'02), Tunis, Tunisia, September 2002. INRIA. ( Web page | BibTeX )

Journals

BGGP12

O. Bouissou, É. Goubault, J. Goubault-Larrecq and S. Putot.  A Generalization of P-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs.  Computing, 2012. To appear. ( PDF | BibTeX + Abstract )

FG12

A. Finkel and J. Goubault-Larrecq.  Forward Analysis for WSTS, Part II: Complete WSTS.  Logical Methods in Computer Science, 2012. To appear. ( BibTeX + Abstract )

Gou12

J. Goubault-Larrecq.  QRB-Domains and the Probabilistic Powerdomain.  Logical Methods in Computer Science, 2012. To appear. ( BibTeX + Abstract )

GK11

J. Goubault-Larrecq and K. Keimel.  Choquet-Kendall-Matheron Theorems for Non-Hausdorff Spaces.  Mathematical Structures in Computer Science 21(3), pages 511-561, 2011. ( PDF | BibTeX + Abstract )

Gou11a

J. Goubault-Larrecq.  Musings Around the Geometry of Interaction, and Coherence.  Theoretical Computer Science 412(20), pages 1998-2014, 2011. ( PDF | BibTeX + Abstract )

Gou10a

J. Goubault-Larrecq.  Finite Models for Formal Security Proofs.  Journal of Computer Security 18(6), pages 1247-1299, 2010. ( PDF | BibTeX + Abstract )

Gou10b

J. Goubault-Larrecq.  De Groot Duality and Models of Choice: Angels, Demons, and Nature.  Mathematical Structures in Computer Science 20(2), pages 169-237, 2010. ( PDF | BibTeX + Abstract )

GLN08

J. Goubault-Larrecq, S. Lasota and D. Nowak.  Logical Relations for Monadic Types.  Mathematical Structures in Computer Science 18(6), pages 1169-1217, 2008. 81 pages. ( PDF | BibTeX + Abstract )

VG07

K. N. Verma and J. Goubault-Larrecq.  Alternating Two-Way AC-Tree Automata.  Information and Computation 205(6), pages 817-869, 2007. ( PDF | PS | PS.GZ | BibTeX + Abstract )

VG05

K. N. Verma and J. Goubault-Larrecq.  Karp-Miller Trees for a Branching Extension of VASS.  Discrete Mathematics & Theoretical Computer Science 7(1), pages 217-230, 2005. ( PDF | PS | PS.GZ | BibTeX + Abstract )

Gou05a

J. Goubault-Larrecq.  Deciding H₁ by Resolution.  Information Processing Letters 95(3), pages 401-408, 2005. ( PDF | BibTeX + Abstract )

GRV05

J. Goubault-Larrecq, M. Roger and K. N. Verma.  Abstraction and Resolution Modulo AC: How to Verify Diffie-Hellman-like Protocols Automatically.  Journal of Logic and Algebraic Programming 64(2), pages 219-251, 2005. ( PS | PS.GZ | BibTeX )

Gou05b

J. Goubault-Larrecq.  Extensions of Valuations.  Mathematical Structures in Computer Science 15(2), pages 271-297, 2005. ( PS | PS.GZ | BibTeX )

GG03

J. Goubault-Larrecq and É. Goubault.  On the Geometry of Intuitionistic S4 Proofs.  Homology, Homotopy and Applications 5(2), pages 137-209, 2003. ( PS | PS.GZ | BibTeX )

Gou02c

J. Goubault-Larrecq.  Sécurité, modélisation et analyse de protocoles cryptographiques.  Phœbus, la revue de la sûreté de fonctionnement 20, 2002. ( DOC | BibTeX )

GG00

H. Goguen and J. Goubault-Larrecq.  Sequent Combinators: A Hilbert System for the Lambda Calculus.  Mathematical Structures in Computer Science 10(1), pages 1-79, 2000. ( PS | PS.GZ | BibTeX )

Conferences

GV11

J. Goubault-Larrecq and D. Varacca.  Continuous Random Variables.  In LICS'11, pages 97-106. IEEE Computer Society Press, 2011. ( PDF | BibTeX + Abstract )

Gou10c

J. Goubault-Larrecq.  Noetherian Spaces in Verification.  In ICALP'10, LNCS 6199, pages 2-21. Springer, 2010. ( PDF | BibTeX + Abstract )

Gou10d

J. Goubault-Larrecq.  ωQRB-Domains and the Probabilistic Powerdomain.  In LICS'10, pages 352-361. IEEE Computer Society Press, 2010. ( PDF | BibTeX + Abstract )

Gou09a

J. Goubault-Larrecq.  "Logic Wins!".  In ASIAN'09, LNCS 5913, pages 1-16. Springer, 2009. ( PDF | BibTeX + Abstract )

FG09a

A. Finkel and J. Goubault-Larrecq.  Forward Analysis for WSTS, Part II: Complete WSTS.  In ICALP'09, LNCS 5556, pages 188-199. Springer, 2009. ( PDF | BibTeX + Abstract )

FG09b

A. Finkel and J. Goubault-Larrecq.  Forward Analysis for WSTS, Part I: Completions.  In STACS'09, Leibniz International Proceedings in Informatics 3, pages 433-444. Leibniz-Zentrum für Informatik, 2009. ( PDF | BibTeX + Abstract )

Gou08a

J. Goubault-Larrecq.  Towards Producing Formally Checkable Security Proofs, Automatically.  In CSF'08, pages 224-238. IEEE Computer Society Press, 2008. ( PDF | BibTeX + Abstract )

Gou08b

J. Goubault-Larrecq.  Simulation Hemi-Metrics Between Infinite-State Stochastic Games.  In FoSSaCS'08, LNCS 4962, pages 50-65. Springer, 2008. ( PDF (long version) | BibTeX + Abstract )

Gou08c

J. Goubault-Larrecq.  Prevision Domains and Convex Powercones.  In FoSSaCS'08, LNCS 4962, pages 318-333. Springer, 2008. ( PDF (long version) | BibTeX + Abstract )

GO08

J. Goubault-Larrecq and J. Olivain.  A Smell of Orchids.  In RV'08, LNCS 5289, pages 1-20. Springer, 2008. ( PDF | BibTeX + Abstract )

BG07

E. Bursztein and J. Goubault-Larrecq.  A Logical Framework for Evaluating Network Resilience Against Faults and Attacks.  In ASIAN'07, LNCS 4846, pages 212-227. Springer, 2007. ( PDF | BibTeX + Abstract )

GPT07

J. Goubault-Larrecq, C. Palamidessi and A. Troina.  A Probabilistic Applied Pi-Calculus.  In APLAS'07, LNCS 4807, pages 175-290. Springer, 2007. ( PDF | BibTeX + Abstract )

Gou07a

J. Goubault-Larrecq.  Continuous Previsions.  In CSL'07, LNCS 4646, pages 542-557. Springer, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )

Gou07b

J. Goubault-Larrecq.  Continuous Capacities on Continuous State Spaces.  In ICALP'07, LNCS 4596, pages 764-776. Springer, 2007. ( PDF | BibTeX + Abstract )

Gou07c

J. Goubault-Larrecq.  On Noetherian Spaces.  In LICS'07, pages 453-462. IEEE Computer Society Press, 2007. ( PDF | PDF (long version) | BibTeX + Abstract )

OG05

J. Olivain and J. Goubault-Larrecq.  The Orchids Intrusion Detection Tool.  In CAV'05, LNCS 3576, pages 286-290. Springer, 2005. ( PDF | BibTeX )

GP05

J. Goubault-Larrecq and F. Parrennes.  Cryptographic Protocol Analysis on Real C Code.  In VMCAI'05, LNCS 3385, pages 363-379. Springer, 2005. ( PDF | PDF (long version) | BibTeX + Abstract )

GLNZ04

J. Goubault-Larrecq, S. Lasota, D. Nowak and Y. Zhang.  Complete Lax Logical Relations for Cryptographic Lambda-Calculi.  In CSL'04, LNCS 3210, pages 400-414. Springer, 2004. ( PS | PS.GZ | BibTeX )

Gou02d

J. Goubault-Larrecq.  Higher-Order Positive Set Constraints.  In CSL'02, LNCS 2471, pages 473-489. Springer, 2002. ( PS | PS.GZ | BibTeX )

GLN02

J. Goubault-Larrecq, S. Lasota and D. Nowak.  Logical Relations for Monadic Types.  In CSL'02, LNCS 2471, pages 553-568. Springer, 2002. ( PS | PS.GZ | BibTeX )

Gou01a

J. Goubault-Larrecq.  Well-Founded Recursive Relations.  In CSL'01, LNCS 2142, pages 484-497. Springer, 2001. ( PS | PS.GZ | BibTeX )

RG01a

X. Rival and J. Goubault-Larrecq.  Experiments with Finite Tree Automata in Coq.  In TPHOLs'01, LNCS 2152, pages 362-377. Springer, 2001. ( PS | PS.GZ | BibTeX )

RG01b

M. Roger and J. Goubault-Larrecq.  Log Auditing through Model Checking.  In CSFW'01, pages 220-236. IEEE Computer Society Press, 2001. ( PS | PS.GZ | BibTeX )

VGPA00

K. N. Verma, J. Goubault-Larrecq, S. Prasad and S. Arun-Kumar.  Reflecting BDDs in Coq.  In ASIAN 2000, LNCS 1961, pages 162-181. Springer, 2000. ( PS | PS.GZ | BibTeX )

Gou00

J. Goubault-Larrecq.  A Method for Automatic Cryptographic Protocol Verification (Extended Abstract).  In Proceedings of the Workshops of the 15th International Parallel and Distributed Processing Symposium, Cancun, Mexico, May 2000, LNCS 1800, pages 977-984. Springer, 2000. ( PS | PS.GZ | BibTeX )

Gou99a

J. Goubault-Larrecq.  Conjunctive Types and SKInT.  In TYPES'98, LNCS 1657, pages 106-120. Springer, 1999. ( PS | PS.GZ | BibTeX )

Gou99b

J. Goubault-Larrecq.  A Simple Sequent System for First-Order Logic with Free Constructors.  In TABLEAUX'99, LNAI 1617, pages 202-216. Springer, 1999. ( BibTeX )

Gou98a

J. Goubault-Larrecq.  A Proof of Weak Termination of Typed λ-σ-Calculi.  In TYPES'96, LNCS 1512, pages 134-151. Springer, 1998. ( PS | PS.GZ | BibTeX )

Gou97a

J. Goubault-Larrecq.  Ramified Higher-Order Unification.  In LICS'97, pages 410-421. IEEE Computer Society Press, 1997. ( PS | PS.GZ | BibTeX )

SG97

P. H. Schmitt and J. Goubault-Larrecq.  A Tableau System for Linear-TIME Temporal Logic.  In TACAS'97, LNCS 1217, pages 130-144. Springer, 1997. ( PS | PS.GZ | BibTeX )

Theses

Gou97b

J. Goubault-Larrecq.  Logique, complexité, démonstration automatique et thèmes connexes.  Mémoire d'habilitation, Université Paris 9 (Dauphine), Paris, France, September 1997. ( PS | PS.GZ | BibTeX )

Other Publications

OGB⁺11

J. Olivain, J. Goubault-Larrecq, H. Benzina, B. Gourdin and R. Ben Younès.  ORCHIDS, 2011. ( Web page | BibTeX + Abstract )

Gou11b

J. Goubault-Larrecq.  A Few Pearls in the Theory of Quasi-Metric Spaces, Invited talk, Fifth International Conference on Topology, Algebra, and Categories in Logic (TACL'11), Marseilles, France, July 2011, 2011. ( BibTeX )

BG10

H. Benzina and J. Goubault-Larrecq.  Some Ideas on Virtualized Systems Security, and Monitors.  In DPM/SETOP'10, LNCS 6514, pages 244-258. Springer, 2010. ( PDF | BibTeX + Abstract )

BGGP10

O. Bouissou, É. Goubault, J. Goubault-Larrecq and S. Putot.  A Generalization of P-boxes to Affine Arithmetic, and Applications to Static Analysis of Programs.  In SCAN'10. 2010. ( BibTeX )

Gou09b

J. Goubault-Larrecq.  On a Generalization of a Result by Valk and Jantzen.  Research Report LSV-09-09, Laboratoire Spécification et Vérification, ENS Cachan, France, May 2009. 18 pages. ( PDF | BibTeX + Abstract )

Gou08d

J. Goubault-Larrecq.  HimML: HimML is a map-oriented ML, 2008. ( Web page | BibTeX )

Gou08e

J. Goubault-Larrecq.  A Cone-Theoretic Krein-Milman Theorem.  Research Report LSV-08-18, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2008. 8 pages. ( PDF | BibTeX + Abstract )

Gou08f

J. Goubault-Larrecq.  The h1 Tool Suite, 2008. ( Web page | BibTeX )

Gou07d

J. Goubault-Larrecq.  Believe It Or Not, GOI is a Model of Classical Linear Logic.  Research Report LSV-07-03, Laboratoire Spécification et Vérification, ENS Cachan, France, January 2007. 18 pages. ( PDF | BibTeX + Abstract )

Gou06b

J. Goubault-Larrecq.  The ORCHIDS Intrusion Prevention System, Invited talk, Annual Adaptive and Resilient Computing Systems Workshop (AARCS'06), Santa Fe, New Mexico, USA, 2006. ( Web page | BibTeX )

OG06

J. Olivain and J. Goubault-Larrecq.  Detecting Subverted Cryptographic Protocols by Entropy Checking.  Research Report LSV-06-13, Laboratoire Spécification et Vérification, ENS Cachan, France, June 2006. 19 pages. ( PDF | BibTeX + Abstract )

Gou05c

J. Goubault-Larrecq.  A Biased Survey of Models and Methods for Verifying Cryptographic Protocols, Invited talk, Workshop on Classical and Quantum Information Security, Pasadena, California, USA, 2005. ( Web page | Slides | BibTeX )

GP04

J. Goubault-Larrecq and F. Parrennes.  Csur: Static Analysis of C Code, 2004. ( Web page | BibTeX )

Gou04a

J. Goubault-Larrecq.  On Computational Interpretations of the Modal Logic S4, Invited talk, 2nd Workshop on the Logic for Pragmatics (WoLP'04), Créteil, France, 2004. ( BibTeX )

Gou04b

J. Goubault-Larrecq.  On Cryptographic Protocols, Regular Tree Languages, and Automated Deduction, Invited talk, Workshop on Security of Systems: Formalism and Tools (SASYFT'04), Orleans, France, 2004. ( Web page | Slides | BibTeX )

Gou04c

J. Goubault-Larrecq.  Une fois qu'on n'a pas trouvé de preuve, comment le faire comprendre à un assistant de preuve ?  In JFLA'04, pages 1-40. INRIA, 2004. Invited paper. ( PS | PS.GZ | BibTeX )

Gou02e

J. Goubault-Larrecq.  The EVA Parser and Translator, Available at http://www.lsv.ens-cachan.fr/˜goubault/EVA.html, 2002. Started 2001. Written in C (1327 lines), OCaml (361 lines), HimML (see [Gou08]) (3454 lines). ( Web page | BibTeX )

Gou02f

J. Goubault-Larrecq.  Un algorithme pour l'analyse de logs.  Research Report LSV-02-18, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2002. 33 pages. ( PS | PS.GZ | BibTeX )

Gou02g

J. Goubault-Larrecq.  Vérification de protocoles cryptographiques: la logique à la rescousse!  In SECI'02, pages 119-152. INRIA, 2002. Invited paper. ( PS | PS.GZ | BibTeX )

GV02

J. Goubault-Larrecq and K. N. Verma.  Alternating Two-Way AC-Tree Automata.  Research Report LSV-02-11, Laboratoire Spécification et Vérification, ENS Cachan, France, September 2002. 21 pages. ( PS | PS.GZ | BibTeX )

Gou02h

J. Goubault-Larrecq.  SKInT Labels.  Research Report LSV-02-7, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 15 pages. ( PS | PS.GZ | BibTeX )

Gou02i

J. Goubault-Larrecq.  A Note on the Completeness of Certain Refinements of Resolution.  Research Report LSV-02-8, Laboratoire Spécification et Vérification, ENS Cachan, France, July 2002. 16 pages. ( PS | PS.GZ | BibTeX )

Gou01b

J. Goubault-Larrecq.  Higher-Order Automata, Pushdown Systems, and Set Constraints.  Research Report LSV-01-9, Laboratoire Spécification et Vérification, ENS Cachan, France, November 2001. 15 pages. ( PS | PS.GZ | BibTeX )

GG99

J. Goubault-Larrecq and É. Goubault.  Order-Theoretic, Geometric and Combinatorial Models of Intuitionistic S4 Proofs.  In IMLA'99. 1999. ( PS | PS.GZ | BibTeX )

Gou99c

J. Goubault-Larrecq.  A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction.  Research Report RR-3653, INRIA Rocquencourt, France, March 1999. ( PS | PS.GZ | BibTeX )

Gou98b

J. Goubault-Larrecq.  A Few Remarks on SKInT.  Research Report RR-3475, INRIA Rocquencourt, France, August 1998. ( PS | PS.GZ | BibTeX )

Gou97c

J. Goubault-Larrecq.  On Computational Interpretations of the Modal Logic S4 - IIIb. Confluence, Termination of the λevQ_H-Calculus.  Research Report RR-3164, INRIA Rocquencourt, France, May 1997. ( PS | PS.GZ | BibTeX )

About LSV

• News
• People
• Research
• Seminars
• Teaching
• Contact

• École Normale Supérieure de Cachan
• Centre National de la Recherche Scientifique