Refs for ONS

biblio-eigen.bib

@@ -71,3 +71,24 @@
 	biburl    = {https://dblp.org/rec/bib/conf/lata/2016},
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
+
+@inproceedings{MoermanS0KS17,
+	author    = {Joshua Moerman and
+	             Matteo Sammartino and
+	             Alexandra Silva and
+	             Bartek Klin and
+	             Michal Szynwelski},
+	editor    = {Giuseppe Castagna and
+	             Andrew D. Gordon},
+	title     = {Learning nominal automata},
+	booktitle = {Proceedings of the 44th {ACM} {SIGPLAN} Symposium on Principles of
+	             Programming Languages, {POPL} 2017, Paris, France, January 18-20,
+	             2017},
+	pages     = {613--625},
+	publisher = {{ACM}},
+	year      = {2017},
+	url       = {http://dl.acm.org/citation.cfm?id=3009879},
+	timestamp = {Wed, 28 Dec 2016 13:22:29 +0100},
+	biburl    = {https://dblp.org/rec/bib/conf/popl/MoermanS0KS17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}

biblio.bib

@@ -191,6 +191,26 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/cav/DAntoniV17,
+	author    = {Loris D'Antoni and
+	             Margus Veanes},
+	editor    = {Rupak Majumdar and
+	             Viktor Kuncak},
+	title     = {The Power of Symbolic Automata and Transducers},
+	booktitle = {Computer Aided Verification - 29th International Conference, {CAV}
+	             2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {I}},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {10426},
+	pages     = {47--67},
+	publisher = {Springer},
+	year      = {2017},
+	url       = {https://doi.org/10.1007/978-3-319-63387-9\_3},
+	doi       = {10.1007/978-3-319-63387-9\_3},
+	timestamp = {Fri, 14 Jul 2017 12:55:54 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/cav/DAntoniV17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/icwsm/BastianHJ09,
 	author    = {Mathieu Bastian and
 	             Sebastien Heymann and
@@ -703,6 +723,23 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{CianciaKM10,
+	author    = {Vincenzo Ciancia and
+	             Alexander Kurz and
+	             Ugo Montanari},
+	title     = {Families of Symmetries as Efficient Models of Resource Binding},
+	journal   = {Electr. Notes Theor. Comput. Sci.},
+	volume    = {264},
+	number    = {2},
+	pages     = {63--81},
+	year      = {2010},
+	url       = {https://doi.org/10.1016/j.entcs.2010.07.014},
+	doi       = {10.1016/j.entcs.2010.07.014},
+	timestamp = {Mon, 05 Jun 2017 20:49:18 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/entcs/CianciaKM10},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/iandc/CianciaM10,
 	author    = {Vincenzo Ciancia and
 	             Ugo Montanari},
@@ -774,6 +811,27 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DrewsD17,
+	author    = {Samuel Drews and
+	             Loris D'Antoni},
+	editor    = {Axel Legay and
+	             Tiziana Margaria},
+	title     = {Learning Symbolic Automata},
+	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
+	             - 23rd International Conference, {TACAS} 2017, Held as Part of the
+	             European Joint Conferences on Theory and Practice of Software, {ETAPS}
+	             2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part {I}},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {10205},
+	pages     = {173--189},
+	year      = {2017},
+	url       = {https://doi.org/10.1007/978-3-662-54577-5\_10},
+	doi       = {10.1007/978-3-662-54577-5\_10},
+	timestamp = {Wed, 24 May 2017 08:28:32 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/tacas/DrewsD17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/infsof/DorofeevaEMCY10,
 	author    = {Rita Dorofeeva and
 	             Khaled El{-}Fakih and
@@ -827,6 +885,24 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{FerrariMT05,
+	author    = {Gian Luigi Ferrari and
+	             Ugo Montanari and
+	             Emilio Tuosto},
+	title     = {Coalgebraic minimization of HD-automata for the Pi-calculus using
+	             polymorphic types},
+	journal   = {Theor. Comput. Sci.},
+	volume    = {331},
+	number    = {2-3},
+	pages     = {325--365},
+	year      = {2005},
+	url       = {https://doi.org/10.1016/j.tcs.2004.09.021},
+	doi       = {10.1016/j.tcs.2004.09.021},
+	timestamp = {Thu, 08 Jun 2017 09:02:47 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/tcs/FerrariMT05},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/fmics/Fiterau-BrosteanJV14,
 	author    = {Paul Fiterau{-}Brostean and
 	             Ramon Janssen and
@@ -902,6 +978,22 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{GabbayP02,
+	author    = {Murdoch Gabbay and
+	             Andrew M. Pitts},
+	title     = {A New Approach to Abstract Syntax with Variable Binding},
+	journal   = {Formal Asp. Comput.},
+	volume    = {13},
+	number    = {3-5},
+	pages     = {341--363},
+	year      = {2002},
+	url       = {https://doi.org/10.1007/s001650200016},
+	doi       = {10.1007/s001650200016},
+	timestamp = {Tue, 06 Jun 2017 22:21:37 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/fac/GabbayP02},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/tacas/GaravelLMS11,
 	author    = {Hubert Garavel and
 	             Fr{\'{e}}d{\'{e}}ric Lang and
@@ -968,6 +1060,21 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{DBLP:journals/corr/GrigoreT16,
+	author    = {Radu Grigore and
+	             Nikos Tzevelekos},
+	title     = {History-Register Automata},
+	journal   = {Logical Methods in Computer Science},
+	volume    = {12},
+	number    = {1},
+	year      = {2016},
+	url       = {https://doi.org/10.2168/LMCS-12(1:7)2016},
+	doi       = {10.2168/LMCS-12(1:7)2016},
+	timestamp = {Mon, 13 Aug 2018 16:46:38 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1209-0680},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/pts/GrozLPS08,
 	author    = {Roland Groz and
 	             Keqin Li and
@@ -1578,6 +1685,31 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{MalerM17,
+	author    = {Oded Maler and
+	             Irini-Eleftheria Mens},
+	editor    = {Luca Aceto and
+	             Giorgio Bacci and
+	             Giovanni Bacci and
+	             Anna Ing{\'{o}}lfsd{\'{o}}ttir and
+	             Axel Legay and
+	             Radu Mardare},
+	title     = {A Generic Algorithm for Learning Symbolic Automata from Membership
+	             Queries},
+	booktitle = {Models, Algorithms, Logics and Tools - Essays Dedicated to Kim Guldstrand
+	             Larsen on the Occasion of His 60th Birthday},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {10460},
+	pages     = {146--169},
+	publisher = {Springer},
+	year      = {2017},
+	url       = {https://doi.org/10.1007/978-3-319-63121-9\_8},
+	doi       = {10.1007/978-3-319-63121-9\_8},
+	timestamp = {Tue, 22 Aug 2017 08:17:15 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/birthday/MalerM17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @phdthesis{DBLP:phd/hal/Mens17,
 	author    = {Irini-Eleftheria Mens},
 	title     = {Learning regular languages over large alphabets},
@@ -1615,6 +1747,21 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{MontanariP97,
+	author    = {Ugo Montanari and
+	             Marco Pistore},
+	title     = {An Introduction to History Dependent Automata},
+	journal   = {Electr. Notes Theor. Comput. Sci.},
+	volume    = {10},
+	pages     = {170--188},
+	year      = {1997},
+	url       = {https://doi.org/10.1016/S1571-0661(05)80696-6},
+	doi       = {10.1016/S1571-0661(05)80696-6},
+	timestamp = {Sun, 28 May 2017 13:22:55 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/entcs/MontanariP97},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/tcs/MontanariS14,
 	author    = {Ugo Montanari and
 	             Matteo Sammartino},
@@ -1700,6 +1847,23 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{MurawskiRT15,
+	author    = {Andrzej S. Murawski and
+	             Steven J. Ramsay and
+	             Nikos Tzevelekos},
+	title     = {Bisimilarity in Fresh-Register Automata},
+	booktitle = {30th Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
+	             2015, Kyoto, Japan, July 6-10, 2015},
+	pages     = {156--167},
+	publisher = {{IEEE} Computer Society},
+	year      = {2015},
+	url       = {https://doi.org/10.1109/LICS.2015.24},
+	doi       = {10.1109/LICS.2015.24},
+	timestamp = {Thu, 25 May 2017 00:42:41 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/lics/MurawskiRT15},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @phdthesis{DBLP:phd/de/Niese2003,
 	author    = {Oliver Niese},
 	title     = {An integrated approach to testing complex systems},
@@ -1771,6 +1935,21 @@
 	year={2013}
 }
 
+@article{Pitts16,
+	author    = {Andrew M. Pitts},
+	title     = {Nominal techniques},
+	journal   = {{SIGLOG} News},
+	volume    = {3},
+	number    = {1},
+	pages     = {57--72},
+	year      = {2016},
+	url       = {http://doi.acm.org/10.1145/2893582.2893594},
+	doi       = {10.1145/2893582.2893594},
+	timestamp = {Mon, 18 Jul 2016 11:41:35 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/siglog/Pitts16},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @thesis{Ploeger05,
 	title     = {Analysis of concurrent state machines in embedded copier software},
 	author    = {Bas Ploeger},
@@ -1877,6 +2056,25 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{Segoufin06,
+	author    = {Luc Segoufin},
+	editor    = {Zolt{\'{a}}n {\'{E}}sik},
+	title     = {Automata and Logics for Words and Trees over an Infinite Alphabet},
+	booktitle = {Computer Science Logic, 20th International Workshop, {CSL} 2006, 15th
+	             Annual Conference of the EACSL, Szeged, Hungary, September 25-29,
+	             2006, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {4207},
+	pages     = {41--57},
+	publisher = {Springer},
+	year      = {2006},
+	url       = {https://doi.org/10.1007/11874683\_3},
+	doi       = {10.1007/11874683\_3},
+	timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/csl/Segoufin06},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @book{DBLP:books/daglib/SelicGW94,
 	author    = {Bran Selic and
 	             Garth Gullekson and
@@ -1891,6 +2089,18 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@techreport{ShinwellP05,
+	title     = {Fresh objective {Caml} user manual},
+	author    = {Mark R. Shinwell and
+	             Andrew M. Pitts},
+	year      = {2005},
+	month     = {feb},
+	institution = {University of Cambridge, Computer Laboratory},
+	url       = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-621.pdf},
+	number    = {UCAM-CL-TR-621},
+	issn      = {1476-2986}
+}
+
 @article{DBLP:journals/entcs/Shinwell06,
 	author    = {Mark R. Shinwell},
 	title     = {Fresh {O'Caml}: Nominal Abstract Syntax for the Masses},
@@ -2012,6 +2222,40 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{UrbanT05,
+	author    = {Christian Urban and
+	             Christine Tasson},
+	editor    = {Robert Nieuwenhuis},
+	title     = {Nominal Techniques in {Isabelle}/{HOL}},
+	booktitle = {Automated Deduction - CADE-20, 20th International Conference on Automated
+	             Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {3632},
+	pages     = {38--53},
+	publisher = {Springer},
+	year      = {2005},
+	url       = {https://doi.org/10.1007/11532231\_4},
+	doi       = {10.1007/11532231\_4},
+	timestamp = {Tue, 30 May 2017 16:36:52 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/cade/UrbanT05},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{Vaandrager17,
+	author    = {Frits W. Vaandrager},
+	title     = {Model learning},
+	journal   = {Commun. {ACM}},
+	volume    = {60},
+	number    = {2},
+	pages     = {86--95},
+	year      = {2017},
+	url       = {http://doi.acm.org/10.1145/2967606},
+	doi       = {10.1145/2967606},
+	timestamp = {Mon, 06 Feb 2017 15:05:06 +0100},
+	biburl    = {https://dblp.org/rec/bib/journals/cacm/Vaandrager17},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{ValmariL08,
 	author    = {Antti Valmari and
 	             Petri Lehtinen},

content/ordered-nominal-sets.tex

@@ -23,21 +23,21 @@ In both cases, \ONS{} is competitive compared to existing implementations and ou
   [title={Introduction}]
 
 Automata over infinite alphabets are natural models for programs with unbounded data domains.
-Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[bojanczyk2014automata, DAntoniV17, DBLP:journals/corr/abs-1209-0680, KaminskiF94, MontanariP97, Segoufin06] and references therein).
+Such automata, often formalised as \emph{register automata}, are applied in modelling and analysis of communication protocols, hardware, and software systems (see \citenp[DBLP:journals/corr/BojanczykKL14, DBLP:conf/cav/DAntoniV17, DBLP:journals/corr/GrigoreT16, DBLP:journals/tcs/KaminskiF94, MontanariP97, Segoufin06] and references therein).
 Typical infinite alphabets include sequence numbers, timestamps, and identifiers.
 This means one can model data flow in such automata beside the basic control flow provided by ordinary automata.
-Recently, it has been shown in a series of papers that such models are amenable to learning \citep[AartsFKV15, BolligHLM13, CasselHJS16, DrewsD17, moerman2017learning, Vaandrager17] with the verification of (closed source) TCP implementations by \citet[Fiterau-Brostean16] as a prominent example.
+Recently, it has been shown in a series of papers that such models are amenable to learning \citep[DBLP:conf/ictac/AartsFKV15, DBLP:conf/dlt/BolligHLM13, DBLP:journals/fac/CasselHJS16, DrewsD17, MoermanS0KS17, Vaandrager17] with the verification of (closed source) TCP implementations by \citet[DBLP:conf/cav/Fiterau-Brostean16] as a prominent example.
 
-A foundational approach to infinite alphabets is provided by the notion of \emph{nominal set}, originally introduced in computer science as an elegant formalism for name binding \citep[GabbayP02, pitts2016nominal].
+A foundational approach to infinite alphabets is provided by the notion of \emph{nominal set}, originally introduced in computer science as an elegant formalism for name binding \citep[GabbayP02, Pitts16].
-Nominal sets have been used in a variety of applications in semantics, computation, and concurrency theory (see \citenp[pitts2013nominal] for an overview). 
+Nominal sets have been used in a variety of applications in semantics, computation, and concurrency theory (see \citenp[Pitts13] for an overview). 
-\citet[bojanczyk2014automata] introduce \emph{nominal automata}, which allow one to model languages over infinite alphabets with different symmetries.
+\citet[DBLP:journals/corr/BojanczykKL14] introduce \emph{nominal automata}, which allow one to model languages over infinite alphabets with different symmetries.
 Their results are parametric in the structure of the data values.
 Important examples of data domains are ordered data values (e.g., timestamps) and data values that can only be compared for equality (e.g., identifiers).
-In both data domains, nominal automata and register automata are equally expressive \citep[bojanczyk2014automata].
+In both data domains, nominal automata and register automata are equally expressive.
 
 Important for applications of nominal sets and automata are implementations.
 A couple of tools exist to compute with nominal sets.
-Notably, \NLambda{} \citep[EPTCS207.3] and \LOIS{} \citep[kopczynski1716, kopczynski2017] provide a general purpose programming language to manipulate infinite sets.
+Notably, \NLambda{} \citep[DBLP:journals/corr/KlinS16] and \LOIS{} \citep[DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17] provide a general purpose programming language to manipulate infinite sets.
 \footnote{Other implementations of nominal techniques that are less directly related to our setting (Mihda, Fresh OCaml, and Nominal Isabelle) are discussed in \in{Section}[sec:related].}
 Both tools are based on SMT solvers and use logical formulas to represent the infinite sets.
 These implementations are very flexible, and the SMT solver does most of the heavy lifting, which makes the implementations themselves relatively straightforward.
@@ -46,8 +46,8 @@ Since the formulas used to describe sets tend to grow as more calculations are d
 
 In the current paper, we use a direct representation, based on symmetries and orbits, to represent nominal sets.
 We focus on the \emph{total order symmetry}, where data values are rational numbers and can be compared for their order.
-Nominal automata over the total order symmetry are more expressive than automata over the equality symmetry (i.e., traditional register automata of \citenp[KaminskiF94]).
+Nominal automata over the total order symmetry are more expressive than automata over the equality symmetry (i.e., traditional register automata of \citenp[DBLP:journals/tcs/KaminskiF94]).
-A key insight is that the representation of nominal sets from \citet[bojanczyk2014automata] becomes rather simple in the total order symmetry; each orbit is presented solely by a natural number, intuitively representing the number of variables or registers.
+A key insight is that the representation of nominal sets from \citet[DBLP:journals/corr/BojanczykKL14] becomes rather simple in the total order symmetry; each orbit is presented solely by a natural number, intuitively representing the number of variables or registers.
 
 Our main contributions include the following.
 \startitemize
@@ -62,7 +62,7 @@ Using the representation theory, we are able to \emph{implement nominal sets in
 The library includes all the results from the representation theory (sets, products, and maps).
 \item
 We \emph{evaluate the performance} of \ONS{} and compare it to \NLambda{} and \LOIS{}, using two algorithms on nominal automata:
-minimisation \citep[BojanczykL12] and automata learning \citep[moerman2017learning].
+minimisation \citep[DBLP:conf/icalp/BojanczykL12] and automata learning \citep[MoermanS0KS17].
 We use randomly generated automata as well as concrete, logically structured models such as FIFO queues.
 For random automata, our methods are drastically faster than the other tools.
 On the other hand, \LOIS{} and \NLambda{} are faster in minimising the structured automata as they exploit their logical structure.
@@ -82,7 +82,7 @@ Related work is discussed in \in{Section}[sec:related], and future work in \in{S
    reference=sec:nomsets]
 
 Nominal sets are infinite sets that carry certain symmetries, allowing a finite representation in many interesting cases.
-We recall their formalisation in terms of group actions, following \citet[bojanczyk2014automata, pitts2013nominal], to which we refer for an extensive introduction.
+We recall their formalisation in terms of group actions, following \citet[DBLP:journals/corr/BojanczykKL14, Pitts13], to which we refer for an extensive introduction.
 
 
 \startsubsubsection
@@ -135,7 +135,7 @@ The existence of least supports is crucial for representing orbits.
 Unfortunately, even when elements have a finite support, in general they do not always have a least support.
 A data symmetry $(\mathcal{D}, G)$ is said to \emph{admit least supports} if every element of every nominal set 
 has a least support. Both the equality and the total order symmetry admit least supports.
-(See \citep[bojanczyk2014automata] for other (counter)examples of data symmetries admitting least supports.)
+(\citenp[DBLP:journals/corr/BojanczykKL14] give additional (counter)examples of data symmetries admitting least supports.)
 Having least supports is useful for a finite representation.
 
 Given a nominal set $X$, the size of the least support of an element $x \in X$ is denoted by $\dim(x)$, the \emph{dimension} of $x$.
@@ -150,7 +150,7 @@ For a single-orbit set $O$, observe that $\dim(O) = \dim(x)$ where $x$ is any el
    reference=subsec:nomorbit]
 
 We represent nominal sets as collections of single orbits. 
-The finite representation of single orbits is based on the theory of \citet[bojanczyk2014automata], which uses the technical notions of \emph{restriction} and \emph{extension}.
+The finite representation of single orbits is based on the theory of \citet[DBLP:journals/corr/BojanczykKL14], which uses the technical notions of \emph{restriction} and \emph{extension}.
 We only briefly report their definitions here.
 However, the reader can safely move to the concrete representation theory in \in{Section}[sec:total-order] with only a superficial understanding of \in{Theorem}[representation_tuple] below.
 
@@ -160,7 +160,7 @@ The \emph{extension} of a subgroup $S \le G|_C$ is defined as $\ext_G(S) = \{\pi
 For $C \subseteq \mathcal{D}$ and $S\le G|_C$, define $[C,S]^{ec} = \{\{sg \mid s \in \ext_G(S)\}\mid g\in G\}$, i.e., the set of right cosets of $\ext_G(S)$ in $G$.
 Then $[C,S]^{ec}$ is a single-orbit nominal set.
 
-Using the above, we can formulate the representation theory from \citet[bojanczyk2014automata] that we will use in the current paper.
+Using the above, we can formulate the representation theory from \citet[DBLP:journals/corr/BojanczykKL14] that we will use in the current paper.
 This gives a finite description for all single-orbit nominal sets $X$, namely a finite set $C$ together with some of its symmetries.
 
 \starttheorem[reference=representation_tuple]
@@ -168,7 +168,7 @@ Let $X$ be a single-orbit nominal set for a data symmetry $(\mathcal{D}, G)$ tha
 Then there exists a subgroup $S \le G|_C$ such that $X \cong [C,S]^{ec}$.
 \stoptheorem
 
-The proof by \citet[bojanczyk2014automata] uses a bit of category theory:
+The proof by \citet[DBLP:journals/corr/BojanczykKL14] uses a bit of category theory:
 it establishes an equivalence of categories between single-orbit sets and the pairs $(C, S)$.
 We will not use the language of category theory much in order to keep the paper self-contained.
 
@@ -417,8 +417,6 @@ The function \kw{nomset_product} then uses the enumeration of product strings me
 Finally, it prints a representative element for each of the orbits in the product.
 These elements are constructed based on the description of the orbits stored, filled in to make their support equal to sets of the form $\{1, 2, \ldots, n\}$.
 
-\todo{Linenumbering}
-
 \starttyping
 nomset<rational> A = nomset_rationals();
 nomset<pair<rational, rational>> B({rational(1),rational(2)});
@@ -515,7 +513,7 @@ These languages naturally arise as the semantics of register automata.
 The definition of register automata is not as simple as that of ordinary finite automata.
 Consequently, transferring results from automata theory to this setting often requires non-trivial proofs.
 Nominal automata, instead, are defined as ordinary automata by replacing finite sets with orbit-finite nominal sets.
-The theory of nominal automata is developed by \citet[bojanczyk2014automata] and it is shown that many, but not all, algorithms from automata theory transfer to nominal automata.
+The theory of nominal automata is developed by \citet[DBLP:journals/corr/BojanczykKL14] and it is shown that many, but not all, algorithms from automata theory transfer to nominal automata.
 
 As an example we consider the following language on rational numbers:
 \startformula
@@ -618,20 +616,20 @@ The alphabet is defined by two orbits: $\{\kw{Put}(a) \mid a \in \Q \}$ and $\{\
 \description{$\Lint$} The language accepting a series of nested intervals, as defined above.
 
 In \in{Table}[minimize_results] we report the number of orbits for each automaton.
-The first two classes of automata were previously used as test cases by \citet[moerman2017learning].
+The first two classes of automata were previously used as test cases by \citet[MoermanS0KS17].
 These two classes are also equivariant w.r.t. the equality symmetry.
 The extra bit of structure allows the automata to be encoded more efficiently, as we do not need to encode a transition for each orbit in $S \times A$.
 Instead, a more symbolic encoding is possible.
 Both \LOIS{} and \NLambda{} allow to use this more symbolic representation.
 Our tool, \ONS{}, only works with nominal sets and the input data needs to be provided orbit-wise.
-Where applicable, the automata listed above were generated using the code from \citet[moerman2017learning], ported to the other libraries as needed.
+Where applicable, the automata listed above were generated using the code from \citet[MoermanS0KS17], ported to the other libraries as needed.
 
 
 \stopsubsubsection
 \startsubsection
   [title={Minimising nominal automata}]
 
-For languages recognised by nominal DFAs, a Myhill-Nerode theorem holds which relates states to right congruence classes \citep[bojanczyk2014automata].
+For languages recognised by nominal DFAs, a Myhill-Nerode theorem holds which relates states to right congruence classes \citep[DBLP:journals/corr/BojanczykKL14].
 This guarantees the existence of unique minimal automata.
 We say an automaton is \emph{minimal} if its set of states has the least number of orbits and each orbit has the smallest dimension possible.
 \footnote{Abstractly, an automaton is minimal if it has no proper quotients.
@@ -690,7 +688,7 @@ This suggest that it is possible to further optimise an implementation with simi
   [title={Implementations.}]
 
 We implemented the minimisation algorithm in \ONS{}.
-For \NLambda{} and \LOIS{} we used their implementations of Moore's minimisation algorithm \citep[EPTCS207.3, kopczynski1716, kopczynski2017].
+For \NLambda{} and \LOIS{} we used their implementations of Moore's minimisation algorithm \citep[DBLP:journals/corr/KlinS16, DBLP:conf/cade/KopczynskiT16, DBLP:conf/popl/KopczynskiT17].
 For each of the libraries, we wrote routines to read in an automaton from a file and,
 for the structured test cases, to generate the requested automaton.
 For \ONS{}, all automata were read from file.
@@ -750,22 +748,22 @@ Despite this, it remains viable: even for the larger cases it falls behind signi
 
 Another application that we implemented in \ONS{} is \emph{automata learning}.
 The aim of automata learning is to infer an unknown regular language $\lang$.
-We use the framework of active learning as set up by \citet[Angluin87]
+We use the framework of active learning as set up by \citet[DBLP:journals/iandc/Angluin87]
 where a learning algorithm can query an oracle to gather information about $\lang$.
 Formally, the oracle can answer two types of queries:
 \startitemize
 \item \emph{membership queries}, where a query consists of a word $w \in A^{*}$ and the oracle replies whether $w \in \lang$, and
 \item \emph{equivalence queries}, where a query consists of an automaton $\mathcal{H}$ and the oracle replies positively if $\lang(\mathcal{H}) = \lang$ or provides a counterexample if $\lang(\mathcal{H}) \neq \lang$.
 \stopitemize
-With these queries, the \LStar{} algorithm can learn regular languages efficiently \citep[Angluin87].
+With these queries, the \LStar{} algorithm can learn regular languages efficiently \citep[DBLP:journals/iandc/Angluin87].
 In particular, it learns the unique minimal automaton for $\lang$ using only finitely many queries.
-The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages \citep[moerman2017learning].
+The \LStar{} algorithm has been generalised to \nLStar{} in order to learn \emph{nominal} regular languages \citep[MoermanS0KS17].
 In particular, it learns a nominal DFA (over an infinite alphabet) using only finitely many queries.
 We implement \nLStar{} in the presented library and compare it to its previous implementation in \NLambda{}.
 The algorithm is not polynomial, unlike the minimisation algorithm described above.
 However, the authors conjecture that there is a polynomial algorithm.
 \footnote{See \todo{joshuamoerman.nl/papers/2017/17popl-learning-nominal-automata.html} for a sketch of the polynomial algorithm.}
-For the correctness, termination, and comparison with other learning algorithms see \citep[moerman2017learning].
+For the correctness, termination, and comparison with other learning algorithms see \in{Chapter}[chap:learning-nominal-automata].
 
 
 \startsubsubsection
@@ -842,7 +840,7 @@ It is interesting to see that these languages can be learned more efficiently by
   [title={Related work},
    reference=sec:related]
 
-As stated in the introduction, \NLambda{} by \citet[EPTCS207.3] and \LOIS{} by \citet[kopczynski1716] use first-order formulas to represent nominal sets and use SMT solvers to manipulate them.
+As stated in the introduction, \NLambda{} by \citet[DBLP:journals/corr/KlinS16] and \LOIS{} by \citet[DBLP:conf/cade/KopczynskiT16] use first-order formulas to represent nominal sets and use SMT solvers to manipulate them.
 This makes both libraries very flexible and they indeed implement the equality symmetry as well as the total order symmetry.
 As their representation is not unique, the efficiency depends on how the logical formulas are constructed.
 As such, they do not provide complexity results.
@@ -852,30 +850,30 @@ A second big difference is that both \NLambda{} and \LOIS{} implement a \quotati
 This means that they overload natural programming constructs in their host languages (\haskell{} and \cpp{} respectively).
 For programmers this means they can think of infinite sets without having to know about nominal sets.
 
-It is worth mentioning that an older (unreleased) version of \NLambda{} implemented nominal sets with orbits instead of SMT solvers \citep[towardsnominal].
+It is worth mentioning that an older (unreleased) version of \NLambda{} implemented nominal sets with orbits instead of SMT solvers \citep[DBLP:conf/popl/BojanczykBKL12].
 However, instead of characterising orbits (e.g., by its dimension), they represent orbits by a representative element.
-The authors of \NLambda{} have reported that the current version is faster \citep[EPTCS207.3].
+The authors of \NLambda{} have reported that the current version is faster \citep[DBLP:journals/corr/KlinS16].
 
-The theoretical foundation of our work is the main representation theorem in \citep[bojanczyk2014automata].
+The theoretical foundation of our work is the main representation theorem in \citep[DBLP:journals/corr/BojanczykKL14].
 We improve on that by instantiating it to the total order symmetry and distil a concrete representation of nominal sets.
-As far as we know, we provide the first implementation of the representation theory in \citep[bojanczyk2014automata].
+As far as we know, we provide the first implementation of the representation theory in \citep[DBLP:journals/corr/BojanczykKL14].
 
-Another tool using nominal sets is Mihda \citep[ferrari2005].
+Another tool using nominal sets is Mihda \citep[FerrariMT05].
 Here, only the equality symmetry is implemented.
 This tool implements a translation from $\pi$-calculus to history-dependent automata (HD-automata) with the aim of minimisation and checking bisimilarity.
 The implementation in OCaml is based on \emph{named sets}, which are finite representations for nominal sets.
 The theory of named sets is well-studied and has been used to model various behavioural models with local names.
-For those results, the categorical equivalences between named sets, nominal sets and a certain (pre)sheaf category have been exploited \citep[CianciaKM10, CianciaM10].
+For those results, the categorical equivalences between named sets, nominal sets and a certain (pre)sheaf category have been exploited \citep[CianciaKM10, DBLP:journals/iandc/CianciaM10].
 The total order symmetry is not mentioned in their work.
 We do, however, believe that similar equivalences between categories can be stated.
 Interestingly, the product of named sets is similar to our representation of products of nominal sets: pairs of elements together with data which denotes the relation between data values.
 
-Fresh OCaml by \citet[shinwell2005fresh] and Nominal Isabelle by \citet[urban2005nominal] are
+Fresh OCaml by \citet[ShinwellP05] and Nominal Isabelle by \citet[UrbanT05] are
 both specialised in name-binding and $\alpha$-conversion used in proof systems.
 They only use the equality symmetry and do not provide a library for manipulating nominal sets.
 Hence they are not suited for our applications.
 
-On the theoretical side, there are many complexity results for register automata \citep[DBLP:journals/corr/abs-1209-0680, DBLP:conf/lics/MurawskiRT15].
+On the theoretical side, there are many complexity results for register automata \citep[DBLP:journals/corr/GrigoreT16, MurawskiRT15].
 In particular, we note that problems such as emptiness and equivalence are NP-hard depending on the type of register automaton.
 This does not easily compare to our complexity results for minimisation.
 One difference is that we use the total order symmetry, where the local symmetries are always trivial (\in{Lemma}[group_trivial]).
@@ -883,9 +881,9 @@ As a consequence, all the complexity required to deal with groups vanishes.
 Rather, the complexity is transferred to the input of our algorithms, because automata over the equality symmetry require more orbits when expressed over the total order symmetry.
 Another difference is that register automata allow for duplicate values in the registers.
 In nominal automata, such configurations will be encoded in different orbits.
-An interesting open problem is whether equivalence of unique-valued register automata is in {\sc Ptime} \citep[DBLP:conf/lics/MurawskiRT15].
+An interesting open problem is whether equivalence of unique-valued register automata is in {\sc Ptime} \citep[MurawskiRT15].
 
-Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DAntoniV17, maler2017generic].
+Orthogonal to nominal automata, there is the notion of symbolic automata \citep[DBLP:conf/cav/DAntoniV17, MalerM17].
 These automata are also defined over infinite alphabets but they use predicates on transitions, instead of relying on symmetries.
 Symbolic automata are finite state (as opposed to infinite state nominal automata) and do not allow for storing values.
 However, they do allow for general predicates over an infinite alphabet, including comparison to constants.
@@ -906,7 +904,7 @@ A natural direction for future work is to consider other symmetries, such as the
 Here, we may take inspiration from existing tools such as Mihda (see \in{Section}[sec:related]).
 Another interesting question is whether it is possible to translate a nominal automaton over the total order symmetry which accepts an equality language to an automaton over the equality symmetry.
 This would allow one to efficiently move between symmetries.
-Finally, our techniques can potentially be applied to timed automata by exploiting the intriguing connection between the nominal automata that we consider and timed automata \citep[BojanczykL12].
+Finally, our techniques can potentially be applied to timed automata by exploiting the intriguing connection between the nominal automata that we consider and timed automata \citep[DBLP:conf/icalp/BojanczykL12].
 
 
 \stopsection