@unpublished{talk:wqo:LOP24c,
location = {{LaBRI}},
shortlocation={Highlights},
title = {Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width},
type = {Slides},
abstract = {We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width.},
howpublished = {Slides},
note = {{HIGHLIGHTS} Workshop},
author = {Lopez, Aliaume},
date = {2024-09-18},
year = {2024},
langid = {english},
slides={/ressources/publications/Talks%2000/2024-HIGHLIGHTS-presentation.pdf},
}
@unpublished{LOP24b,
title = {$\mathbb{N}$-polyregular functions arise from well-quasi-orderings},
author = {Lopez, Aliaume},
year = {2024},
type = {preprint},
shortlocation = {Nowhere... yet},
eprint = {2409.07882v1},
arxiv = {2409.07882v1},
archivePrefix = {arXiv},
langid = {english},
abstract = {
A fundamental construction in formal language theory is the Myhill-Nerode congruence on words, whose finiteness characterizes regular language. This construction was generalized to functions from finite words to ℤ by Colcombet, Douéneau-Tabot, and Lopez to characterize the class of so-called ℤ-polyregular functions. In this paper, we relax the notion of equivalence relation to quasi-ordering in order to study the class of ℕ-polyregular functions, that plays the role of ℤ-polyregular functions among functions from finite words to ℕ. The analogue of having a finite index is then being a well-quasi-ordering. This provides a canonical object to describe ℕ-polyregular functions, together with a powerful new characterization of this class.
}
}
@unpublished{wqo:LOP24,
title={Labelled Well Quasi Ordered Classes of Bounded Linear Clique Width},
author={Lopez, Aliaume},
year={2024},
eprint={2405.10894},
arxiv={2405.10894},
archivePrefix={arXiv},
type={preprint},
shortlocation={CSL'25},
langid={english},
pages={25},
abstract={We provide an algorithm to decide whether a class of finite graphs that has bounded linear clique width is well-quasi-ordered by the induced subgraph relation in the presence of a labelling of the vertices, where the class is given by an MSO-transduction from finite words. This study leverages tools from automata theory, and the proof scheme allows to derive a weak version of the Pouzet conjecture for classes of bounded linear clique-width. We also provide an automata based characterization of which classes of NLC graphs are labelled-well-quasi-ordered by the induced subgraph relation, where we recover the results of Daligault Rao and Thomassé by encoding the models into trees with the gap embedding relation of Dershowitz and Tzameret.},
}
@unpublished{zpoly:LOP24,
title={Commutative N-polyregular functions},
author={Lopez, Aliaume},
year={2024},
eprint={2404.02232},
arxiv = {2404.02232},
archivePrefix={arXiv},
type={preprint},
shortlocation={CSL'25},
langid={english},
pages={29},
abstract={This paper addresses two questions regarding N-polyregular functions, that forms a proper subset of N-rational series. We show that given a Z-rational series, it is decidable whether it is computable via a commutative N-polyregular function, and provide a counter-example to the theorem of Karhumäki that studied the same question in the case of polynomials. We also prove that it is decidable whether a commutative N-polyregular function is star-free, by proving the stronger statement that star-free Z-polyregular functions that are N-polyregular are in fact computable using a star-free N-polyregular function. Building towards answering the same questions in the non-commutative case, we present a canonical model of computation of N-polyregular functions by generalizing the notion of residual transducers previously introduced in Z-polyregular functions.},
}
@unpublished{wqo:AHLSSV23,
title={Measuring well quasi-ordered finitary powersets},
author={Abriola, Sergio and Halfon, Simon and Lopez, Aliaume and Schmitz, Sylvain and Schnoebelen, Philippe and Vialard, Isa},
year={2023},
date={2023},
arxiv={2312.14587},
langid={english},
pages={20},
type={preprint},
shortlocation={MSCS},
abstract={The complexity of a well-quasi-order (wqo) can be measured through three classical ordinal invariants: the width as a measure of antichains, the height as a measure of chains, and the maximal order type as a measure of bad sequences. This article considers the "finitary powerset" construction: the collection Pf(X) of finite subsets of a wqo X ordered with the Hoare embedding relation remains a wqo. The width, height and maximal order type of Pf(X) cannot be expressed as a function of the invariants of X, and we provide tight upper and lower bounds for the three invariants. The article also identifies an algebra of well-behaved wqos, that include finitary powersets as well as other more classical constructions, and for which the ordinal invariants can be computed compositionnally. This relies on a new ordinal invariant called the approximated maximal order type.}
}
@unpublished{talk:zpoly:LOP23d,
location = {{LIS}},
shortlocation={the MOVE seminar of LIS},
title = {Z-Polyregular functions},
type = {Slides},
abstract = {Regular languages over finite words are defined equivalently in terms of restrictions of Turing Machines (finite deterministic automata, and the numerous equivalent automata models that are equi-expressive in this context), syntactic presentations (regular expressions), algebraic descriptions (recognisability by finite monoids), and logical specifications (via sentences in monadic second order logic). In this talk, we propose a generalisation of regular languages, i.e. functions from Σ* to Booleans, to functions from Σ* to integers, which we call Z-polyregular functions. This class shares many similarities with regular languages, both in terms of definitions, and in terms of decidability properties. We identify Z-polyregular functions as a subclass of other existing computational models, each time with appealing characterisations. Our main result is that one can decide whether Z-polyregular functions are star-free (aperiodic), whose proof relies on two beautiful ingredients: the construction of a residual transducer, and a semantic characterisation of aperiodicity for functions that is based on multivariate polynomials.
This is a joint work with Gaëtan Douéneau-Tabot and Thomas Colcombet.},
howpublished = {Slides},
note = {{MOVE} Seminar},
author = {Lopez, Aliaume},
date = {2023-12-07},
year = {2023},
langid = {english},
slides={/ressources/publications/Talks%2000/2023-MOVE-presentation.pdf},
}
@unpublished{talk:preservation:LOP23c,
location = {{LIRMM}},
shortlocation={the BOREAL seminar of LIRMM},
title = {Compositional Techniques for Preservation Theorems over Classes of
Finite Structures},
type = {Slides},
abstract = {Preservation theorems connect syntactic fragments of
first-order logic to corresponding "semantic" properties. For instance, the
fragment of unions of conjunctive queries is characterized as the fragment
of (first-order) queries that are "preserved under homomorphisms", that is,
if A is satisfies the query, and there is a homomorphism from A to B, then
B also satisfies the query: this is known as the Homomorphism Presrevation
Theorem. As an example of application of such theorems, the homomorphism
preservation theorem has been used to characterize the termination of the
"Core Chase Algorithm" by Deutsch, Nash and Remmel in 2008. Preservation
theorems date back to the 1950s, but the classical proofs of these result
are done in the framing of Model Theory and rely heavily on the compactness
theorem of first order logic. When restricting our attention to classes of
finite structures (which model finite databases), the status of the
preservation theorems have been investigated in the past years, with
positive and negative results on different classes of finite structures,
often with carefully built ad-hoc proofs. The goal of this talk is to
recall the landscape of preservation theorems in the finite, and propose a
compositional approach to constructing classes of structures over which
preservation theorems can be guaranteed. },
slides={/ressources/publications/Talks%2000/2023-LIRMM-presentation.pdf},
url={https://info-web.lirmm.fr/collorg/6d7169a1-7fef-4683-89a1-31752e376a5e},
howpublished = {Slides},
note = {{BOREAL} Seminar},
author = {Lopez, Aliaume},
date = {2023-11-06},
year = {2023},
langid = {english},
}
@unpublished{talk:preservation:LOP23b,
location = {{MIMUW}},
shortlocation={the automata seminar of MIMUW},
title = {The Łos-Tarski theorem and locality},
type = {Slides},
abstract = {We consider first order sentences over a finite relational signature σ. Classical preservation theorems, dating back to the 1950s, state the correspondence between syntactic fragments of FO[σ], and semantic ones. The archetypal example of such preservation theorem is the Łoś–Tarski Theorem, that states the correspondence between the syntactic fragment of existential sentences, and the semantic fragment of sentences preserved under extensions. As its proof heavily relies on the compactness of first order logic, it is a priori unclear whether Łoś–Tarski Theorem relativizes to classes of finite structures. Tait has proven in 1959 that the theorem does not relativize to the class Fin[σ] of all finite structures, but it was proven by Atserias, Dawar, and Grohe that the Łoś–Tarski Theorem relativizes to hereditary classes of finite structures that have bounded degree, and are closed under disjoint unions.
In this talk, we provide a full characterization of classes of hereditary classes finite structures that are closed under disjoint unions for which the Łoś–Tarski Theorem relativizes. This result follows form the study of the existential-local fragment of first order logic, that corresponds to a positive variant of the Gaifman normal form, and is itself subject to a preservation theorem.},
howpublished = {Slides},
note = {{M2F} Seminar},
author = {Lopez, Aliaume},
date = {2023-10-18},
year = {2023},
langid = {english},
}
@inproceedings{polyregular:CDA23,
type={conf},
author = {Colcombet, Thomas and Douéneau-Tabot, Gaëtan and Lopez, Aliaume},
booktitle = {38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title = {$\mathbb{Z}$-polyregular functions},
year = {2023},
volume = {},
issn = {},
pages = {1-13},
abstract = {This paper studies a robust class of functions from finite words to integers that we call ℤ-polyregular functions. We show that it admits natural characterizations in terms of logics, ℤ-rational expressions, ℤ-rational series and transducers.We then study two subclass membership problems. First, we show that the asymptotic growth rate of a function is computable, and corresponds to the minimal number of variables required to represent it using logical formulas. Second, we show that first-order definability of ℤ-polyregular functions is decidable. To show the latter, we introduce an original notion of residual transducer, and provide a semantic characterization based on aperiodicity.},
keywords = {computer science;transducers;semantics},
doi = {10.1109/LICS56636.2023.10175685},
url = {https://doi.ieeecomputersociety.org/10.1109/LICS56636.2023.10175685},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {jun},
shortlocation={LICS'23},
langid={english},
arxiv={2207.07450},
video={/ressources/publications/LICS%202023/lics-2023-pres.mp4},
pdf={/ressources/publications/LICS%202023/lics-2023-paper.pdf},
slides={/ressources/publications/LICS%202023/lics-2023-pres.pdf},
}
@inproceedings{topology:LOP23,
author={Lopez, Aliaume},
editor={Kupferman, Orna and Sobocinski, Pawel},
title={Fixed Points and Noetherian Topologies},
booktitle={Foundations of Software Science and Computation Structures},
year={2023},
publisher={Springer Nature Switzerland},
pages={456--476},
isbn={978-3-031-30828-4},
volume={13992},
abstract={Noetherian spaces are a generalisation of well-quasi-orderings to
topologies, that can be used to prove termination of programs.
They find applications in the verification of transition systems,
some of which are better described using topology. The goal of
this paper is to allow the systematic description of computations
using inductively defined datatypes via Noetherian spaces. This is
achieved through a fixed point theorem based on a topological
minimal bad sequence argument.},
isbn={978-3-031-30829-1},
type={conf},
langid={english},
shortlocation={FoSSACS'23},
doi={10.1007/978-3-031-30829-1_22},
url={https://link.springer.com/chapter/10.1007/978-3-031-30829-1_22},
pdf={/ressources/publications/FOSSACS%202023/fossacs-2023-paper.pdf},
arxiv = {2207.07614},
slides={/ressources/publications/FOSSACS%202023/fossacs-2023-slides.pdf},
}
@unpublished{talk:preservation:LOP23,
location = {{LaBRI}},
shortlocation={the M2F seminar of LaBRI},
title = {Preservation theorems and locality of first order logic},
slides = {/ressources/publications/Talks%2000/2023-BDX-presentation.pdf},
type = {Slides},
abstract = {In this talk, we will investigate the tight connection between
the locality properties of first-order logic, and the
relativisation (or lack thereof) of the Łós-Tarski Theorem to
classes of structures. Starting with a gentle introduction to
preservation theorems, we will then focus on two particular
classes of sentences: existential formulas, and existential
local formulas. We prove that existential local sentences are
exactly those that can be rewritten in a positive variant of the
Gaifman normal form, and can be characterized semantically as
sentences that are preserved under local elementary embeddings.
As expected, this semantic characterization fails in the finite.
Quite surprisingly though, we can leverage this class of
sentences to prove the following locality property for classes
of finite structures: the Łós-Tarski Theorem relativises to a
class C of finite structures if and only if the Łós-Tarski
Theorem locally relativises to the class C, provided that the
class C is hereditary and closed under disjoint unions. As a
consequence of this result, we not only obtain new proofs of
relativisation of Łós-Tarski Theorem, but also provide new
classes where this relativisation holds.},
howpublished = {Slides},
note = {{M2F} Seminar},
author = {Lopez, Aliaume},
date = {2023-03-02},
year = {2023},
langid = {english},
}
@unpublished{topology:GHL22,
abstract = {We show that the spaces of transfinite words, namely ordinal-indexed words, over a Noetherian space, is also Noetherian, under a natural topology which we call the regular subword topology. We characterize its sobrification and its specialization ordering, and we give an upper bound on its dimension and on its stature.},
shortlocation={Colloquium Mathematicum},
title = {Infinitary Noetherian Constructions II. Transfinite Words and the Regular Subword Topology},
author = {Goubault-Larrecq, Jean and Halfon, Simon and Lopez, Aliaume},
date = {2022},
year = {2022},
arxiv={2202.05047},
pages={26},
langid = {english},
type={preprint},
}
@unpublished{talk:topology:LOP22,
location = {{ENS} Paris-Saclay},
shortlocation={the BRAVAS team seminar},
title = {Generic Noetherian Theorems - Defining Noetherian Topologies Through Iterations},
slides = {/ressources/publications/Talks%2000/2022-BRAVAS-presentation.pdf},
type = {Slides},
abstract = {The goal of this talk is to provide a canonical
way to construct Noetherian topologies as least fixed points.
This is done by
proving a least fixed point theorem, that
extends the work of Hasegawa on well-quasi-orderings
to Noetherian spaces. This extension allows us to justify
previously introduced Noetherian topologies, and
construct new Noetherian spaces. Finally,
note that we can apply our result to spaces
that are not inductively defined, provided that the
topology/ordering is inductively defined, which
is a limitation in Hasegawa's approach.
},
howpublished = {Slides},
note = {{BRAVAS}},
author = {Lopez, Aliaume},
date = {2022-04-11},
year = {2022},
langid = {english},
}
@unpublished{talk:preservation:LOP22,
location = {Lille {DAAL}, Lille, 2022},
title = {Locality and Preservation Theorems},
slides = {/ressources/publications/Talks%2000/2022-DAAL-presentation.pdf},
shortlocation={the GT DAAL},
type = {Slides},
howpublished = {Slides},
note = {{DAAL}},
author = {Lopez, Aliaume},
date = {2022-03-28},
year={2022},
langid = {english},
abstract = {This talk is a brief introduction to the relationship
between locality based techniques and preservation theorems
in finite model theory.},
ref={preservation:LOP22}
}
@unpublished{talk:admin:LOP22,
location = {{ENS} Paris-Saclay},
shortlocation={the ENS Paris-Saclay student seminar},
title = {Rejoindre l'administration publique avec un doctorat - Comment et
pourquoi ?},
slides = {/ressources/publications/Talks%2000/2022-DPTINFO-ENS-presentation.pdf},
type = {Slides},
abstract = {Les présentations de l'ENS décrivent souvent une formation « par la recherche, pour la recherche », selon la formule consacrée. Ainsi, une grande majorité des normaliens commencent leur parcours professionnel par un doctorat (c'est le cas d'environ 80% des élèves du département informatique). Néanmoins, seuls 50% des docteurs diplômés en France rejoignent finalement les métiers de la recherche et de l'enseignement publics. Cela contraste avec les débouchés usuellement présentés aux normaliens, centrés sur les postes permanents de maîtres de conférences, chargés de recherche ou professeurs agrégés. Parmi les docteurs, on compte également 30% de débouchés dans le secteur privé ou l'entreprenariat. Notre objectif est de discuter des 20% restants, qui choisissent de rejoindre le secteur public hors du monde académique, autrement dit les administrations publiques. Les voies d'accès de la fonction publique aux jeunes docteurs sont nombreuses,qu'il s'agisse de recrutements sur concours ou en tant que contractuels (CDD ou CDI), à des postes de managers ou d'experts techniques. L'objectif de ce séminaire est de présenter les postes et les recrutements dans l'administration, ainsi que quelques parcours de normaliens l'ayant rejointe.},
howpublished = {Slides},
note = {Séminaire du Département Informatique},
author = {Lopez, Aliaume and Douéneau-Tabot, Gaëtan},
date = {2022-11-29},
year = {2022},
langid = {french},
}
@inproceedings{preservation:LOP22,
location = {New York, {NY}, {USA}},
shortlocation={LICS'22},
title = {When Locality Meets Preservation},
isbn = {978-1-4503-9351-5},
url = {https://doi.org/10.1145/3531130.3532498},
doi = {10.1145/3531130.3532498},
series = {{LICS} '22},
abstract = {This paper investigates the expressiveness of a fragment of first-order sentences in Gaifman normal form, namely the positive Boolean combinations of basic local sentences. We show that they match exactly the first-order sentences preserved under local elementary embeddings, thus providing a new general preservation theorem and extending the Łós-Tarski Theorem. This full preservation result fails as usual in the finite, and we show furthermore that the naturally related decision problems are undecidable. In the more restricted case of preservation under extensions, it nevertheless yields new well-behaved classes of finite structures: we show that preservation under extensions holds if and only if it holds locally.},
pages = {1--14},
booktitle = {37th Annual {ACM}/{IEEE} Symposium on Logic in Computer Science},
publisher = {Association for Computing Machinery},
author = {Lopez, Aliaume},
urldate = {2022-10-17},
year = {2022},
date = {2022-08-02},
langid={english},
type={conf},
keywords = {Finite Model Theory., Gaifman normal form, Locality, Preservation theorem, Tree depth, Undecidability, Well quasi ordering},
arxiv={2204.02108},
slides={/ressources/publications/LICS%202022/lics-2022-slides.pdf},
pdf={/ressources/publications/LICS%202022/lics-2022-paper.pdf},
}
@unpublished{talk:effects:LOP21,
location = {{IRIF}},
shortlocation={the PPS Seminar at IRIF},
title = {Basic Operational Preorders for Algebraic Effects - With a pinch of non-determinism and probabilities},
slides = {https://www.irif.fr/~alopez/ressources/publications/Talks%2000/2021-IRIF-GDT-PPS.pdf},
type = {Slides},
abstract = {The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
},
howpublished = {Slides},
note = {{PPS} Seminar},
author = {Lopez, Aliaume},
date = {2021-12-17},
year = {2021},
langid = {english},
}
@unpublished{talk:preservation:LOP21,
title = {Preservation theorems - At the crossroads of topology and logics},
slides = {https://www.irif.fr/~alopez/ressources/publications/Talks%2000/2021-ASV-presentation.pdf},
type = {Slides},
howpublished = {Slides},
shortlocation={the ASV Seminar of IRIF},
note = {{ASV} Seminar},
author = {Lopez, Aliaume},
date = {2021-11-19},
year={2021},
langid = {english},
abstract = {In this talk, we introduce a family of topological spaces that
captures the existence of preservation theorems. The structure
of those spaces allows us to study the relativisation of
preservation theorems under suitable definitions of surjective
morphisms, subclasses, sums, products, topological closures, and
projective limits. Throughout the talk,
we also integrate already known results
into this new framework and show how it captures
the essence of their proofs.},
ref={preservation:LOP21},
}
@report{report:admin:DLP21,
author = {Douéneau-Tabot, Gaëtan and Lopez, Aliaume and Prosperi, Laurent},
title = {Recrutement et emploi des docteurs dans les administrations
publiques.},
year={2021},
date = {2023-10},
type={Report},
shortlocation={IDeA},
langid={french},
publisher={Initiative Docteurs et Administrations},
url = {https://docteurs-administrations.fr/media/productions/IDeA_docteurs-administrations.pdf},
abstract={Plus de 14 000 docteurs sont diplômés chaque année en France.
À l'issue de leur thèse, ils s'intègrent au sein de trois grands
secteurs : le monde académique (recherche et enseignement), le
privé, ou le secteur public hors académique. Si l'insertion
professionnelle dans l’académique ou le privé est régulièrement
mentionnée, il semble qu’aucun rapport n’étudie l'emploi et le
recrutement dans le public hors académique. Pourtant, l'Enquête
emploi en continu (EEC) de l'INSEE estime à plus de 18 000 le
nombre de docteurs dans ce secteur (hors doctorats de santé).
L'objectif de ce rapport est donc de dresser un état des lieux de
l'insertion professionnelle des docteurs au sein des
administrations publiques. Il constitue une première réflexion sur
un sujet peu étudié et ne prétend pas à l'exhaustivité.}
}
@inproceedings{preservation:LOP21,
abstract = {In this paper, we introduce a family of topological spaces that captures the existence of preservation theorems. The structure of those spaces allows us to study the relativisation of preservation theorems under suitable definitions of surjective morphisms, subclasses, sums, products, topological closures, and projective limits. Throughout the paper, we also integrate already known results into this new framework and show how it captures the essence of their proofs. },
type={conf},
shortlocation={CSL'21},
title = {Preservation Theorems Through the Lens of Topology},
volume = {183},
doi = {10.4230/LIPIcs.CSL.2021.32},
series = {Leibniz International Proceedings in Informatics},
pages = {32:1--32:17},
booktitle = {30th {EACSL} Annual Conference on Computer Science Logic ({CSL} 2021)},
author = {Lopez, Aliaume},
date = {2021},
year = {2021},
keywords = {Noetherian space, Pre-spectral space, Preservation theorem, Spectral space},
annotation = {Keywords: Preservation theorem, Pre-spectral space, Noetherian space, Spectral space},
arxiv={2007.07879},
slides={/ressources/publications/CSL%202021/csl-2021-slides.pdf},
pdf={/ressources/publications/CSL%202021/csl-2021-paper.pdf},
}
@online{blog:topology:GL20,
abstract = {
Given a quasi-ordered set $(X, ≤)$, the set of finite words over $X$
is built as $X^* = ⋃_{0 \leq k < \infty} X_k$.
This set can be equipped with many different quasi-orders, but it appears that
often the right notion is the one relying on subwords, that is, a word $w$
is smaller than a word $w'$
if there exists a map $h\colon |w|\to|w'|$ such that
$\forall 1 \leq k \leq |w|, w_k \leq w_{h(k)}'$.
This order is called the subword ordering. This blog posts explores how
one can recover this ordering by looking at functions that decompose words
($\operatorname{split} \colon X^* \to \mathcal{P}(X^* \times X^*)$),
rather than considering their inductive constructors
($\operatorname{concat} \colon X^* \times X^* \to X^*$).
},
shortlocation = {Jean Goubault-Larrecq's blog},
title = {On the word topology, and beyond},
url = {https://projects.lsv.ens-cachan.fr/topology/?page_id=2735},
titleaddon = {Non-Hausdorff Topology and Domain Theory},
author = {Goubault-Larrecq, Jean and Lopez, Aliaume},
date = {2020},
year = {2020},
langid = {english},
type={blog},
}
@inproceedings{effects:LOP18,
location = {Dagstuhl, Germany},
title = {Basic Operational Preorders for Algebraic Effects in General, and for Combined Probability and Nondeterminism in Particular},
volume = {119},
abstract={
The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
},
isbn = {978-3-95977-088-0},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9696},
doi = {10.4230/LIPIcs.CSL.2018.29},
series = {Leibniz International Proceedings in Informatics ({LIPIcs})},
pages = {29:1--29:17},
booktitle = {27th {EACSL} Annual Conference on Computer Science Logic ({CSL} 2018)},
publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
author = {Lopez, Aliaume and Simpson, Alex},
editor = {Ghica, Dan and Jung, Achim},
urldate = {2022-10-17},
year = {2018},
date = {2018-09-07},
keywords = {algebraic effects, contextual equivalence, domain theory, Markov decision process, nondeterminism, operational semantics, probabilistic choice},
shortlocation={CSL'18},
type={conf},
slides={/ressources/publications/CSL%202018/csl-2018-slides.pdf},
pdf={/ressources/publications/CSL%202018/csl-2018-paper.pdf},
}
@report{report:effects:LOP17,
location = {{ENS} Cachan},
shortlocation={ENS Cachan},
title = {Generic Operational Metatheory},
url = {https://www.irif.fr/~alopez/ressources/publications/M1%202017/rapport.pdf},
pdf = {/ressources/publications/M1%202017/presentation.pdf},
slides = {/ressources/publications/M1%202017/rapport.pdf},
type = {Rapport de Stage},
abstract = {
The "generic operational metatheory" of Johann, Simpson and Voigtländer (LiCS 2010) defines contextual equivalence, in the presence of algebraic effects, in terms of a basic operational preorder on ground-type effect trees. We propose three general approaches to specifying such preorders: (i) operational (ii) denotational, and (iii) axiomatic; coinciding with the three major styles of program semantics. We illustrate these via a nontrivial case study: the combination of probabilistic choice with nondeterminism, for which we show that natural instantiations of the three specification methods (operational in terms of Markov decision processes, denotational using a powerdomain, and axiomatic) all determine the same canonical preorder. We do this in the case of both angelic and demonic nondeterminism.
},
howpublished = {Slides},
note = {Soutenance de Stage},
author = {Lopez, Aliaume},
date = {2017-08-30},
year = {2017},
pages = {28},
langid = {english},
abstract = {The goal of this internship was to give a systematic study of contextual equivalence in the presence of algebraic effects in a uniform, compact and syntactic way, in the continuation of preexisting work. To reach this objective, we extended a call-by-value PCF with a signature of algebraic effects, and gave an abstract equality between the contextual equivalence for this language and a usable logical relation, independently of the signature itself. Generic meta theorems were then proven using this abstract equivalence. To justify the usefulness of this approach, a direct link with denotational semantics and the work of Plotkin and Power was developed, and signature of mixed non-determinism and probabilities was studied in-depth.},
}
@inproceedings{ghica_diagrammatic_2017,
location = {Dagstuhl, Germany},
title = {Diagrammatic Semantics for Digital Circuits},
volume = {82},
isbn = {978-3-95977-045-3},
url = {http://drops.dagstuhl.de/opus/volltexte/2017/7671},
doi = {10.4230/LIPIcs.CSL.2017.24},
series = {Leibniz International Proceedings in Informatics ({LIPIcs})},
pages = {24:1--24:16},
booktitle = {26th {EACSL} Annual Conference on Computer Science Logic ({CSL} 2017)},
shortlocation={CSL'17},
type={conf},
publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
author = {Ghica, Dan R. and Jung, Achim and Lopez, Aliaume},
editor = {Goranko, Valentin and Dam, Mads},
urldate = {2022-10-17},
abstract = {We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications. },
date = {2017},
year = {2017},
arxiv={1703.10247},
keywords = {operational semantics, digital circuits, monoidal categories, rewriting, string diagrams},
file = {Full Text PDF:/home/alopez/Zotero/storage/BSIAKELT/Ghica et al. - 2017 - Diagrammatic Semantics for Digital Circuits.pdf:application/pdf;Snapshot:/home/alopez/Zotero/storage/G8IC5CIT/7671.html:text/html},
}
@inproceedings{ghica_structural_2017,
title = {A structural and nominal syntax for diagrams},
abstract = {The correspondence between monoidal categories and graphical languages of diagrams has been studied extensively, leading to applications in quantum computing and communication, systems theory, circuit design and more. From the categorical perspective, diagrams can be specified using (name-free) combinators which enjoy elegant equational properties. However, conventional notations for diagrammatic structures, such as hardware description languages (VHDL, Verilog) or graph languages (Dot), use a different style, which is flat, relational, and reliant on extensive use of names (labels). Such languages are not known to enjoy nice syntactic equational properties. However, since they make it relatively easy to specify (and modify) arbitrary diagrammatic structures they are more popular than the combinator style. In this paper we show how the two approaches to diagram syntax can be reconciled and unified in a way that does not change the semantics and the existing equational theory. Additionally, we give sound and complete equational theories for the combined syntax.},
volume = {266},
url = {https://doi.org/10.4204/EPTCS.266.4},
doi = {10.4204/EPTCS.266.4},
shortlocation={QPL},
series = {{EPTCS}},
year={2017},
type={conf},
langid={english},
arxiv={1702.01695v2},
pages = {71--83},
booktitle = {Proceedings 14th International Conference on Quantum Physics and Logic, {QPL} 2017, Nijmegen, The Netherlands, 3-7 July 2017},
author = {Ghica, Dan R. and Lopez, Aliaume},
editor = {Coecke, Bob and Kissinger, Aleks},
date = {2017},
}
@unpublished{lopez_syntaxe_2016,
type={report},
shortlocation={ENS Cachan},
title = {Une syntaxe améliorée pour la description de circuits digitaux},
abstract = {$\emptyset$},
pages={24},
institution = {{ENS} Cachan},
url = {https://www.irif.fr/~alopez/ressources/publications/L3%202016/presentation.pdf},
slides = {/ressources/publications/L3%202016/presentation.pdf},
pdf = {/ressources/publications/L3%202016/rapport.pdf},
type = {Rapport de Stage},
howpublished = {Rapport de Stage},
author = {Lopez, Aliaume},
date = {2016},
langid = {french},
url = {https://www.irif.fr/~alopez/ressources/publications/L3%202016/synth.pdf},
}