@phdthesis{GL:hab,
author = {Goubault{-}Larrecq, Jean},
title = {Logique, complexit{\'e}, d{\'e}monstration automatique
et th{\`e}mes connexes},
type = {M{\'e}moire d'habilitation},
year = {1997},
month = sep,
school = {Universit{\'e} Paris~9 (Dauphine), Paris, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Gou-habil97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-habil97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gou-habil97.pdf},
lsv-lang = {FR}
}
@book{GLM:proof,
author = {Goubault{-}Larrecq, Jean and Mackie, Ian},
title = {Proof Theory and Automated Deduction},
volume = {6},
series = {Applied Logic Series},
year = {1997},
publisher = {Kluwer Academic Publishers},
month = may,
isbn = {0-7923-4593-2}
}
@techreport{JGL:S4:IIIb,
author = {Goubault{-}Larrecq, Jean},
title = {On Computational Interpretations of the Modal Logic
{S4}~--- {IIIb}.~{C}onfluence, Termination of the
{{\(\lambda\)}}{\(\mathtt{ev}{Q}_{H}\)}-Calculus},
type = {Research Report},
number = {RR-3164},
year = {1997},
month = may,
institution = {INRIA Rocquencourt, France},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/RR-3164.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-3164.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/RR-3164.pdf}
}
@inproceedings{JGL:ramified:HOU,
address = {Warsaw, Poland},
month = jul,
year = 1997,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'97},
booktitle = {{P}roceedings of the 12th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'97)},
author = {Goubault{-}Larrecq, Jean},
title = {Ramified Higher-Order Unification},
pages = {410-421},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/Gou-lics97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-lics97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Gou-lics97.pdf}
}
@inproceedings{SGL:PLTL1,
address = {Enschede, The Netherlands},
month = apr,
year = 1997,
volume = 1217,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Brinksma, Ed},
acronym = {{TACAS}'97},
booktitle = {{P}roceedings of the 3rd {I}nternational
{C}onference on {T}ools and {A}lgorithms for
{C}onstruction and {A}nalysis of {S}ystems
({TACAS}'97)},
author = {Schmitt, Peter H. and Goubault{-}Larrecq, Jean},
title = {A Tableau System for Linear-{TIME} Temporal Logic},
pages = {130-144},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/SchGou-tacas97.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/SchGou-tacas97.ps},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SchGou-tacas97.pdf}
}
@techreport{JGL:SKInT:conj:long,
author = {Goubault{-}Larrecq, Jean},
title = {A~Few Remarks on {SKI}n{T}},
type = {Research Report},
number = {RR-3475},
year = {1998},
month = aug,
institution = {INRIA Rocquencourt, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-3475.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-3475.ps}
}
@inproceedings{JGL:lamsigma:wterm,
address = {Aussois, France},
year = 1998,
volume = 1512,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Gim{\'e}nez, Eduardo and Paulin{-}Mohring, {\relax Ch}ristine},
acronym = {{TYPES}'96},
booktitle = {{S}elected {P}apers from the {I}nternational
{W}orkshop on {T}ypes for {P}roofs and {P}rograms
({TYPES}'96)},
author = {Goubault{-}Larrecq, Jean},
title = {A Proof of Weak Termination of Typed
{{\(\lambda-\sigma\)}}-Calculi},
pages = {134-151},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-types96.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-types96.ps}
}
@inproceedings{GGL:S4:models,
address = {Trento, Italy},
month = jul,
year = 1999,
editor = {Fairtlough, Matt and Mendler, Michael},
acronym = {{IMLA}'99},
booktitle = {{P}roceedings of the 1st {W}orkshop
on {I}ntuitionistic {M}odal {L}ogics and
{A}pplications
({IMLA}'99)},
author = {Goubault{-}Larrecq, Jean and Goubault, {\'E}ric},
title = {Order-Theoretic, Geometric and Combinatorial
Models of Intuitionistic {S4} Proofs},
missingpages = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GouGou-imla99.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GouGou-imla99.ps}
}
@inproceedings{JGL:SKInT:conj,
address = {Kloster Irsee, Germany},
year = 1999,
volume = 1657,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Altenkirch, {\relax Th}orsten and
Naraschewski, Wolfgang and Reus, Bernhard},
acronym = {{TYPES}'98},
booktitle = {{S}elected {P}apers from the {I}nternational
{W}orkshop on {T}ypes for {P}roofs and {P}rograms
({TYPES}'98)},
author = {Goubault{-}Larrecq, Jean},
title = {Conjunctive Types and {SKI}n{T}},
pages = {106-120},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-types98.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-types98.ps}
}
@inproceedings{JGL:freecons,
address = {Saratoga Springs, New York, USA},
month = jun,
year = 1999,
volume = 1617,
series = {Lecture Notes in Artificial Intelligence},
publisher = {Springer},
editor = {Murray, Neil V.},
acronym = {{TABLEAUX}'99},
booktitle = {{P}roceedings of the 8th {I}nternational
{W}orkshop on {T}heorem {P}roving with
{A}nalytic {T}ableaux and {R}elated {M}ethods
({TABLEAUX}'99)},
author = {Goubault{-}Larrecq, Jean},
title = {A Simple Sequent System for First-Order Logic with
Free Constructors},
pages = {202-216}
}
@techreport{JGL:freecons:ind,
author = {Goubault{-}Larrecq, Jean},
title = {A Simple Deduction System for First-Order Logic
with Equality, Free Constructors and Induction},
type = {Research Report},
number = {RR-3653},
year = {1999},
month = mar,
institution = {INRIA Rocquencourt, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-3653.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RR-3653.ps}
}
@article{GGL:SKIn,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goguen, Healfdene and Goubault{-}Larrecq, Jean},
title = {Sequent Combinators: {A} {H}ilbert System for the
Lambda Calculus},
volume = {10},
number = {1},
pages = {1-79},
year = {2000},
month = feb,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GogGou-MSCS2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GogGou-MSCS2000.ps}
}
@misc{GL:ASPROM,
author = {Goubault{-}Larrecq, Jean},
title = {Analyse de protocoles cryptographiques},
year = {2000},
month = oct,
howpublished = {Invited lecture, Journ{\'e}es {ASPROM}, Paris,
France},
lsv-lang = {FR}
}
@inproceedings{JGL:crypto:orPTA,
address = {Cancun, Mexico},
month = may,
year = 2000,
volume = 1800,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Rolim, Jos{\'e} D. P.},
booktitle = {{P}roceedings of the Workshops of the 15th {I}nternational
{P}arallel and {D}istributed {P}rocessing {S}ymposium},
author = {Goubault{-}Larrecq, Jean},
title = {A Method for Automatic Cryptographic Protocol
Verification (Extended Abstract)},
pages = {977-984},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-fmppta2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-fmppta2000.ps}
}
@inproceedings{VGLPAK:BDDinCoq,
address = {Penang, Malaysia},
month = nov,
year = 2000,
volume = 1961,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {He, Jifeng and Sato, Masahito},
acronym = {{ASIAN} 2000},
booktitle = {{P}roceedings of the 6th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN} 2000)},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean and
Prasad, Sanjiva and Arun{-}Kumar, S.},
title = {Reflecting {BDD}s in {C}oq},
pages = {162-181},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGPA-asian2000.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGPA-asian2000.ps}
}
@inproceedings{GL:WFRR,
address = {Paris, France},
month = sep,
year = 2001,
volume = 2142,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Fribourg, Laurent},
acronym = {{CSL}'01},
booktitle = {{P}roceedings of the 15th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'01)},
author = {Goubault{-}Larrecq, Jean},
title = {Well-Founded Recursive Relations},
pages = {484-497},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-csl2001.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-csl2001.ps}
}
@techreport{JGL:eva:propal,
author = {Goubault{-}Larrecq, Jean},
title = {Une proposition de langage de description de
protocoles cryptographiques},
year = {2001},
month = jul,
type = {Contract Report},
number = 2,
institution = {projet RNTL~EVA},
note = {12 pages},
missingcomprehension = {Je ne comprends pas pourquoi cette entree est en RC et pas en wwwpublic,
alors que d'autres contrats EVA sont en TR et wwwpublic public}
}
@techreport{JGL:eva:sem,
author = {Goubault{-}Larrecq, Jean},
title = {Les syntaxes et la s{\'e}mantique du langage de
sp{\'e}cification~{EVA}},
year = {2001},
month = nov,
type = {Contract Report},
number = 3,
institution = {projet RNTL~EVA},
note = {32 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR3.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR3.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EVA-TR4.ps}
}
@techreport{LSV:01:9,
author = {Goubault{-}Larrecq, Jean},
title = {Higher-Order Automata, Pushdown Systems, and Set
Constraints},
type = {Research Report},
number = {LSV-01-9},
year = {2001},
month = nov,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-9.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2001-9.rr.ps}
}
@inproceedings{RGL:TAinCoq,
address = {Edinburgh, Scotland, UK},
month = sep,
year = 2001,
volume = 2152,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Boulton, Richard J. and Jackson, Paul B.},
acronym = {{TPHOLs}'01},
booktitle = {{P}roceedings of the 14th {I}nternational
{C}onference on {T}heorem {P}roving in
{H}igher {O}rder {L}ogics
({TPHOLs}'01)},
author = {Rival, Xavier and Goubault{-}Larrecq, Jean},
title = {Experiments with Finite Tree Automata in {C}oq},
pages = {362-377},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RivGou-tphol01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RivGou-tphol01.ps}
}
@inproceedings{RGL:log-art,
address = {Cape Breton, Nova Scotia, Canada},
month = jun,
year = 2001,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSFW}'01},
booktitle = {{P}roceedings of the
14th {IEEE} {C}omputer {S}ecurity {F}oundations
{W}orkshop ({CSFW}'01)},
author = {Roger, Muriel and Goubault{-}Larrecq, Jean},
title = {Log Auditing through Model Checking},
pages = {220-236},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RogGou-csfw01.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RogGou-csfw01.ps}
}
@inproceedings{GLLN-csl2002,
address = {Edinburgh, Scotland, UK},
month = sep,
year = 2002,
volume = 2471,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bradfield, Julian C.},
acronym = {{CSL}'02},
booktitle = {{P}roceedings of the 16th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'02)},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir and
Nowak, David},
title = {Logical Relations for Monadic Types},
pages = {553-568},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLN-csl2002.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLN-csl2002.ps}
}
@misc{JG:EVA:trans,
author = {Goubault{-}Larrecq, Jean},
title = {The {EVA} Parser and Translator},
year = {2002},
missingmonth = {},
missingnmonth = {},
howpublished = {Available at
\url{http://www.lsv.ens-cachan.fr/~goubault/EVA.html}},
note = {Started 2001. Written in C (1327 lines), OCaml (361
lines), HimML (see~\cite{JG:HimML:dwnld}) (3454
lines).},
url = {http://www.lsv.ens-cachan.fr/~goubault/EVA.html}
}
@inproceedings{JGL-csl2002,
address = {Edinburgh, Scotland, UK},
month = sep,
year = 2002,
volume = 2471,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Bradfield, Julian C.},
acronym = {{CSL}'02},
booktitle = {{P}roceedings of the 16th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'02)},
author = {Goubault{-}Larrecq, Jean},
title = {Higher-Order Positive Set Constraints},
pages = {473-489},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-6.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-6.rr.ps}
}
@misc{JGL:Csur,
author = {Goubault{-}Larrecq, Jean and Parrennes, Fabrice},
title = {{Csur}: {S}tatic Analysis of {C}~Code},
year = {2004},
missingmonth = {},
missingnmonth = {},
nohowpublished = {Available at \url{http://www.lsv.ens-cachan.fr/Software/csur/}},
nmnote = {Written in OCaml (12648 lines)},
url = {http://www.lsv.ens-cachan.fr/Software/csur/},
oldurl = {http://www.lsv.ens-cachan.fr/~goubault/Csur/csur.html}
}
@techreport{JGL:EVA:CPV/2,
author = {Goubault{-}Larrecq, Jean},
title = {Outils {CPV} et {CPV2}},
year = {2002},
month = may,
type = {Contract Report},
number = 8,
institution = {Projet RNTL~EVA},
oldhowpublished = {Rapport num{\'e}ro 8 du projet RNTL EVA},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR8.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR8.pdf},
note = {7 pages}
}
@article{JGL:JTIT,
address = {Warsaw, Poland},
publisher = {Instytut {\L}{\k a}csno{\'s}ci},
journal = {Journal of Telecommunications and
Information Technology},
author = {Goubault{-}Larrecq, Jean},
editor = {Goubault{-}Larrecq, Jean},
title = {Special Issue on Models and Methods for Cryptographic
Protocol Verification},
volume = {4/2002},
year = {2002},
missingmonth = {},
missingnmonth = {},
url = {http://www.nit.eu/archive?view=kwartalrok&rok=2002&kwartal=4}
}
@inproceedings{JGL:SECI:pirates,
address = {Tunis, Tunisia},
month = sep,
year = 2002,
publisher = {INRIA},
editor = {Goubault{-}Larrecq, Jean},
acronym = {{SECI}'02},
booktitle = {{A}ctes du 1er {W}orkshop {I}nternational
sur la {S}{\'e}curit{\'e} des {C}ommunications
sur {I}nternet
({SECI}'02)},
author = {Goubault{-}Larrecq, Jean},
title = {{V}{\'e}rification de protocoles cryptographiques: la
logique {\`a} la rescousse!},
pages = {119-152},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-seci.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-seci.ps}
}
@article{JGL:crypto:modeles,
address = {Bordeaux, France},
publisher = {Groupe Pr{\'e}ventique},
journal = {Ph{\oe}bus, la revue de la s{\^u}ret{\'e} de
fonctionnement},
author = {Goubault{-}Larrecq, Jean},
title = {{S}{\'e}curit{\'e}, mod{\'e}lisation et analyse de
protocoles cryptographiques},
missingpages = {??},
volume = {20},
year = {2002},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/DOC/GL-Phoebus2002.doc}
}
@techreport{JGL:dico:3.1,
author = {Goubault{-}Larrecq, Jean and
Pouzol, Jean-{\relax Ph}ilippe and Demri, St{\'e}phane
and M{\'e}, Ludovic and Carle, P.},
missingauthor = {},
title = {Langages de d{\'e}tection d'attaques par signatures},
year = {2002},
month = jun,
type = {Contract Report},
number = {(Sous-projet~3, livrable~1)},
institution = {Projet RNTL DICO},
oldhowpublished = {Sous-projet 3, livrable 1 du projet RNTL DICO. Version
1},
note = {30 pages}
}
@techreport{LSV:02:11,
author = {Goubault{-}Larrecq, Jean and Verma, Kumar N.},
title = {Alternating Two-Way {AC}-Tree Automata},
type = {Research Report},
number = {LSV-02-11},
year = {2002},
month = sep,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {21 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-11.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-11.rr.ps}
}
@techreport{LSV:02:18,
author = {Goubault{-}Larrecq, Jean},
title = {Un algorithme pour l'analyse de logs},
type = {Research Report},
number = {LSV-02-18},
year = {2002},
month = nov,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {33 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-18.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-18.rr.ps}
}
@techreport{LSV:02:7,
author = {Goubault{-}Larrecq, Jean},
title = {{SKInT} Labels},
type = {Research Report},
number = {LSV-02-7},
year = {2002},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {15 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-7.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-7.rr.ps}
}
@techreport{LSV:02:8,
author = {Goubault{-}Larrecq, Jean},
title = {A Note on the Completeness of Certain Refinements of
Resolution},
type = {Research Report},
number = {LSV-02-8},
year = {2002},
month = jul,
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
note = {16 pages},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-8.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-8.rr.ps}
}
@article{JGL:S4:geometry,
lsv-note = {Published in partnership with International Press},
publisher = {HHA Publications},
journal = {Homology, Homotopy and Applications},
author = {Goubault{-}Larrecq, Jean and Goubault, {\'E}ric},
title = {On the Geometry of Intuitionistic {S4} Proofs},
volume = {5},
number = {2},
pages = {137-209},
year = {2003},
missingmonth = {},
missingnmonth = {},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/S4G.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/S4G.ps}
}
@techreport{JGL:dico:3.3,
author = {Demri, St{\'e}phane and Ducass{\'e}, Mireille and
Goubault{-}Larrecq, Jean
and M{\'e}, Ludovic and Olivain, Julien and
Picaronny, Claudine and
Pouzol, Jean-{\relax Ph}ilippe and
Totel, {\'E}ric and Vivinis, Bernard},
title = {Algorithmes de d{\'e}tection et langages de
signatures},
year = {2003},
month = oct,
type = {Contract Report},
number = {(Sous-projet~3, livrable~3)},
institution = {projet RNTL DICO},
oldhowpublished = {Sous-projet 3, livrable 3 du projet RNTL DICO.
Version~1},
note = {72~pages}
}
@inproceedings{GLNZ-csl2004,
address = {Karpacz, Poland},
month = sep,
year = 2004,
volume = {3210},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Marcinkowski, Jerzy and Tarlecki, Andrzej},
acronym = {{CSL}'04},
booktitle = {{P}roceedings the 18th {I}nternational
{W}orkshop on {C}omputer {S}cience {L}ogic
({CSL}'04)},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir
and Nowak, David and
Zhang, Yu},
title = {Complete Lax Logical Relations for Cryptographic
Lambda-Calculi},
pages = {400-414},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLNZ-csl04.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLLNZ-csl04.ps}
}
@article{GLRV:acm,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Programming},
author = {Goubault{-}Larrecq, Jean and Roger, Muriel and
Verma, Kumar N.},
title = {Abstraction and Resolution Modulo~{AC}: {H}ow to
Verify
{D}iffie-{H}ellman-like Protocols Automatically},
volume = 64,
number = 2,
pages = {219-251},
year = {2005},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GLRV-acm.ps},
doi = {10.1016/j.jlap.2004.09.004}
}
@inproceedings{JGL:JFLA04,
address = {Sainte-Marie-de-R{\'e}, France},
month = jan,
year = 2004,
publisher = {INRIA},
editor = {M{\'e}nissier-Morain, Val{\'e}rie},
acronym = {{JFLA}'04},
booktitle = {{A}ctes des 15{\`e}mes {J}ourn{\'e}es
{F}rancophones sur les {L}angages
{A}pplicatifs
({JFLA}'04)},
author = {Goubault{-}Larrecq, Jean},
title = {Une fois qu'on n'a pas trouv{\'e} de preuve,
comment le
faire comprendre {\`a} un assistant de preuve~?},
pages = {1-40},
oldpublisher = {INRIA, collection didactique},
note = {Invited paper},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-JFLA2004.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/JGL-JFLA2004.ps}
}
@misc{JGL:wlp04,
author = {Goubault{-}Larrecq, Jean},
title = {On Computational Interpretations of the Modal Logic~{S4}},
year = 2004,
month = jul,
howpublished = {Invited talk, 2nd {W}orkshop on the {L}ogic for {P}ragmatics
({WoLP}'04), Cr{\'e}teil, France},
futureslides = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/JGL-talk_.pdf}
}
@misc{JGL:wcqis04,
author = {Goubault{-}Larrecq, Jean},
title = {A Biased Survey of Models and Methods for Verifying Cryptographic Protocols},
year = 2005,
month = dec,
howpublished = {Invited talk, {W}orkshop on {C}lassical and
{Q}uantum {I}nformation {S}ecurity, Pasadena, California, USA},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/JGL-wcqis05.pdf}
}
@misc{JGL:SASYFT04,
author = {Goubault{-}Larrecq, Jean},
title = {On Cryptographic Protocols, Regular Tree Languages,
and Automated Deduction},
year = 2004,
month = jun,
howpublished = {Invited talk, {W}orkshop on {S}ecurity
of {S}ystems: {F}ormalism and {T}ools
({SASYFT}'04), Orleans, France},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/SLIDES/JGL-talk_sasyft.pdf}
}
@article{JGL:val:ext,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Extensions of Valuations},
year = {2005},
volume = 15,
number = 2,
pages = {271-297},
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2002-17.rr.ps},
ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
rr-lsv-2002-17.rr.ps},
doi = {10.1017/S096012950400461X}
}
@inproceedings{GLP:VMCAI,
address = {Paris, France},
month = jan,
year = 2005,
volume = 3385,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cousot, Radhia},
acronym = {{VMCAI}'05},
booktitle = {{P}roceedings of the 6th {I}nternational {C}onference on
{V}erification, {M}odel {C}hecking and {A}bstract {I}nterpretation
({VMCAI}'05)},
author = {Goubault{-}Larrecq, Jean and Parrennes, Fabrice},
title = {Cryptographic Protocol Analysis on Real {C}~Code},
pages = {363-379},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GouPar-VMCAI2005.pdf},
doi = {10.1007/b105073},
abstract = {Implementations of
cryptographic protocols, such as OpenSSL for
example, contain bugs affecting security,
which cannot be detected by just analyzing
abstract protocols (e.g., SSL or TLS). We
describe how cryptographic protocol
verification techniques based on solving
clause sets can be applied to detect
vulnerabilities of C programs in the
Dolev-Yao model, statically. This involves
integrating fairly simple pointer analysis
techniques with an analysis of which messages
an external intruder may collect and forge.
This also involves relating concrete run-time
data with abstract, logical terms
representing messages. To this end, we make
use of so-called trust assertions.
The output of the analysis is a set of
clauses in the decidable class H1, which can
then be solved independently. This can be
used to establish secrecy properties, and to
detect some other bugs. }
}
@article{JGL-ipl2005,
publisher = {Elsevier Science Publishers},
journal = {Information Processing Letters},
author = {Goubault{-}Larrecq, Jean},
title = {Deciding {\(\mathcal{\MakeUppercase{H}}_1\)}
by Resolution},
year = {2005},
volume = 95,
number = 3,
pages = {401-408},
month = aug,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Goubault-h1.pdf},
doi = {10.1016/j.ipl.2005.04.007},
abstract = {Nielson, Nielson and Seidl's
class \(\mathcal{H}_1\) is a decidable class
of first-order Horn clause sets, describing
strongly regular relations. We give
another proof of decidability, and of the
regularity of the defined languages, based
on fairly standard automated deduction
techniques. }
}
@article{VGL-dmtcs05,
journal = {Discrete Mathematics \& Theoretical Computer Science},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
title = {{K}arp-{M}iller Trees for a Branching Extension of~{VASS}},
volume = 7,
number = 1,
pages = {217-230},
year = 2005,
month = nov,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
secondurl = {http://www.dmtcs.org/volumes/abstracts/dm070113.abs.html},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VGL-dmtcs05.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VGL-dmtcs05.ps},
abstract = {We study BVASS (Branching VASS)
which extend VASS (Vector Addition Systems with
States) by allowing addition transitions that
merge two configurations. Runs in BVASS are
tree-like structures instead of linear ones as
for VASS. We show that the construction of
Karp-Miller trees for VASS can be extended to
BVASS. This entails that the coverability set
for BVASS is computable. This allows us to
obtain decidability results for certain classes
of equational tree automata with an
associative-commutative symbol. Recent
independent work by de Groote \emph{et al.} implies
that decidability of reachability in BVASS is
equivalent to decidability of provability in
MELL (multiplicative exponential linear logic),
which is still an open problem. Hence our
results are also a step towards answering this
question in the affirmative.}
}
@inproceedings{Orchids-cav05,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2005,
volume = 3576,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Etessami, Kousha and Rajamani, Sriram},
acronym = {{CAV}'05},
booktitle = {{P}roceedings of the 17th
{I}nternational {C}onference on
{C}omputer {A}ided {V}erification
({CAV}'05)},
author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
title = {The {O}rchids Intrusion Detection Tool},
pages = {286-290},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/OG-cav05.pdf},
doi = {10.1007/11513988_28}
}
@incollection{jgl-encyc06,
author = {Goubault{-}Larrecq, Jean},
title = {Preuve et v{\'e}rification pour la s{\'e}curit{\'e}
et la s{\^u}ret{\'e}},
booktitle = {Encyclop{\'e}die de l'informatique et des syst{\`e}mes
d'information},
editor = {Akoka, Jacky and Comyn-Wattiau, Isabelle},
pages = {683-703},
publisher = {Vuibert},
year = 2006,
month = dec,
chapter = {I.6},
url = {http://www.vuibert.com/livre12401.html},
abstract = {La s\^uret\'e, comme la s\'ecurit\'e, \'enonce qu'un mal n'arrive
jamais. Le but de cet article est de d\'efinir la notion de propri\'et\'e
de s\^uret\'e, et d'en d\'ecrire quelques techniques de v\'erification et de
preuve~: model-checking, interpr\'etation abstraite notamment. Apr\`es
avoir remarqu\'e qu'il n'y avait pas de s\'ecurit\'e sans s\^uret\'e, il est
expliqu\'e que l'analyse de s\'ecurit\'e d'un syst\`eme repose sur un
mod\`ele, des hypoth\`eses, des propri\'et\'es \`a v\'erifier, et une
architecture de s\'ecurit\'e. Finalement, il est donn\'e un aper\c{c}u de
quelques mod\`eles et m\'ethodes de preuve de protocoles
cryptographiques.}
}
@techreport{LSV:06:13,
author = {Olivain, Julien and Goubault{-}Larrecq, Jean},
title = {Detecting Subverted Cryptographic Protocols by Entropy Checking},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2006,
month = jun,
type = {Research Report},
number = {LSV-06-13},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2006-13.pdf},
note = {19~pages},
abstract = {What happens when your implementation of SSL or some other
cryptographic protocol is subverted through a buffer overflow
attack? You have been hacked, right. Unfortunately, you may be
unaware of~it: since normal traffic is encrypted, most IDSs cannot
monitor~it. We propose a simple, yet efficient technique to detect
such attacks, by computing the entropy of the flow and comparing it
against known thresholds. This was implemented in the Net-Entropy
sensor.}
}
@misc{JGL:aarcs06,
author = {Goubault{-}Larrecq, Jean},
title = {The {ORCHIDS} Intrusion Prevention System},
month = nov,
year = {2006},
howpublished = {Invited talk, {A}nnual {A}daptive and {R}esilient
{C}omputing {S}ystems {W}orkshop (AARCS'06), Santa Fe, New Mexico, USA},
url = {http://www.lsv.ens-cachan.fr/~goubault/aarcs06_orchids.pdf}
}
@inproceedings{Gou-fossacs08b,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Simulation Hemi-Metrics Between Infinite-State Stochastic Games},
pages = {50-65},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-34.pdf},
doi = {10.1007/978-3-540-78499-9_5},
abstract = {We investigate simulation hemi-metrics between certain forms
of turn-based \(2\frac{1}{2}\)-player games played on infinite
topological spaces. They have the desirable property of bounding the
difference in payoffs obtained by starting from one state or another.
All
constructions are described as the special case of a unique one, which we
call the Hutchinson hemi-metric on various spaces of continuous
previsions. We show a directed form of the Kantorovich-Rubinstein theorem,
stating that the Hutchinson hemi-metric on spaces of continuous
probability valuations coincides with a notion of trans-shipment
hemi-metric. We also identify the class of so-called sym-compact spaces as
the right class of topological spaces, where the theory works out as
nicely as possible.}
}
@inproceedings{Gou-fossacs08a,
address = {Budapest, Hungary},
month = mar # {-} # apr,
year = 2008,
volume = 4962,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Amadio, Roberto},
acronym = {{FoSSaCS}'08},
booktitle = {{P}roceedings of the 11th {I}nternational
{C}onference on {F}oundations of {S}oftware {S}cience
and {C}omputation {S}tructures
({FoSSaCS}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Prevision Domains and Convex Powercones},
pages = {318-333},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-33.pdf},
doi = {10.1007/978-3-540-78499-9_23},
abstract = {Two recent semantic families of models for mixed
probabilistic and non-deterministic choice over a space~\(X\) are the
convex powercone models, due independently to Mislove, and to Tix,
Keimel, and Plotkin, and the continuous prevision model of the
author. We show that, up to some minor details, these models are
isomorphic whenever \(X\) is a continuous, coherent cpo, and whether
the particular brand of non-determinism we focus on is demonic,
angelic, or chaotic. The construction also exhibits domains of
continuous previsions as retracts of well-known continuous cpos,
providing simple bases for the various continuous cpos of continuous
previsions. This has practical relevance to computing approximations
of operations on previsions.}
}
@inproceedings{BG-asian07,
address = {Doha, Qatar},
month = dec,
year = 2007,
volume = 4846,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cervesato, Iliano},
acronym = {{ASIAN}'07},
booktitle = {{P}roceedings of the 12th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'07)},
author = {Bursztein, Elie and Goubault{-}Larrecq, Jean},
title = {A Logical Framework for Evaluating Network Resilience Against
Faults and Attacks},
pages = {212-227},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BGL-asian07.pdf},
doi = {10.1007/978-3-540-76929-3_20},
abstract = {We present a logic-based framework to evaluate the resilience of
computer networks in the face of incidents, i.e., attacks
from malicious intruders as well as random faults. Our model
uses a two-layered presentation of dependencies between
files and services, and of timed games to represent not just
incidents, but also the dynamic responses from
administrators and their respective delays. We demonstrate
that a variant TATL\(\Diamond\) of timed alternating-time temporal
logic is a convenient language to express several desirable
properties of networks, including several forms of
survivability. We illustrate this on a simple redundant Web
service architecture, and show that checking such timed
games against the so-called TATL\(\Diamond\) variant of the timed
alternating time temporal logic TATL is EXPTIME-complete.}
}
@inproceedings{GPT-aplas07,
address = {Singapore},
month = nov # {-} # dec,
year = 2007,
volume = 4807,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Shao, Zhong},
acronym = {{APLAS}'07},
booktitle = {{P}roceedings of the 5th {A}sian {S}ymposium
on {P}rogramming {L}anguages and {S}ystems
({APLAS}'07)},
author = {Goubault{-}Larrecq, Jean and Palamidessi, Catuscia and
Troina, Angelo},
title = {A Probabilistic Applied Pi-Calculus},
pages = {175-290},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GPT-aplas07.pdf},
doi = {10.1007/978-3-540-76637-7_12},
abstract = {We propose an extension of the Applied Pi-calculus by
introducing nondeterministic and probabilistic choice operators. The
semantics of the resulting model, in which probability and nondeterminism
are combined, is given by Segala's Probabilistic Automata driven by
schedulers which resolve the nondeterministic choice among the probability
distributions over target states. Notions of static and observational
equivalence are given for the enriched calculus. In order to model the
possible interaction of a process with its surrounding environment a
labeled semantics is given together with a notion of weak bisimulation
which is shown to coincide with the observational equivalence. Finally, we
prove that results in the probabilistic framework are preserved in a
purely nondeterministic setting.}
}
@inproceedings{Gou-csl07,
address = {Lausanne, Switzerland},
month = sep,
year = 2007,
volume = 4646,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Duparc, Jacques and Henzinger, {\relax Th}omas A.},
acronym = {{CSL}'07},
booktitle = {{P}roceedings of the 16th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {Continuous Previsions},
pages = {542-557},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-csl07.pdf},
doi = {10.1007/978-3-540-74915-8_40},
abstract = {We define strong monads of continuous (lower, upper) previsions,
and of forks, modeling both probabilistic and non-deterministic choice.
This is an elegant alternative to recent proposals by Mislove, Tix,
Keimel, and Plotkin. We show that our monads are sound and complete, in
the sense that they model exactly the interaction between probabilistic
and (demonic, angelic, chaotic) choice.}
}
@inproceedings{JGL-icalp07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
volume = 4596,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Arge, Lars and Cachin, {\relax Ch}ristian and Jurdzi{\'n}ski, Tomasz
and Tarlecki, Andrzej},
acronym = {{ICALP}'07},
booktitle = {{P}roceedings of the 34th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {Continuous Capacities on Continuous State Spaces},
pages = {764-776},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-icalp07.pdf},
doi = {10.1007/978-3-540-73420-8_66},
abstract = {We propose axiomatizing some stochastic games, in a
continuous state
space setting, using continuous belief functions, resp.
plausibilities, instead of measures. Then, stochastic games are
just variations on continuous Markov chains. We argue that drawing
at random along a belief function is the same as letting the
probabilistic player~\(P\) play first, then letting the
non-deterministic player~\(C\) play demonically. The same
holds for an angelic~\(C\), using plausibilities instead.
We then define a simple modal logic, and characterize simulation in
terms of formulae of this logic. Finally, we show that (discounted)
payoffs are defined and unique, where in the demonic case,
\(P\)~maximizes payoff, while \(C\)~minimizes it}
}
@inproceedings{Gou-lics07,
address = {Wroc{\l}aw, Poland},
month = jul,
year = 2007,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'07},
booktitle = {{P}roceedings of the 22nd
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'07)},
author = {Goubault{-}Larrecq, Jean},
title = {On {N}oetherian Spaces},
pages = {453-462},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-lics07.pdf},
doi = {10.1109/LICS.2007.34},
abstract = {A topological space is Noetherian iff every open is compact.
Our~starting point is that this notion generalizes that of
well-quasi order, in the sense that an Alexandroff-discrete space is
Noetherian iff its specialization quasi-ordering is well. For~more
general spaces, this opens the way to verifying infinite transition
systems based on non-well quasi ordered sets, but where the preimage
operator satisfies an additional continuity assumption. The
technical development rests heavily on techniques arising from
topology and domain theory, including sobriety and the de Groot dual
of a stably compact space. We~show that the category Nthr of
Noetherian spaces is finitely complete and finitely cocomplete.
Finally, we note that if \(X\)~is a Noetherian space, then the set of
all (even infinite) subsets of~\(X\) is again Noetherian, a~result
that fails for well-quasi orders.}
}
@techreport{LSV:07:03,
author = {Goubault{-}Larrecq, Jean},
title = {Believe It Or Not, {GOI}~is a Model of Classical Linear Logic},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2007,
month = jan,
type = {Research Report},
number = {LSV-07-03},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-03.pdf},
note = {18~pages},
othernote = {a draft of the longer version of this report is available at
http://www.lsv.ens-cachan.fr/~goubault/isg.pdf},
abstract = {We introduce the Danos-R\'egnier category \(\mathcal{DR}(M)\) of a linear
inverse monoid~\(M\), a categorical description of geometries of
interaction~(GOI). The usual setting for GOI is that of a weakly
Cantorian linear inverse monoid. It is well-known that GOI is
perfectly suited to describe the multiplicative fragment of linear
logic, and indeed \(\mathcal{DR}(M)\) will be a \(*\)-autonomous category in this
case. It is also well-known that the categorical interpretation of
the other linear connectives conflicts with GOI interpretations. We
make this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no
cartesian product, and no exponential---whatever \(M\) is, unless \(M\)
is trivial. However, a form of coherence completion of~\(\mathcal{DR}(M)\) \`a
la Hu-Joyal provides a model of full classical linear logic, as soon
as \(M\) is weakly Cantorian.}
}
@article{VG-icomp2007,
publisher = {Elsevier Science Publishers},
journal = {Information and Computation},
author = {Verma, Kumar N. and Goubault{-}Larrecq, Jean},
title = {Alternating Two-Way {AC}-Tree Automata},
pages = {817-869},
year = {2007},
month = jun,
volume = 205,
number = 6,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/VG-icomp07.pdf},
ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/VG-icomp07.ps},
doi = {10.1016/j.ic.2006.12.006},
abstract = {We explore the notion of alternating two-way tree automata
modulo the theory of finitely many associative-commutative
(AC) symbols. This was prompted by questions arising in
cryptographic protocol verification, in~particular in
modeling group key agreement schemes based on
Diffie-Hellman-like functions, where the emptiness question
for intersections of such automata is fundamental. This also
has independent interest. We~show that the use of general
push clauses, or of alternation, leads to undecidability,
already in the case of one AC symbol, with only functions of
arity zero. On~the other hand, emptiness is decidable in the
general case of several function symbols, including several
AC symbols, provided push clauses are unconditional and
intersection clauses are final. This class of automata is
also shown to be closed under intersection.}
}
@misc{JGL:H1,
author = {Goubault{-}Larrecq, Jean},
title = {The {\ttfamily h1} Tool Suite},
year = {2008},
month = jan,
nmnote = {See~\cite{JGL:JFLA04} for description. Written in
HimML (15746 lines) and C (1823 lines)},
nmnote-fr = {Voir~\cite{JGL:JFLA04} pour la description. \'Ecrit en
HimML (15746 lignes) et C (1823 lignes)},
url = {http://www.lsv.ens-cachan.fr/~goubault/H1.dist/dh1index.html}
}
@misc{JG:HimML:dwnld,
author = {Goubault{-}Larrecq, Jean},
title = {{HimML}: {\bfseries \MakeUppercase{H}}im{ML}
{\bfseries i}s a {\bfseries m}ap-oriented
{\bfseries \MakeUppercase{ML}}},
year = {2008},
month = dec,
number = {v\(\alpha\)18r3},
nohowpublished = {An extension of core Standard ML, available at
\url{http://www.lsv.ens-cachan.fr/~goubault/himml-dwnld.html}},
nmnote = {Version 1.0 alpha 17. Written in C (108948 lines),
Emacs-Lisp (1850 lines). Documentation: 91 pages},
url = {http://www.lsv.ens-cachan.fr/~goubault/himml-dwnld.html}
}
@article{GLLN-mscs08,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean and Lasota, S{\l}awomir
and Nowak, David},
title = {Logical Relations for Monadic Types},
volume = 18,
number = 6,
pages = {1169-1217},
month = dec,
year = 2008,
note = {81~pages},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GLLN-arxiv05.pdf},
doi = {10.1017/S0960129508007172},
abstract = {Logical relations and their generalisations are a fundamental
tool in proving properties of lambda calculi, for example,
for yielding sound principles for observational equivalence.
We propose a natural notion of logical relations that is
able to deal with the monadic types of Moggi's computational
lambda calculus. The treatment is categorical, and is based
on notions of subsconing, mono factorisation systems and
monad morphisms. Our approach has a number of interesting
applications, including cases for lambda calculi with
non-determinism (where being in a logical relation means
being bisimilar), dynamic name creation and probabilistic
systems.}
}
@techreport{LSV:08:18,
author = {Goubault{-}Larrecq, Jean},
title = {A Cone-Theoretic {K}rein-{M}ilman Theorem},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = 2008,
month = jun,
type = {Research Report},
number = {LSV-08-18},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-18.pdf},
note = {8~pages},
abstract = {We prove the following analogue of the Krein-Milman
Theorem: in any locally convex \(T_{0}\) topological cone, every
convex compact saturated subset is the compact saturated convex hull
of its extreme points.}
}
@inproceedings{JGL:badweeds,
address = {Budapest, Hungary},
month = mar,
year = 2008,
volume = 5289,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Leucker, Martin},
acronym = {{RV}'08},
booktitle = {{P}roceedings of the 8th {W}orkshop on {R}untime {V}erification ({RV}'08)},
author = {Goubault{-}Larrecq, Jean and Olivain, Julien},
title = {A Smell of Orchids},
pages = {1-20},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/go-rv08.pdf},
doi = {10.1007/978-3-540-89247-2_1},
abstract = {Orchids is an intrusion detection tool based on techniques for
fast, on-line model-checking. Orchids detects complex, correlated strands
of events with very low overhead in practice, although its detec- tion
algorithm has worst-case exponential time complexity.\par
The purpose of this paper is twofold. First, we explain the salient
features of the basic model-checking algorithm in an intuitive way, as a
form of dynamically-spawned monitors. One distinctive feature of the
Orchids algorithm is that fresh monitors need to be spawned at a pos-
sibly alarming rate.\par
The second goal of this paper is therefore to explain how we tame the
complexity of the procedure, using abstract interpretation techniques to
safely kill useless monitors. This includes monitors which will provably
detect nothing, but also monitors that are subsumed by others, in the
sense that they will definitely fail the so-called shortest run criterion.
We take the opportunity to show how the Orchids algorithm maintains its
monitors sorted in such a way that the subsumption operation is effected
with no overhead, and we correct a small, but definitely annoying bug in
its core algorithm, as it was published in~2001.}
}
@inproceedings{JGL-csf08,
address = {Pittsburgh, Pennsylvania, USA},
month = jun,
year = 2008,
publisher = {{IEEE} Computer Society Press},
acronym = {{CSF}'08},
booktitle = {{P}roceedings of the
21st {IEEE} {C}omputer {S}ecurity {F}oundations
{S}ymposium ({CSF}'08)},
author = {Goubault{-}Larrecq, Jean},
title = {Towards Producing Formally Checkable Security Proofs, Automatically},
pages = {224-238},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2008-15.pdf},
doi = {10.1109/CSF.2008.21},
abstract = {First-order logic models of security for cryptographic protocols,
based on variants of the Dolev-Yao model, are now well-established
tools. Given that we have checked a given security protocol~\(\pi\)
using a given first-order prover, how hard is it to extract a
formally checkable proof of~it, as~required in, e.g., common
criteria at evaluation level~\(7\)? We~demonstrate that this is
surprisingly hard: the problem is non-recursive in general.
On~the practical side, we show how we can extract finite models~\(\mathcal{M}\)
from a set~\(\mathcal{S}\) of clauses representing~\(\pi\),
automatically, in two ways. We~then define a model-checker
testing \(\mathcal{M} \models \mathcal{S}\), and show how we can instrument it
to output a formally checkable proof, e.g., in~Coq. This was
implemented in the \texttt{h1} tool suite. Experience on a number of
protocols shows that this is practical.}
}
@article{JGL-mscs09,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {{D}e~{G}root Duality and Models of Choice: Angels, Demons, and Nature},
volume = {20},
number = 2,
pages = {169-237},
month = apr,
year = 2010,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-mscs09.pdf},
doi = {10.1017/S0960129509990363},
abstract = {We introduce convex-concave duality for various models of
non-deterministic choice, probabilistic choice, and the two of them
together. This complements the well-known duality of stably compact spaces
in a pleasing way: convex-concave duality swaps angelic and demonic
choice, and leaves probabilistic choice invariant.}
}
@inproceedings{JGL-asian09,
address = {Seoul, Korea},
month = dec,
year = 2009,
volume = 5913,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Datta, Anupam},
acronym = {{ASIAN}'09},
booktitle = {{P}roceedings of the 13th {A}sian
{C}omputing {S}cience {C}onference
({ASIAN}'09)},
author = {Goubault{-}Larrecq, Jean},
title = {{\textquotedbl}{L}ogic Wins!{\textquotedbl}},
pages = {1-16},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-asian09.pdf},
doi = {10.1007/978-3-642-10622-4_1},
abstract = {Clever algorithm design is sometimes superseded by simple
encodings into logic. We apply this motto to a few case studies in the
formal verification of security properties. In particular, we examine
confidentiality objectives in hardware circuit descriptions written in
VHDL.}
}
@techreport{LSV:09:09,
author = {Goubault{-}Larrecq, Jean},
title = {On a Generalization of a Result by {V}alk and {J}antzen},
institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
ENS Cachan, France},
year = {2009},
month = may,
type = {Research Report},
number = {LSV-09-09},
url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-09.pdf},
note = {18~pages},
abstract = {We~show that, under mild assumptions on the effective, well
quasi-ordered set~\(X\), one~can compute a finite basis of an
upward-closed subset~\(U\) of~\(X\) if and only if one can decide whether
\(U \cap \downarrow z\) is empty for every \(z \in \widehat{X}\). Here
\(\widehat{X}\) is the completion of \(X\) as defined in Finkel and
Goubault-Larrecq, {\em Forward Analysis for WSTS, Part~{I:} Completions},
STACS'09, pages 433-444, 2009. This generalizes a useful result proved by
Valk and Jantzen in~1985, which is the case \(X = \\mathbb{N}^k\).}
}
@article{goubault-jcs09,
publisher = {{IOS} Press},
journal = {Journal of Computer Security},
author = {Goubault{-}Larrecq, Jean},
title = {Finite Models for Formal Security Proofs},
volume = 18,
number = 6,
pages = {1247-1299},
year = 2010,
month = nov,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-jcs09.pdf},
doi = {10.3233/JCS-2009-0395},
abstract = {First-order logic models of security for cryptographic
protocols, based on variants of the Dolev-Yao model, are now
well-established tools. Given that we have checked a given security
protocol using a given first-order prover, how hard is it to extract a
formally checkable proof of it, as required in, \textit{e.g.}, common
criteria at the highest evaluation level~(EAL7)? We~demonstrate that this
is surprisingly hard in the general case: the problem is non-recursive.
Nonetheless, we show that we can instead extract finite
models~\(\mathcal{M}\) from a set~\(S\) of clauses representing~\(\pi\),
automatically, and give two ways of doing~so. We~then define a
model-checker testing \(\mathcal{M} \models S\), and show how we can
instrument it to output a formally checkable proof, \textit{e.g.}, in~Coq.
Experience on a number of protocols shows that this is practical, and that
even complex (secure) protocols modulo equational theories have small
finite models, making our approach suitable.}
}
@inproceedings{FGL-icalp09,
address = {Rhodes, Greece},
month = jul,
year = 2009,
volume = 5556,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Albers, Susanne and Marchetti-Spaccamela, Alberto and
Matias, Yossi and Thomas, Wolfgang},
acronym = {{ICALP}'09},
booktitle = {{P}roceedings of the 36th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
pages = {188-199},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-icalp09.pdf},
doi = {10.1007/978-3-642-02930-1_16},
abstract = {We~describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathcal{S}\). This computes the \emph{clover}
of a state~\(s_0\) , \textit{i.e.}, a~finite description of the closure of
the cover of~\(s_0\) . When \(S\) is the completion of a
WSTS~\(\mathcal{X}\), the clover in~\(\mathcal{S}\) is a finite
description of the cover in~\(\mathcal{X}\). We~show that this applies
exactly when \(\mathcal{X}\) is an \(\omega^2\)-WSTS, a~new robust class
of WSTS. We~show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets. We
characterize the WSTS where our procedure terminates as those that are
\emph{clover-flattable}. Finally, we~apply this to well-structured counter
systems.}
}
@inproceedings{FGL-stacs2009,
address = {Freiburg, Germany},
month = feb,
year = 2009,
volume = 3,
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Albers, Susanne and Marion, Jean-Yves},
acronym = {{STACS}'09},
booktitle = {{P}roceedings of the 26th {A}nnual
{S}ymposium on {T}heoretical {A}spects of
{C}omputer {S}cience
({STACS}'09)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for~{WSTS}, Part~{I}: Completions},
pages = {433-444},
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGL-stacs2009.pdf},
abstract = {Well-structured transition systems provide the right foundation
to compute a finite basis of the set of predecessors of the upward closure
of a state. The~dual problem, to compute a finite representation of the
set of successors of the downward closure of a state, is~harder: Until
now, the theoretical framework for manipulating downward-closed sets was
missing. We~answer this problem, using insights from domain theory (dcpos
and ideal completions), from topology (sobrifications), and shed new light
on the notion of adequate domains of limits.}
}
@inproceedings{BGGLP-scan10,
address = {Lyon, France},
month = sep,
year = 2010,
noeditor = {},
acronym = {SCAN'10},
booktitle = {{P}roceedings of the 14th {GAMM}-{IMACS} {I}nternational
{S}ymposium on {S}cientific {C}omputing, {C}omputer
{A}rithmetic and {V}alidated {N}umerics ({SCAN}'10)},
author = {Bouissou, Olivier and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean and Putot, Sylvie},
title = {A Generalization of {P}-boxes to Affine Arithmetic, and Applications to
Static Analysis of Programs},
nopages = {}
}
@article{GLK-mscs10,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean and Keimel, Klaus},
title = {{C}hoquet-{K}endall-{M}atheron Theorems for Non-{H}ausdorff
Spaces},
volume = 21,
number = 3,
pages = {511-561},
month = jun,
year = 2011,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLK-mscs10.pdf},
doi = {10.1017/S0960129510000617},
abstract = {We establish Choquet-Kendall-Matheron theorems on non-Hausdorff
topological spaces. This typical result of random set theory is profitably
recast in purely topological terms, using intuitions and tools from domain
theory. We obtain three variants of the theorem, each one characterizing
distributions, in the form of continuous valuations, over relevant
powerdomains of demonic, resp. angelic, resp. erratic non-determinism.}
}
@inproceedings{bgl-setop10,
address = {Athens, Greece},
month = sep,
year = 2010,
volume = 6514,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cavalli, Ana and Leneutre, Jean},
acronym = {{DPM}{{\slash}}{SETOP}'10},
booktitle = {{R}evised {S}elected {P}apers of the 5th {I}nternational {W}orkshop
on {D}ata {P}rivacy {M}anagement and {A}utonomous
{S}pontaneous {S}ecurity ({DPM}'10) and 3rd {I}nternational
{W}orkshop on {A}utonomous
and {S}pontaneous {S}ecurity ({SETOP}'10)},
author = {Benzina, Hedi and Goubault{-}Larrecq, Jean},
title = {Some Ideas on Virtualized Systems Security, and Monitors},
pages = {244-258},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/bgl-setop10.pdf},
doi = {10.1007/978-3-642-19348-4_18},
abstract = {Virtualized systems such as Xen, VirtualBox, VMWare or QEmu have
been proposed to increase the level of security achievable on personal
computers. On the other hand, such virtualized systems are now targets for
attacks. We propose an intrusion detection architecture for virtualized
systems, and discuss some of the security issues that arise. We argue that
a weak spot of such systems is domain zero administration, which is left
entirely under the administrator's responsibility, and is in particular
vulnerable to trojans. To~avert some of the risks, we~propose to install a
role-based access control model with possible role delegation, and to
describe all undesired activity ows through simple temporal formulas. We
show how the latter are compiled into Orchids rules, via a fragment of
linear temporal logic, through a generalization of the so-called history
variable mechanism.}
}
@inproceedings{JGL-icalp10,
address = {Bordeaux, France},
month = jul,
year = 2010,
volume = 6199,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Abramsky, Samson and Meyer{ }auf{ }der{ }Heide, Friedhelm
and Spirakis, Paul},
acronym = {{ICALP}'10},
booktitle = {{P}roceedings of the 37th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'10)~-- {P}art~{II}},
author = {Goubault{-}Larrecq, Jean},
title = {Noetherian Spaces in Verification},
pages = {2-21},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-icalp10.pdf},
doi = {10.1007/978-3-642-14162-1_2},
abstract = {Noetherian spaces are a topological concept that generalizes
well quasiorderings. We explore applications to infinite-state
verification problems, and show how this stimulated the search for
infinite procedures \`a la Karp-Miller.}
}
@inproceedings{JGL-lics10,
address = {Edinburgh, Scotland, UK},
month = jul,
year = 2010,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'10},
booktitle = {{P}roceedings of the 25th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'10)},
author = {Goubault{-}Larrecq, Jean},
title = {{{\(\omega\)}}{\textbf{\MakeUppercase{QRB}}}-Domains and the
Probabilistic Powerdomain},
pages = {352-361},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lics10.pdf},
doi = {10.1109/LICS.2010.50},
abstract = {Is there any cartesian-closed category of continuous domains
that would be closed under Jones and Plotkin's probabilistic powerdomain
construction? This is a major open problem in the area of denotational
semantics of probabilistic higher-order languages. We relax the question,
and look for quasi-continuous dcpos instead. We introduce a natural class
of such quasi-continuous dcpos, the \(\omega\textbf{QRB}\)-domains. We
show that they form a category \(\omega\textbf{QRB}\) with pleasing
properties: \(\omega\textbf{QRB}\) is closed under the probabilistic
powerdomain functor, has all finite products, all bilimits, and is stable
under retracts, and even under so-called quasiretracts. But...
\(\omega\textbf{QRB}\) is not cartesian closed.}
}
@misc{JGL-tacl11,
author = {Jean Goubault{-}Larrecq},
title = {A Few Pearls in the Theory of Quasi-Metric Spaces},
year = {2011},
month = jul,
howpublished = {Invited talk, Fifth International Conference on Topology,
Algebra, and Categories in Logic (TACL'11), Marseilles,
France, July~2011}
}
@article{FG-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {Forward Analysis for {WSTS}, Part~{II}: Complete {WSTS}},
year = 2012,
month = sep,
volume = 8,
number = {3:28},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FG-lmcs12.pdf},
doi = {10.2168/LMCS-8(3:28)2012},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show
that such completions are infinity-complete exactly when
\(\mathfrak{X}\) is an \(\omega^2\)-WSTS, a~new robust class of WSTS.
We show that our procedure terminates in more cases than the
generalized Karp-Miller procedure on extensions of Petri nets and on
lossy channel systems. We characterize the WSTS where our procedure
terminates as those that are \emph{clover-flattable}. Finally, we
apply this to well-structured counter systems.}
}
@article{JGL-lmcs12,
journal = {Logical Methods in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {{QRB}-Domains and the Probabilistic Powerdomain},
year = 2012,
volume = 8,
number = {1:14},
nopages = {},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf},
doi = {10.2168/LMCS-8(1:14)2012},
abstract = {Is there any Cartesian-closed category of continuous
domains that would be closed under Jones and Plotkin's
probabilistic powerdomain construction? This is a major open
problem in the area of denotational semantics of probabilistic
higher-order languages. We relax the question, and look for
quasi-continuous dcpos instead.\par
We introduce a natural class of such quasi-continuous dcpos, the
omega-QRB-domains. We show that they form a category omega-QRB
with pleasing properties: omega-QRB is closed under the
probabilistic powerdomain functor, under finite products, under
taking bilimits of expanding sequences, under retracts, and
even under so-called quasi-retracts. But... omega-QRB is
not Cartesian closed. We conclude by showing that the QRB
domains are just one half of an FS-domain, merely lacking
control.}
}
@article{BGGLP-comp11,
publisher = {Springer},
journal = {Computing},
author = {Bouissou, Olivier and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean and Putot, Sylvie},
title = {A Generalization of {P}-boxes to Affine Arithmetic, and Applications to
Static Analysis of Programs},
year = 2012,
month = mar,
volume = 94,
number = {2-4},
pages = {189-201},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/BGGLP-comp11.pdf},
doi = {10.1007/s00607-011-0182-8},
abstract = {We often need to deal with information that contains
both interval and probabilistic uncertainties. P-boxes and
Dempster-Shafer structures are models that unify both kind of
information, but they suffer from the main defect of intervals,
the wrapping effect. We present here a new arithmetic that
mixes, in a guaranteed manner, interval uncertainty with
probabilities, while using some information about variable
dependencies, hence limiting the loss from not accounting for
correlations. This increases the precision of the result and
decreases the computation time compared to standard p-box
arithmetic.}
}
@misc{orchids-v1.0,
author = {Olivain, Julien and Goubault{-}Larrecq, Jean and Benzina,
Hedi and Gourdin, Baptiste and Ben{~}Youn{\`e}s, Romdhane},
title = {{ORCHIDS}},
year = {2011},
nmnote = {See~\url{http://www.lsv.ens-cachan.fr/orchids/} for
description. Written in C (about 48800 lines)},
nmnote-fr = {Voir~\url{http://www.lsv.ens-cachan.fr/orchids/} pour la
description. \'Ecrit en~C (environ 48800 lignes)},
url = {http://www.lsv.ens-cachan.fr/Software/orchids/},
abstract = {An efficient, on-line, real-time, multi-event intrusion
detection system originally based on model-checking ideas.}
}
@inproceedings{GLV-lics2011,
address = {Toronto, Canada},
month = jun,
year = 2011,
publisher = {{IEEE} Computer Society Press},
acronym = {{LICS}'11},
booktitle = {{P}roceedings of the 26th
{A}nnual {IEEE} {S}ymposium on
{L}ogic in {C}omputer {S}cience
({LICS}'11)},
author = {Goubault{-}Larrecq, Jean and Varacca, Daniele},
title = {Continuous Random Variables},
pages = {97-106},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLV-lics2011-errata.pdf},
doi = {10.1109/LICS.2011.23},
abstract = {We introduce the domain of continuous random variables (CRV)
over a domain, as an alternative to Jones and Plotkin's probabilistic
powerdomain. While no known Cartesian-closed category is stable under the
latter, we show that the so-called thin (uniform) CRVs define a strong
monad on the Cartesian-closed category of bc-domains. We also characterize
their inequational theory, as (fair-)coin algebras. We apply this to solve
a recent problem posed by M. Escard{\'o}: testing is semi-decidable for
EPCF terms. CRVs arose from the study of the second author's (layered)
Hoare indexed valuations, and we also make the connection apparent.}
}
@article{JGL-jyg10,
publisher = {Elsevier Science Publishers},
journal = {Theoretical Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Musings Around the Geometry of Interaction, and Coherence},
volume = 412,
number = 20,
pages = {1998-2014},
year = 2011,
month = apr,
url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/jgl-jyg10.pdf},
doi = {10.1016/j.tcs.2010.12.023},
abstract = {We introduce the Danos-R{\'e}gnier category \(\mathcal{DR}(M)\)
of a linear inverse monoid~\(M\), as~a categorical description of
geometries of interaction~(GOI) inspired from the weight algebra. The
natural setting for GOI is that of a so-called weakly Cantorian linear
inverse monoid, in which case \(\mathcal{DR}(M)\) is a kind of symmetrized
version of the classical Abramsky-Haghverdi-Scott construction of a weak
linear category from a GOI situation. It is well-known that GOI is
perfectly suited to describe the multiplicative fragment of linear logic,
and indeed \(\mathcal{DR}(M)\) will be a \(\star\)-autonomous category in
this case. It is also well-known that the categorical interpretation of
the other linear connectives conflicts with GOI interpretations. We make
this precise, and show that \(\mathcal{DR}(M)\) has no terminal object, no
cartesian product of any two objects, and no exponential---whatever
\(M\)~is, unless \(M\)~is trivial. However, a form of coherence completion
of \(\mathcal{DR}(M)\) \textit{{\`a} la} Hu-Joyal (which for additives
resembles a layered approach \textit{{\`a} la} Hughes-van Glabbeek),
provides a model of full classical linear logic, as soon as \(M\) is
weakly Cantorian. One finally notes that Girard's notion of \emph{coherence} is
pervasive, and instrumental in every aspect of this work.}
}
@techreport{AGL-arxiv12,
author = {Adj{\'e}, Assal{\'e} and Goubault{-}Larrecq, Jean},
title = {Concrete Semantics of Programs with Non-Deterministic and
Random Inputs},
year = {2012},
month = oct,
type = {Research Report},
institution = {Computing Research Repository},
number = {cs.LO/1210.2605},
url = {http://arxiv.org/abs/1210.2605},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AGL-arxiv12.pdf},
originalpdf = {http://arxiv.org/pdf/1210.2605},
note = {19~pages},
abstract = {This document gives semantics to programs written in a C-like
programming language, featuring interactions with an external environment
with noisy and imprecise data.}
}
@inproceedings{FGL-pn12,
address = {Hamburg, Germany},
month = jun,
year = 2012,
volume = 7347,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Haddad, Serge and Pomello, Lucia},
acronym = {{PETRI~NETS}'12},
booktitle = {{P}roceedings of the 33rd
{I}nternational {C}onference on
{A}pplications and {T}heory of {P}etri {N}ets
({PETRI~NETS}'12)},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {The~Theory of~{WSTS}: The~Case of Complete~{WSTS}},
pages = {3-31},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/FGL-atpn12.pdf},
doi = {10.1007/978-3-642-31131-4_2},
abstract = {We describe a simple, conceptual forward analysis procedure for
\(\infty\)-complete WSTS~\(\mathfrak{S}\). This computes the so-called
\emph{clover} of a state. When \(\mathfrak{S}\) is the completion of a
WSTS~\(\mathfrak{X}\), the clover in~\(\mathfrak{S}\) is a finite
description of the downward closure of the reachability set. We show that
such completions are \(\infty\)-complete exactly when \(\mathfrak{X}\) is
an \emph{\(\omega^{2}\)-WSTS}, a new robust class of WSTS. We show that
our procedure terminates in more cases than the generalized Karp-Miller
procedure on extensions of Petri nets. We characterize the WSTS where our
procedure terminates as those that are \emph{clover-flattable}. Finally,
we apply this to well-structured Presburger counter systems.}
}
@book{JGL-topology,
author = {Goubault{-}Larrecq, Jean},
title = {Non-{H}ausdorff Topology and Domain Theory---Selected Topics
in Point-Set Topology},
publisher = {Cambridge University Press},
series = {New Mathematical Monographs},
volume = {22},
year = {2013},
month = mar,
url = {http://www.cambridge.org/9781107034136},
isbn = {9781107034136}
}
@inproceedings{JGL-mfcs13,
address = {Klosterneuburg, Austria},
month = aug,
year = 2013,
volume = {8087},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Chatterjee, Krishnendu and Sgall, Ji{\v{r}}{\'\i}},
acronym = {{MFCS}'13},
booktitle = {{P}roceedings of the 38th
{I}nternational {S}ymposium on
{M}athematical {F}oundations of
{C}omputer {S}cience
({MFCS}'13)},
author = {Goubault{-}Larrecq, Jean},
title = {A Constructive Proof of the Topological {K}ruskal Theorem},
pages = {22-41},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mfcs13.pdf},
doi = {10.1007/978-3-642-40313-2_3},
abstract = {We give a constructive proof of Kruskal's Tree
Theorem---precisely, of a topological extension of~it. The proof is in the
style of a constructive proof of Higman's Lemma due to Murthy and
Russell~(1990), and illuminates the role of regular expressions there. In
the process, we discover an extension of Dershowitz' recursive path
ordering to a form of cyclic terms which we call \(\mu\)-terms. This all came
from recent research on Noetherian spaces, and serves as a teaser for
their theory.}
}
@inproceedings{ABGGP-vstte13,
address = {Atherton, California, USA},
year = 2014,
volume = 8164,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Cohen, Ernie and Rybalchenko, Andrey},
acronym = {{VSTTE}'13},
booktitle = {{R}evised {S}elected {P}apers of the
5th {IFIP} {TC2}\slash{WG2.3} {C}onference {V}erified
{S}oftware---{T}heories, {T}ools, and {E}xperiments
({VSTTE}'13)},
author = {Adj{\'e}, Assal{\'e} and Bouissou, Olivier and
Goubault{-}Larrecq, Jean and
Goubault, {\'E}ric and Putot, Sylvie},
title = {Static Analysis of Programs with Imprecise Probabilistic Inputs},
pages = {22-47},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/ABGGP-vstte13.pdf},
doi = {10.1007/978-3-642-54108-7},
abstract = {Having a precise yet sound abstraction of the inputs of
numerical programs is important to analyze their behavior. For many
programs, these inputs are probabilistic, but the actual distribution used
is only partially known. We present a static analysis framework for
reasoning about programs with inputs given as imprecise probabilities: we
define a collecting semantics based on the notion of previsions and an
abstract semantics based on an extension of Dempster-Shafer structures. We
prove the correctness of our approach and show on some realistic examples
the kind of invariants we are able to infer.}
}
@incollection{GLJ-hg13,
noaddress = {},
month = jan,
year = 2013,
volume = 7797,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
noacronym = {},
booktitle = {Programming Logics~-- Essays in Memory of {H}arald {G}anzinger},
editor = {Voronkov, Andrei and Weidenbach, Christoph},
author = {Goubault{-}Larrecq, Jean and Jouannaud, Jean-Pierre},
title = {The Blossom of Finite Semantic Trees},
pages = {90-122},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-hg13.pdf}
}
@inproceedings{GLJ-mfps30,
address = {Ithaca, New~York, USA},
month = jun,
year = 2014,
volume = 308,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jacobs, Bart and Silva, Alexandra and Staton, Sam},
acronym = {{MFPS}'14},
booktitle = {{P}roceedings of the 30th {C}onference on
{M}athematical {F}oundations of {P}rogramming
{S}emantics ({MFPS}'14)},
author = {Goubault{-}Larrecq, Jean and Jung, Achim},
title = {{QRB}, {QFS}, and the Probabilistic Powerdomain},
pages = {167-182},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLJ-mfps14.pdf},
doi = {10.1016/j.entcs.2014.10.010},
abstract = {We show that the first author's QRB-domains coincide with Li and
Xu's QFS-domains, and also with Lawson-compact quasi-continuous dcpos,
with stably-compact locally finitary compact spaces, with sober
QFS-spaces, and with sober QRB-spaces. The first three coincidences were
discovered independently by Lawson and~Xi. The equivalence with sober
QFS-spaces is then applied to give a novel, direct proof that the
probabilistic powerdomain of a QRB-domain is a QRB-domain. This improves
upon a previous, similar result, which was limited to pointed,
second-countable QRB-domains.}
}
@article{jgl-jlap14,
publisher = {Elsevier Science Publishers},
journal = {Journal of Logic and Algebraic Methods in Programming},
author = {Goubault{-}Larrecq, Jean},
title = {Full Abstraction for Non-Deterministic and Probabilistic
Extensions of {PCF}~{I}: the~Angelic Cases},
volume = 84,
number = 1,
year = 2015,
month = jan,
pages = {155-184},
opteditor = {Berger, Ulrich},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/jgl-jlap14.pdf},
doi = {10.1016/j.jlamp.2014.09.003},
abstract = {We examine several extensions and variants of Plotkin's
language~PCF, including non-deterministic and probabilistic choice
constructs. For~each, we give an operational and a denotational semantics,
and compare them. In each case, we show soundness and computational
adequacy: the two semantics compute the same values at ground types.
Beyond this, we establish full abstraction (the~observational preorder
coincides with the denotational preorder) in a number of cases. In~the
probabilistic cases, this requires the addition of so-called statistical
termination testers to the language.}
}
@inproceedings{GLS-pp14,
year = 2014,
volume = 8464,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {van Breugel, Franck and Kashefi, Elham and Palamidessi,
Catuscia and Rutten, Jan},
booktitle = {Horizons of the Mind. A~Tribute to Prakash Panangaden},
author = {Goubault{-}Larrecq, Jean and Segala, Roberto},
title = {Random Measurable Selections},
pages = {343-362},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-pp14.pdf},
doi = {10.1007/978-3-319-06880-0_18},
abstract = {We make the first steps towards showing a general {"}randomness
for free{"} theorem for stochastic automata. The goal of such theorems is
to replace randomized schedulers by averages of pure schedulers. Here, we
explore the case of measurable multifunctions and their measurable
selections. This involves constructing probability measures on the
measurable space of measurable selections of a given measurable
multifunction, which seems to be a fairly novel problem. We then extend
this to the case of IT automata, namely, non-deterministic (infinite)
automata with a history-dependent transition relation. Throughout, we
strive to make our assumptions minimal.}
}
@article{GL-acs13,
publisher = {Springer},
journal = {Applied Categorical Structures},
author = {Goubault{-}Larrecq, Jean},
title = {Exponentiable streams and prestreams},
volume = {22},
number = {3},
year = 2014,
month = jun,
pages = {515-549},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13.pdf},
corrigendumpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf},
doi = { 10.1007/s10485-013-9315-x},
note = {Errata 1: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum.pdf};
Errata 2: \url{http://www.lsv.fr/Publis/PAPERS/PDF/GL-acs13-erratum2.pdf}},
abstract = {Inspired by a construction of Escard{\'o}, Lawson, and Simpson,
we give a general construction of \(\mathcal C\)-generated objects in a
topological construct. When \(\mathcal C\) consists of exponentiable
objects, the resulting category is Cartesian-closed. This generalizes the
familiar construction of compactly-generated spaces, and we apply this to
Krishnan's categories of streams and prestreams, as well as to Haucourt
streams. For that, we need to identify the exponentiable objects in these
categories: for prestreams, we show that these are the preordered
core-compact topological spaces, and for streams, these are the
core-compact streams.}
}
@article{GL-mscs13,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {A~short proof of the {S}chr{\"o}der-{S}impson theorem},
volume = 25,
number = 1,
year = 2015,
month = jan,
pages = {1-5},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GL-mscs13.pdf},
doi = {10.1017/S0960129513000467},
abstract = {We give a short and elementary proof of the
Schr{\"o}der-Simpson Theorem, which states that the space of all
continuous maps from a given space~\(X\) to the non-negative reals with their
Scott topology is the cone-theoretic dual of the probabilistic powerdomain
on~\(X\).}
}
@inproceedings{DGGL-icalp15,
address = {Kyoto, Japan},
month = jul,
year = 2015,
volume = {9135},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Halld{\'o}rsson, Magnus M. and Iwama, Kazuo and Kobayashi,
Naoki and Speckmann, Bettina},
acronym = {{ICALP}'15},
booktitle = {{P}roceedings of the 42nd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'15)~-- {P}art~{II}},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {Natural Homology},
pages = {171-183},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-icalp15.pdf},
doi = {10.1007/978-3-662-47666-6_14},
abstract = {We propose a notion of homology for directed algebraic topology,
based on so-called natural systems of abelian groups, and which we call
natural homology. Contrarily to previous proposals, and as we show,
natural homology has many desirable properties: it~is invariant under
isomorphisms of directed spaces, it is invariant under refinement
(subdivision), and it is computable on cubical complexes.}
}
@article{AFG-sif15,
publisher = {SIF},
journal = {1024~-- Bulletin de la soci{\'e}t{\'e} informatique de France},
author = {Abiteboul, Serge and Fribourg, Laurent and
Goubault{-}Larrecq, Jean},
title = {{G}{\'e}rard {B}erry~: un~informaticien m{\'e}daille d'or du {CNRS}~2014},
volume = 4,
pages = {139-142},
month = oct,
year = 2014,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/AFG-sif15.pdf},
abstract = {C'est un chercheur en informatique qui vient de recevoir la
m{\'e}daille d'or du CNRS, la plus haute distinction scientifique fran{\c
c}aise toutes disciplines confondues. Les informaticiens sont rares {\`a}
avoir {\'e}t{\'e} ainsi honor{\'e}s : ce n'est que la seconde fois
apr{\`e}s Jacques Stern en~2006.}
}
@inproceedings{GLO-fps13,
address = {La Rochelle, France},
month = oct,
year = 2013,
volume = 8352,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Danger, Jean-Luc and Debbabi, Mourad and Marion, Jean-Yves and
Garcia{-}Alfaro, Joaquin and Zincir{-}Heywood,Nur},
acronym = {{FPS}'13},
booktitle = {{R}evised {S}elected {P}apers of the 6th {I}nternational {S}ymposium on
{F}oundations and {P}ractice of {S}ecurity ({FPS}'13)},
author = {Goubault{-}Larrecq, Jean and Olivain, Julien},
title = {On~the Efficiency of Mathematics in Intrusion
Detection: The NetEntropy Case.},
pages = {3-16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLO-fps13.pdf},
doi = {10.1007/978-3-319-05302-8_1},
abstract = {NetEntropy is a plugin to the Orchids intrusion detection tool
that is originally meant to detect some subtle attacks on implementations
of cryptographic protocols such as {SSL\slash TLS}. NetEntropy compares
the sample entropy of a data stream to a known profile, and flags any
significant variation. Our point is to stress the \emph{mathematics} behind
NetEntropy: the reason of the rather incredible precision of NetEntropy is
to be found in theorems due to Paninski and Moddemeijer.}
}
@article{GLSSW-dagrep16,
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
journal = {Dagstuhl Reports},
author = {Goubault{-}Larrecq, Jean and Seisenberger, Monika and Selivanov, Victor and Weiermann, Andreas},
title = {Well {Q}uasi-{O}rders in {C}omputer {S}cience ({D}agstuhl {S}eminar
16031)},
year = 2016,
month = jan,
volume = {6},
number = {1},
pages = {69-98},
url = {http://dx.doi.org/10.4230/DagRep.6.1.69},
pdf = {http://dx.doi.org/10.4230/DagRep.6.1.69},
doi = {10.4230/DagRep.6.1.69},
abstract = {This report documents the program and the outcomes of Dagstuhl Seminar 16031 {"}Well Quasi{-}Orders in Computer
Science{"}, the first seminar devoted to the multiple and deep interactions between the theory of Well quasi{-}orders
(known as the Wqo{-}Theory) and several fields of Computer Science (Verification and Termination of Infinite-State Systems,
Automata and Formal Languages, Term Rewriting and Proof Theory, topological complexity of computational problems on continuous
functions). Wqo{-}Theory is a highly developed part of Combinatorics with ever-growing number of applications in Mathematics and
Computer Science, and Well quasi-orders are going to become an important unifying concept of Theoretical Computer Science.
In this seminar, we brought together several communities from Computer Science and Mathematics in order to facilitate the
knowledge transfer between Mathematicians and Computer Scientists as well as between established and younger researchers and thus
to push forward the interaction between Wqo{-}Theory and Computer Science.}
}
@inproceedings{GLL-rv16,
address = {Madrid, Spain},
volume = 10012,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {Madrid, Spain},
acronym = {{RV}'16},
booktitle = {{P}roceedings of the 16th {C}onference on {R}untime {V}erification ({RV}'16)},
author = {Goubault{-}Larrecq, Jean and Lachance, Jean{-}Philippe},
title = {On the {C}omplexity of {M}onitoring {O}rchids {S}ignatures},
year = 2016,
month = sep,
pages = {169-164},
opturl = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11},
optpdf = {http://link.springer.com/chapter/10.1007%2F978-3-319-46982-9_11},
doi = {10.1007/978-3-319-46982-9_11},
abstract = {Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let f(n) be the maximum number of monitor instances that can be fired on a sequence of n events: we design an algorithm that decides whether f(n) is asymptotically exponential or polynomial, and in the latter case returns an exponent d such that f(n)=Theta(n^d) . Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators + and max, and defining integer sequences u_n, what is the asymptotic behavior of u_n as n tends to infinity? We show that, under simple assumptions, u_n is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan’s strongly connected components algorithm, in linear time.}
}
@inproceedings{DGGL-csl16,
address = {Marseille, France},
month = sep,
year = 2016,
volume = {62},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Regnier, Laurent and Talbot, Jean-Marc},
acronym = {{CSL}'16},
booktitle = {{P}roceedings of the 25th {A}nnual {EACSL} {C}onference on
{C}omputer {S}cience {L}ogic ({CSL}'16)},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {The Directed Homotopy Hypothesis},
pages = {9:1-9:16},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DBS-csl16.pdf},
doi = {10.4230/LIPIcs.CSL.2016.9},
abstract = {The homotopy hypothesis was originally stated by Grothendieck: topological spaces should be {"}equivalent{"} to (weak) infinite-groupoids, which give algebraic representatives of homotopy types. Much later, several authors developed geometrizations of computational models, e.g., for rewriting, distributed systems, (homotopy) type theory etc. But an essential feature in the work set up in concurrency theory, is that time should be considered irreversible, giving rise to the field of directed algebraic topology. Following the path proposed by Porter, we state here a directed homotopy hypothesis: Grandis' directed topological spaces should be {"}equivalent{"} to a weak form of topologically enriched categories, still very close to (infinite,1)-categories. We develop, as in ordinary algebraic topology, a directed homotopy equivalence and a weak equivalence, and show invariance of a form of directed homology.}
}
@inproceedings{DGGL-concur16,
address = {Qu{\'e}bec City, Canada},
month = aug,
year = 2016,
volume = {59},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Desharnais, Jos{\'e}e and Jagadeesan, Radha},
acronym = {{CONCUR}'16},
booktitle = {{P}roceedings of the 27th
{I}nternational {C}onference on
{C}oncurrency {T}heory
({CONCUR}'16)},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and Goubault{-}Larrecq, Jean},
title = {Bisimulations and unfolding in {{\(\mathcal{P}\)}}-accessible categorical models},
pages = {25:1-25:14},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGGL-concur16.pdf},
doi = {10.4230/LIPIcs.CONCUR.2016.25},
abstract = {We propose a categorical framework for bisimulations and
unfoldings that unifies the classical approach from Joyal
\emph{et~al.} via open maps and unfoldings. This is based on a
notion of categories accessible with respect to a subcategory of
path shapes, i.e., for which one can define a nice notion of trees
as glueings of paths. We show that transition systems and presheaf
models are instances of our framework. We also prove that in our
framework, several notions of bisimulation coincide, in particular
an {"}operational~one{"} akin to the standard definition in
transition systems. Also, our notion of accessibility is preserved
by coreflections. This also leads us to a notion of unfolding that
behaves well in the accessible case: it~is a right adjoint and is a
universal covering, i.e., it is initial among the morphisms that
have the unique lifting property with respect to path shapes. As an
application, we prove that the universal covering of a groupoid, a
standard construction in algebraic topology, is an unfolding, when
the category of path shapes is well chosen.}
}
@article{DGG-acs16,
publisher = {Springer},
journal = {Applied Categorical Structures},
author = {Dubut, J{\'e}r{\'e}my and Goubault, {\'E}ric and
Goubault{-}Larrecq, Jean},
title = {Directed homology theories and {E}ilenberg-{S}teenrod
axioms},
year = 2017,
month = oct,
volume = {25},
number = {5},
pages = {775-807},
url = {http://www.lsv.fr/Publis/PAPERS/PDF/DGG-acs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/DGG-acs16.pdf},
doi = {doi:10.1007/s10485-016-9438-y},
abstract = {In this paper, we define and study a homology theory, that
we call {"}natural homology{"}, which associates a natural system of
abelian groups to every space in a large class of directed spaces
and precubical sets. We show that this homology theory enjoys many
important properties, as an invariant for directed homotopy. Among
its properties, we show that subdivided precubical sets have the
same homology type as the original ones ; similarly, the natural
homology of a precubical set is of the same type as the natural
homology of its geometric realization. By same type we mean
equivalent up to some form of bisimulation, that we define using the
notion of open map. Last but not least, natural homology, for the
class of spaces we consider, exhibits very important properties such
as Hurewicz theorems, and most of Eilenberg-Steenrod axioms, in
particular the dimension, homotopy, additivity and exactness axioms.
This last axiom is studied in a general framework of (generalized)
exact sequences.}
}
@inproceedings{GLS-icalp16,
address = {Rome, Italy},
month = jul,
year = 2016,
volume = {55},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Chatzigiannakis, Ioannis and Mitzenmacher,
Michael and Rabani, Yuval and Sangiorgi, Davide},
acronym = {{ICALP}'16},
booktitle = {{P}roceedings of the 43rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'16)},
author = {Goubault{-}Larrecq, Jean and Schmitz, Sylvain},
title = {Deciding Piecewise Testable Separability for Regular
Tree Languages},
pages = {97:1-97:15},
url = {https://hal.inria.fr/hal-01276119/},
optpdf = {http://www.lsv.fr/Publis/PAPERS/PDF/GLS-icalp16.pdf},
doi = {10.4230/LIPIcs.ICALP.2016.97},
abstract = {The piecewise testable separability problem asks, given
two input languages, whether there exists a piecewise testable
language that contains the first input language and is disjoint from
the second. We prove a general characterisation of piecewise
testable separability on languages in a well-quasi-order, in terms
of ideals of the ordering. This subsumes the known characterisations
in the case of finite words. In the case of finite ranked trees
ordered by homeomorphic embedding, we show using effective
representations for tree ideals that it entails the decidability of
piecewise testable separability when the input languages are
regular. A~final byproduct is a new proof of the decidability of
whether an input regular language of ranked trees is piecewise
testable, which was first shown in the unranked case by Boja{\'n}czyk,
Segoufin, and Straubing (Log.~Meth. in Comput.~Sci.,~8(3:26),
2012).}
}
@comment{{B-arxiv16,
author = Bollig, Benedikt,
affiliation = aff-LSVmexico,
title = One-Counter Automata with Counter Visibility,
institution = Computing Research Repository,
number = 1602.05940,
month = feb,
nmonth = 2,
year = 2016,
type = RR,
axeLSV = mexico,
NOcontrat = "",
url = http://arxiv.org/abs/1602.05940,
PDF = "http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
lsvdate-new = 20160222,
lsvdate-upd = 20160222,
lsvdate-pub = 20160222,
lsv-category = "rapl",
wwwpublic = "public and ccsb",
note = 18~pages,
abstract = "In a one-counter automaton (OCA), one can read a letter
from some finite alphabet, increment and decrement the counter by
one, or test it for zero. It is well-known that universality and
language inclusion for OCAs are undecidable. We consider here OCAs
with counter visibility: Whenever the automaton produces a letter,
it outputs the current counter value along with~it. Hence, its
language is now a set of words over an infinite alphabet. We show
that universality and inclusion for that model are in PSPACE, thus
no harder than the corresponding problems for finite automata, which
can actually be considered as a special case. In fact, we show that
OCAs with counter visibility are effectively determinizable and
closed under all boolean operations. As~a~strict generalization, we
subsequently extend our model by registers. The general nonemptiness
problem being undecidable, we impose a bound on the number of
register comparisons and show that the corresponding nonemptiness
problem is NP-complete.",
}}
@article{JGL-mscs16,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {Isomorphism theorems between models of mixed choice},
volume = {27},
number = {6},
pages = {1032-1067},
month = sep,
year = 2017,
url = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mscs16.pdf},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/JGL-mscs16.pdf},
doi = {10.1017/S0960129515000547},
abstract = {We relate the so-called powercone models of mixed
non-deterministic and probabilistic choice proposed by Tix, Keimel,
Plotkin, Mislove, Ouaknine, Worrell, Morgan, and McIver, to our own models
of previsions. Under suitable topological assumptions, we show that they
are isomorphic. We rely on Keimel's cone-theoretic variants of the
classical Hahn-Banach separation theorems, using functional analytic
methods, and on the Schr{\"o}der-Simpson Theorem.}
}
@article{JGL-minimax17,
publisher = {Heldermann Verlag},
journal = {Minimax Theory and its Applications},
author = {Goubault{-}Larrecq, Jean},
title = {A Non-{H}ausdorff Minimax Theorem},
volume = {3},
number = {1},
year = {2017},
pages = {73-80}
}
@article{GLL-fmsd17,
publisher = {Springer},
journal = {Formal Methods in System Design},
author = {Goubault{-}Larrecq, Jean and Lachance, Jean-Philippe},
title = {On the Complexity of Monitoring {O}rchids Signatures, and Recurrence Equations},
volume = {53},
number = {1},
year = {2018},
month = aug,
pages = {6-32},
doi = {10.1007/s10703-017-0303-x},
url = {https://doi.org/10.1007/s10703-017-0303-x},
abstract = {Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let \(f(n)\) be the maximum number of monitor instances that can be fired on a sequence of \(n\) events: we design an algorithm that decides whether \(f(n)\) is asymptotically exponential or polynomial, and in the latter case returns an exponent \(d\) such that \(f(n)=\Theta(n^d)\). Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators \(+\) and \(\max\), and defining integer sequences \(u_n\), what is the asymptotic behavior of \(u_n\) as \(n\) tends to infinity? We show that, under simple assumptions, \(u_n\) is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan's strongly connected components algorithm, in linear time.},
note = {Special issue of RV'16}
}
@article{GLN-lmcs17,
journal = {Logical Methods in Computer Science},
author = {Goubault{-}Larrecq, Jean and Ng, Kok Min},
title = {A Few Notes on Formal Balls},
volume = {13},
number = {4},
year = {2017},
month = nov,
pages = {1-34},
doi = {10.23638/LMCS-13(4:18)2017},
url = {https://lmcs.episciences.org/4100},
pdf = {https://lmcs.episciences.org/4100/pdf},
note = {Special Issue of the Domains XII Workshop}
}
@inproceedings{BFG-fsttcs17,
address = {Kanpur, India},
month = dec,
year = 2017,
volume = {93},
series = {Leibniz International Proceedings in Informatics},
publisher = {Leibniz-Zentrum f{\"u}r Informatik},
editor = {Satya Lokam and R. Ramanujam},
acronym = {{FSTTCS}'17},
booktitle = {{P}roceedings of the 37th {C}onference on
{F}oundations of {S}oftware {T}echnology and
{T}heoretical {C}omputer {S}cience
({FSTTCS}'17)},
author = {Michael Blondin and Alain Finkel and Jean Goubault{-}Larrecq},
title = {Forward Analysis for {WSTS}, {Part III}: {Karp-Miller} Trees},
pages = {16:1-16:15},
url = {https://hal.archives-ouvertes.fr/hal-01736704/},
pdf = {http://drops.dagstuhl.de/opus/volltexte/2018/8403/pdf/LIPIcs-FSTTCS-2017-16.pdf},
doi = {10.4230/LIPIcs.FSTTCS.2017.16},
abstract = {This paper is a sequel of ''Forward Analysis for WSTS, Part I: Completions'' [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and ''Forward Analysis for WSTS, Part II: Complete WSTS'' [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward reachability analyses of WSTS, using finite representations of downwards-closed sets. We further develop this framework to obtain a generic Karp-Miller algorithm for the new class of very-WSTS. This allows us to show that coverability sets of very-WSTS can be computed as their finite ideal decompositions. Under natural assumptions on positive sequences, we also show that LTL model checking for very-WSTS is decidable. The termination of our procedure rests on a new notion of acceleration levels, which we study. We characterize those domains that allow for only finitely many accelerations, based on ordinal ranks.}
}
@misc{JGL:pls16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Encart dans l'article ''S'adapter {\`a} la cyberguerre'', de Karen Elazari, Pour La Science 459},
month = jan,
title = {Les m{\'e}thodes formelles: l'autre arme de la cybers{\'e}curit{\'e}},
year = {2016},
pages = {50-55}
}
@misc{JGL:stc16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk (plenary speaker), Summer Topology Conference, Leicester, UK},
month = aug,
title = {A few things on Noetherian spaces},
year = {2016}
}
@misc{JGL:gs16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Galway Symposium, Leicester, UK},
month = aug,
title = {An introduction to asymmetric topology and domain theory: why, what, and how},
year = {2016}
}
@misc{JGL:dom15,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Domains XII workshop, Cork, Ireland},
month = aug,
title = {Formal balls},
year = {2015}
}
@misc{JGL:lls14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Matinale de l'innovation Logiciels Libres et S{\'e}curit{\'e}, Paris, France},
month = dec,
title = {D{\'e}tection d'intrusions avec {OrchIDS}},
year = {2014}
}
@misc{JGL:ccc14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Continuity, Computability, Constructivity workshop (CCC), Ljubljana, Slovenia},
month = sep,
title = {Noetherian spaces},
year = {2014}
}
@misc{JGL:cps14,
author = {Goubault{-}Larrecq, Jean},
howpublished = {CPS Summer School, Grenoble, France},
month = jul,
title = {{OrchIDS}: on the value of rigor in intrusion detection},
year = {2014}
}
@misc{JGL:stc13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk (semi-plenary speaker), Summer Topology Conference, North Bay, Ontario, CA},
month = jul,
title = {A few pearls in the theory of quasi-metric spaces},
year = {2013}
}
@misc{JGL:dga13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {S{\'e}minaire DGA Innosciences. DGA, Bagneux},
month = jun,
title = {{OrchIDS}, ou : de l'importance de la s{\'e}mantique},
year = {2013}
}
@misc{JGL:at13,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Workshop on Asymmetric Topology, Summer Topology Conference, North Bay, Ontario, CA},
month = jul,
title = {A short proof of the {Schr{\"o}der-Simpson} theorem},
year = {2013}
}
@misc{JGL:dm16,
author = {Goubault{-}Larrecq, Jean},
howpublished = {Invited talk, Dale Miller Festschrift, Paris Diderot University, Paris},
month = dec,
title = {A semantics for {{\(\nabla\)}}},
year = {2016}
}
@misc{GSHM:dga-inria16,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Hulin-Hubard, Francis and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Rapport final et fourniture 4 du contrat DGA-INRIA Orchids},
month = may,
title = {Etat final des travaux engag{\'e}s sur {Orchids}},
year = {2016}
}
@misc{GM:dga-inria16,
author = {Goubault-Larrecq, Jean and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 3 du contrat DGA-INRIA Orchids},
month = may,
title = {G{\'e}n{\'e}ration de signatures pour le suivi de flux d'informations},
year = {2016}
}
@misc{GSM:dga-inria15,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Rapport interm{\'e}diaire du contrat DGA-INRIA Orchids},
month = may,
title = {Etat d'avancement interm{\'e}diaire des travaux engag{\'e}s sur {OrchIDS}},
year = {2015}
}
@misc{GSM:dga-inria-2-14,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 2 du contrat DGA-INRIA Orchids},
month = may,
title = {Techniques et m{\'e}thodes de g{\'e}n{\'e}ration de signatures pour la d{\'e}tection d'intrusions},
year = {2014}
}
@misc{GSM:dga-inria-1-14,
author = {Goubault-Larrecq, Jean and Sentucq, Pierre-Arnaud and Majorczyk, Fr{\'e}d{\'e}ric},
howpublished = {Fourniture 1 du contrat DGA-INRIA Orchids},
month = may,
title = {Politiques de s{\'e}curit{\'e} syst{\`e}me},
year = {2014}
}
@misc{AG:anr-cpp12,
author = {Adj{\'e}, Assal{\'e} and Goubault-Larrecq, Jean},
howpublished = {Fourniture du projet ANR CPP (Confidence, Proofs, and Probabilities), WP 2, version 1},
month = oct,
title = {Concrete semantics of programs with non-deterministic and random inputs},
year = {2012},
url = {http://arxiv.org/abs/1210.2605}
}
@misc{GL:ARC-ProNoBis-16,
author = {Goubault-Larrecq, Jean},
howpublished = {Rapport final ARC ProNoBis},
month = oct,
title = {{Pronobis: Probability and nondeterminism,
bisimulations and security}},
year = {2007}
}
@article{JGL-mscs18,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Goubault{-}Larrecq, Jean},
title = {A semantics for nabla},
volume = {29},
pages = {1250--1274},
year = {2019},
doi = {10.1017/S0960129518000063},
url = {https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/semantics-for-nabla/A3337AB54DC58CBDDEC78116F4390777}
}
@article{JGL-tp19,
publisher = {Auburn University},
journal = {Topology Proceedings},
author = {Goubault-Larrecq, Jean},
title = {{Spaces with no Infinite Discrete Subspace}},
volume = {53},
year = {2019},
pages = {27--36},
abstract = {We show that the spaces with no infinite discrete subspace are
exactly those in which every closed set is a finite union of
irreducibles. Call them FAC spaces: this generalizes a theorem by
Erdos and Tarski (1943), according to which a preordered set has
no infinite antichain---the finite antichain, or FAC, property---if
and only if all its downwards-closed subsets are finite unions of
ideals. All Noetherian spaces are FAC spaces, and we show that
sober FAC spaces have a simple order-theoretic description.},
note = {\url{http://topology.auburn.edu/tp/reprints/v53/tp53003p1.pdf}}
}
@article{HGJX-lmcs18,
journal = {Logical Methods in Computer Science},
author = {Ho, Weng Kin and Goubault-Larrecq, Jean and Jung, Achim and Xi, Xiaoyong},
title = {{The Ho-Zhao Problem}},
volume = {14},
number = {1},
year = {2018},
month = jan,
pages = {1-19},
doi = {10.23638/LMCS-14(1:7)2018},
url = {https://lmcs.episciences.org/4218},
pdf = {http://www.lsv.fr/Publis/PAPERS/PDF/HGJX-lmcs18.pdf}
}
@inproceedings{JGL-lncs11760,
volume = 11760,
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {M{\'a}rio S. Alvim and Kostas Chatzikokolakis and Carlos Olarte and Franck Valencia},
acronym = {{The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy}},
booktitle = {The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy---Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday},
author = {Goubault{-}Larrecq, Jean},
title = {Fooling the Parallel or Tester with Probability $8/27$},
pages = {313--328},
year = 2019,
note = {Updated version on arXiv:1903.12653},
url = {https://arxiv.org/abs/1903.12653},
abstract = {It is well-known that the higher-order language PCF is not fully abstract: there is a program - the so-called parallel or tester, meant to test whether its input behaves as a parallel or - which never terminates on any input, operationally, but is denotationally non-trivial. We explore a probabilistic variant of PCF, and ask whether the parallel or tester exhibits a similar behavior there. The answer is no: operationally, one can feed the parallel or tester an input that will fool it into thinking it is a parallel or. We show that the largest probability of success of such would-be parallel ors is exactly 8/27. The bound is reached by a very simple probabilistic program. The difficult part is to show that that bound cannot be exceeded.}
}
@inproceedings{DGJL-isdt19,
address = {Yangzhou, China},
month = jun,
volume = 345,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jung, Achim and Li, Qingguo and Xu, Luoshan and Zhang, Guo-Qiang},
acronym = {{ISDT}'19},
booktitle = {{P}roceedings of the {I}nternational {S}ymposium on {D}omain {T}heory ({ISDT}'19)},
author = {de Brecht, Matthew and Goubault{-}Larrecq, Jean and Jia, Xiaodong and Lyu, Zhenchao},
title = {Domain-complete and LCS-complete Spaces},
pages = {3-35},
doi = {10.1016/j.entcs.2019.07.014},
year = 2019
}
@inproceedings{GJ-isdt19,
address = {Yangzhou, China},
month = jun,
volume = 345,
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier Science Publishers},
editor = {Jung, Achim and Li, Qingguo and Xu, Luoshan and Zhang, Guo-Qiang},
acronym = {{ISDT}'19},
booktitle = {{P}roceedings of the {I}nternational {S}ymposium on {D}omain {T}heory ({ISDT}'19)},
author = {Goubault{-}Larrecq, Jean and Jia, Xiaodong},
title = {Algebras of the Extended Probabilistic Powerdomain Monad},
pages = {37-61},
doi = {10.1016/j.entcs.2019.07.015},
year = 2019
}
@article{GM-hjm20,
publisher = {University of Houston},
journal = {Houston Journal of Mathematics},
author = {Goubault{-}Larrecq, Jean and Mynard, Fr{\'e}d{\'e}ric},
title = {Convergence without Points},
volume = {46},
number = {1},
pages = {227-282},
year = 2020,
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/GM-hjm20.pdf}
}
@article{JGL-topa19,
publisher = {Elsevier Science Publishers},
journal = {Topology and its Applications},
author = {Goubault{-}Larrecq, Jean},
title = {Formal Ball Monads},
volume = {263},
pages = {372--391},
year = 2019,
doi = {10.1016/j.topol.2019.06.044},
url = {http://www.sciencedirect.com/science/article/pii/S0166864119302160},
abstract = {The formal ball construction B is a central tool of
quasi-metric space theory. We show that it induces monads on certain
natural categories of quasi-metric spaces, with 1-Lipschitz maps as
morphisms, or with 1-Lipschitz continuous maps as morphisms. Those are
left Kock-Zöberlein monads, and that allows us to characterize their
algebras exactly. As an application, we study so-called Lipschitz
regular spaces, a natural class of spaces that contain all standard
algebraic quasi-metric spaces with relatively compact balls, in
particular all metric spaces whose closed balls are compact. There are
other Lipschitz regular spaces, as we show, and notably all B-algebras.
That includes all spaces of formal balls, with their d+-Scott topology.
The value of Lipschitz regularity is that, for a Lipschitz regular
standard quasi-metric space X,d, the space LX of lower semicontinuous
maps from X to the extended non-negative reals, with the Scott topology,
retracts onto each of the spaces L_alpha(X,d) of alpha-Lipschitz
continuous maps, and that the subspace topology on the latter coincides
with the Scott topology.}
}
@inproceedings{JGL-lics19,
address = {Vancouver, Canada},
month = jun,
publisher = {{IEEE} Press},
editor = {Bouyer, Patricia},
acronym = {{LICS}'19},
booktitle = {{P}roceedings of the 34th {A}nnual {ACM\slash
IEEE} {S}ymposium on {L}ogic {I}n {C}omputer {S}cience ({LICS}'19)},
author = {Goubault{-}Larrecq, Jean},
title = {A Probabilistic and Non-Deterministic Call-by-Push-Value Language},
pages = {1-13},
year = 2019,
doi = {10.1109/LICS.2019.8785809},
abstract = {There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract-and those two primitives are required for that.}
}
@article{FG-mscs20,
publisher = {Cambridge University Press},
journal = {Mathematical Structures in Computer Science},
author = {Finkel, Alain and Goubault{-}Larrecq, Jean},
title = {{Forward analysis for WSTS, part I: completions}},
volume = {30},
number = {7},
pages = {752-832},
doi = {10.1017/S0960129520000195},
year = {2020},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FG-mscs2020.pdf},
url = {http://dx.doi.org/10.1017/S0960129520000195}
}
@article{BFG-lmcs20,
journal = {Logical Methods in Computer Science},
author = {Michael Blondin and Alain Finkel and Jean Goubault{-}Larrecq},
title = {{Forward Analysis for WSTS, Part {III:} Karp-Miller Trees}},
volume = {16},
number = {2},
doi = {10.23638/LMCS-16(2:13)2020},
year = {2020},
url = {https://lmcs.episciences.org/6591}
}
@article{JGL-topa2020,
publisher = {Elsevier Science Publishers},
journal = {Topology and its Applications},
author = {Goubault{-}Larrecq, Jean},
title = {{Some Topological Properties of Spaces of Lipschitz Continuous Maps on Quasi-Metric Spaces}},
volume = {282},
year = 2020,
doi = {10.1016/j.topol.2020.107281},
url = {https://doi.org/10.1016/j.topol.2020.107281}
}
@incollection{GHKNS-til2020,
volume = 53,
series = {Trends In Logic},
publisher = {Springer},
booktitle = {Well-Quasi Orders in Computation, Logic, Language and Reasoning},
editor = {Schuster, Peter M. and Seisenberger, Monika and Weiermann, Andreas},
author = {Jean Goubault{-}Larrecq and Simon Halfon and P. Karandikar and K. {Narayan Kumar} and {\relax Ph}ilippe Schnoebelen},
title = {The Ideal Approach to Computing Closed Subsets in Well-Quasi-Orderings},
pages = {55-105},
year = 2020,
doi = {10.1007/978-3-030-30229-0_3}
}
@article{JGL-tp2020,
publisher = {Auburn University},
journal = {Topology Proceedings},
author = {Goubault{-}Larrecq, Jean},
title = {$\Pi^0_2$ Subsets of Domain-Complete Spaces and Countably Correlated Spaces},
volume = {58},
pages = {13-22},
year = 2020,
note = {E-published on March 24, 2020.},
pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/JGL-tp2020.pdf}
}
This file was generated by bibtex2html 1.98.