# Publications of Stefan Milius

You may also want to check my DBLP page.

Click on titles to see abstracts and pdf's.

Filter by publication type: All () Journal () Conference () Edited () Other ()

## 2020

Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors
Draft book.

## Abstract

This draft contains the first ten chapters of our book.

## Bibtex

@unpublished{ammbook, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss}, title = {Initial Algebras, Terminal Coalgebras, and the Theory of Fixed Points of Functors}, note = {Draft book, available from \url{http://www.stefan-milius.eu}}, year = {2020}, }
Efficient and Modular Coalgebraic Partition Refinement
Log. Methods Comput. Sci., vol. 16 (1), pp. 8:1-8:63, 2020. Journal version of CONCUR 2017 conference paper below.

## Abstract

We present a generic partition refinement algorithm that quotients coalgebraic systems by behavioural equivalence, an important task in system analysis and verification. Coalgebraic generality allows us to cover not only classical relational systems but also, e.g. various forms of weighted systems and furthermore to flexibly combine existing system types. Under assumptions on the type functor that allow representing its finite coalgebras in terms of nodes and edges, our algorithm runs in time O(m log(n)) where n and m are the numbers of nodes and edges, respectively. The generic complexity result and the possibility of combining system types yields a toolbox for efficient partition refinement algorithms. Instances of our generic algorithm match the run-time of the best known algorithms for unlabelled transition systems, Markov chains, deterministic automata (with fixed alphabets), Segala systems, and for color refinement.

## Bibtex

@article{wdms20, author = {Thorsten Wißmann and Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder}, title = {Efficient and Modular Coalgebraic Partition Refinement}, journal = {Log. Methods Comput. Sci.}, year = {2020}, volume = {16}, number = {1}, pages = {8:1--8:63}, }
On Well-Founded and Recursive Coalgebras
In: Proc. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20),
Lecture Notes Comput. Sci. (ARCoSS), vol. 12077, pp. 17-36.

## Abstract

This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving endofunctors on complete and well-powered categories every coalgebra has a well-founded part, and we provide a new, shorter proof that this is the coreflection in the category of all well-founded coalgebras. We present a new more general proof of Taylor's General Recursion Theorem that every well-founded coalgebra is recursive, and we study under which hypothesis the converse holds. In addition, we present a new equivalent characterization of well-foundedness: a coalgebra is well-founded iff it admits a coalgebra-to-algebra morphism to the initial algebra.

## Bibtex

@inproceedings{amm20, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss}, title = {On Well-Founded and Recursive Coalgebras}, booktitle = {Proc. 23rd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'20)}, year = {2020}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {12077}, pages = {17--36}, }

## 2019

A Coalgebraic View on Reachability
Comment. Math. Univ. Carolin., vol. 60 (4), pp. 605-638, 2019.

## Abstract

Coalgebras for an endofunctor provide a category-theoretic framework for modeling a wide range of state-based systems of various types. We provide an iterative construction of the reachable part of a given pointed coalgebra that is inspired by and resembles the standard breadth-first search procedure to compute the reachable part of a graph. We also study coalgebras in Kleisli categories: for a functor extending a functor on the base category, we show that the reachable part of a given pointed coalgebra can be computed in that base category.

## Bibtex

@article{wmkd19, author = {Thorsten Wißmann and Stefan Milius and J\'er\'emy Dubut and Shin-ya Katsumata}, title = {A Coalgebraic View on Reachability}, journal = {Comment. Math. Univ. Carolin.}, year = {2019}, volume = {60}, number = {4}, pages = {605--638}, }
Towards a Uniform Theory of Effectful State Machines
Accepted for publication in ACM Trans. Comput. Log. Jourcal version of TCS'14 paper below.

## Abstract

Using recent developments on coalgebraic and monad-based semantics, we present a uniform study of various notions of machines, e.g. finite state machines, multi-stack machines, Turing machines, valence automata, and weighted automata. They are instances of Jacobs' notion of a T-automaton}, where T is a monad. We show that the generic language semantics for T-automata correctly instantiates the usual language semantics for a number of known classes of machines/languages, including~regular, context-free, recursively-enumerable and various subclasses of context free languages (e.g. deterministic and real-time ones). Moreover, our approach provides new generic techniques for studying the expressivity power of various machine-based models.

## Bibtex

@unpublished{gms19, author = {Sergey Goncharov and Stefan Milius and Alexandra Silva}, title = {Towards a Uniform Theory of Effectful State Machines}, note = {Accepted for publication in ACM Trans. Comput. Log. Jourcal version of TCS'14 paper below, available from \url{http://www.stefan-milius.eu}}, year = {2019}, }
Finitely Presentable Algebras For Finitary Monads
Theory Appl. Categ., vol. 34, pp. 1179-1195, 2019.

## Abstract

For finitary regular monads $\T$ on locally finitely presentable categories we characterize the finitely presentable objects in the category of $\T$-algebras in the style known from general algebra: they are precisely the algebras presentable by finitely many generators and finitely many relations.

## Bibtex

@article{amsw19_2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wißmann}, title = {Finitely Presentable Algebras For Finitary Monads}, journal = {Theory Appl. Categ.}, year = {2019}, volume = {34}, pages = {1179--1195}, }
On Finitary Functors
Theory Appl. Categ., vol. 34, pp. 1134-1164, 2019.

## Abstract

A simple criterion for a functor to be finitary is presented: we call $F$ finitely bounded if for all objects $X$ every finitely generated subobject of $FX$ factorizes through the $F$-image of a finitely generated subobject of $X$. This is equivalent to $F$ being finitary for all functors between reasonable' locally finitely presentable categories, provided that $F$ preserves monomorphisms. We also discuss the question when that last assumption can be dropped.

All this generalizes to locally $\lambda$-presentable categories, $\lambda$-accessible functors and $\lambda$-presentable algebras. As an application we obtain an easy proof that the Hausdorff functor on the category of complete metric spaces is $\aleph_1$-accessible.

## Bibtex

@article{amsw19_1, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lurdes Sousa and Thorsten Wißmann}, title = {On Finitary Functors}, journal = {Theory Appl. Categ.}, year = {2019}, volume = {34}, pages = {1134--1164}, }
Hans-Peter Deifel, Stefan Milius, Lutz Schröder and Thorsten Wißmann
Generic Partition Refinement and Weighted Tree Automata
In: Proc. International Symposium on Formal Methods (FM'19),
Lecture Notes Comput. Sci., vol. 11800, pp. 280-297.

## Abstract

Partition refinement is a method for minimizing automata and transition systems of various types. Recently, we have developed a partition refinement algorithm that is generic in the transition type of the given system and matches the run time of the best known algorithms for many concrete types of systems, e.g.~deterministic automata as well as ordinary, weighted, and probabilistic (labelled) transition systems. Genericity is achieved by modelling transition types as functors on sets, and systems as coalgebras. In the present work, we refine the run time analysis of our algorithm to cover additional instances, notably weighted automata and, more generally, weighted tree automata. For weights in a cancellative monoid we match, and for non-cancellative monoids such as (the additive monoid of) the tropical semiring even substantially improve, the asymptotic run time of the best known algorithms. We have implemented our algorithm in a generic tool that is easily instantiated to concrete system types by implementing a simple refinement interface. Moreover, the algorithm and the tool are modular, and partition refiners for new types of systems are obtained easily by composing pre-implemented basic functors. Experiments show that even for complex system types, the tool is able to handle systems with millions of transitions.

## Bibtex

@inproceedings{dmsw19, author = {Hans-Peter Deifel and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann}, title = {Generic Partition Refinement and Weighted Tree Automata}, booktitle = {Proc. International Symposium on Formal Methods (FM'19)}, year = {2019}, series = {Lecture Notes Comput. Sci.}, volume = {11800}, pages = {280--297}, }
In: Proc. 30th International Conference on Concurrency Theory (CONCUR 2017),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 140, pp. 36:1-36:16.

## Abstract

State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.

## Bibtex

@inproceedings{dms19, author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder}, title = {Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum}, booktitle = {Proc. 30th International Conference on Concurrency Theory (CONCUR 2017)}, year = {2019}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {140}, pages = {36:1--36:16}, }
A New Foundation for Finitary Corecursion and Iterative Algebras
Inform. and Comput., vol. ???, pp. ???, 2019. Journal version of FoSSaCS'16 conference paper below.

## Abstract

This paper contributes to a theory of the behaviour of ""finite-state" systems that is generic in the system type. We propose that such systems are modeled as coalgebras with a finitely generated carrier for an endofunctor on a locally finitely presentable category. Their behaviour gives rise to a new fixpoint of the coalgebraic type functor called locally finite fixpoint (LFF). We prove that if the given endofunctor is finitary and preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adamek et al.). Moreover, we show that the LFF is characterized by two universal properties: (1) as the final locally finitely generated coalgebra, and (2) as the initial fg-iterative algebra. As instances of the LFF we first obtain the known instances of the rational fixpoint, e.g. regular languages, rational streams and formal power-series, regular trees etc. Moreover, we obtain a number of new examples, e.g. (realtime deterministic resp. non-deterministic) context-free languages, constructively S-algebraic formal power-series (in general, the behaviour of finite coalgebras under the coalgebraic language semantics arising from the generalized powerset construction by Silva et al., and the monad of Courcelle's algebraic trees.

## Bibtex

@article{mpw19, author = {Stefan Milius and Dirk Pattinson and Thorsten Wißmann}, title = {A New Foundation for Finitary Corecursion and Iterative Algebras}, journal = {Inform. and Comput.}, year = {2019}, volume = {???}, pages = {???}, }
Stefan Milius and Joël Ouaknine (editors)
Special Issue with Selected Papers of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Logical Methods in Computer Science, 2019.
Special issue with selected papers of the conference LICS'17.

## Bibtex

@proceedings{mo19, editor = {Stefan Milius and Joël Ouaknine}, title = {Special Issue with Selected Papers of the Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)}, publisher = {}, series = {Logical Methods in Computer Science}, year = {2019}, volume = {}, number = {}, pages = {}, }
Varieties of Data Languages
In: Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP'19),
Leibniz International Proceedings in Informatics (LIPIcs), vol. 132, pp. 130:1--130:14.

## Abstract

We establish an Eilenberg-type correspondence for data languages, i.e.~languages over an infinite alphabet. More precisely, we prove that there is a bijective correspondence between varieties of languages recognized by orbit-finite nominal monoids and pseudovarieties of such monoids. This is the first result of this kind for data languages. Our approach makes use of nominal Stone duality and a recent category theoretic generalization of Birkhoff-type theorems that we instantiate here for the category of nominal sets. In addition, we prove an axiomatic characterization of weak pseudovarieties as those classes of orbit-finite monoids that can be specified by sequences of nominal equations, which provides a nominal version of a classical theorem of Eilenberg and Schützenberger.

## Bibtex

@inproceedings{um19, author = {Stefan Milius and Henning Urbat}, title = {Varieties of Data Languages}, booktitle = {Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP'19)}, year = {2019}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, volume = {132}, pages = {130:1----130:14}, }
Equational Axiomatization of Algebras with Structure
In: Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'19),
Lecture Notes Comput. Sci. (ARCoSS), vol. 11425, pp. 400-417.

## Abstract

This paper proposes a new category theoretic account of equationally axiomatizable classes of algebras. Our approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. Our main contributions are a generic HSP theorem and a sound and complete equational logic, which are shown to encompass numerous flavors of equational axiomizations studied in the literature.

## Bibtex

@inproceedings{mu19, author = {Stefan Milius and Henning Urbat}, title = {Equational Axiomatization of Algebras with Structure}, booktitle = {Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'19)}, year = {2019}, series = {Lecture Notes Comput. Sci. (ARCoSS)}, volume = {11425}, pages = {400--417}, }
On functors preserving coproducts and algebras with iterativity
Theoret. Comput. Sci., vol. 763, pp. 66-87, 2019. Journal version of CALCO'17 conference paper below.

## Abstract

An algebra for a functor $H$ is called completely iterative (cia, for short) if every flat recursive equation in it has a unique solution. Every cia is corecursive, i.e. it admits a unique coalgebra-to-algebra morphism from every coalgebra. If the converse also holds, $H$ is called a cia functor. We prove that whenever the base category is hyper-extensive (i.e.~countable coproducts are "well-behaved") and $H$ preserves countable coproducts, then $H$ is a cia functor. Surprisingly few cia functors exists among standard finitary set functors: in fact, the only ones are those preserving coproducts; they are given by $X \mapsto W \times (-) + Y$ for some sets $W$ and $Y$.

## Bibtex

@article{am19, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius}, title = {On functors preserving coproducts and algebras with iterativity}, journal = {Theoret. Comput. Sci.}, year = {2019}, volume = {763}, pages = {66--87}, }
Jiří Adámek, Stefan Milius, Rob Myers and Henning Urbat
Generalized Eilenberg theorem: Varieties of languages in a category
ACM Trans. Comput. Log., vol. 20 (1), pp. 3:1-3:47, 2019.

## Abstract

For finite automata as coalgebras in a category $\C$ we study languages they accept, and varieties of such languages. This generalizes Eilenberg's concept of a variety of languages which corresponds to choosing as $\Cat$ the category of boolean algebras. Eilenberg established a bijective correspondence between pseudovarieties of monoids and varieties of regular languages. In our generalization we work with a pair $\C/\D$ of locally finite varieties of algebras that are predual, i.e. dualize on the level of finite algebras, and we prove that pseudovarieties of $\D$-monoids bijectively correspond to varieties of regular languages in $\C$. As one instance, Eilenberg's result is recovered by choosing $\D=$ sets and $\Cat=$ boolean algebras. Another instance, Pin's result on pseudovarieties of ordered monoids, is covered by taking $\D=$ posets and $\C=$ distributive lattices. By choosing as $\C=\D$ the self-predual category of join-semilattices we obtain Polák's result on pseudovarieties of idempotent semirings. Similar, using the self-preduality of vector spaces over a finite field $K$, our result covers that of Reutenauer on pseudovarieties of $K$-algebras. Several new variants of Eilenberg's theorem arise by taking other predualities, e.g. between the categories of non-unital boolean rings and of pointed sets. In each of these cases we also prove a local variant of the bijection, where a fixed alphabet is assumed and one considers local varieties of regular languages over that alphabet in the category $\C$.

## Bibtex

@article{ammu19, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat}, title = {Generalized Eilenberg theorem: Varieties of languages in a category}, journal = {ACM Trans. Comput. Log.}, year = {2019}, volume = {20}, number = {1}, pages = {3:1--3:47}, }

## 2018

Stefan Milius and Lawrence S. Moss (editors)
Special Issue in Honor of Jiří Adámek
Logical Methods in Computer Science, 2018.
Special Festschrift Issue celebrating Jiří Adámek's 70th birthday.

## Bibtex

@proceedings{mm18, editor = {Stefan Milius and Lawrence S. Moss}, title = {Special Issue in Honor of Jiří Adámek}, publisher = {}, series = {Logical Methods in Computer Science}, year = {2018}, volume = {}, number = {}, pages = {}, }
Stefan Milius
Proper Functors and Fixed Points for Finite Behaviour
Log. Methods Comput. Sci., vol. 14 (3:22), 32 pp., 2018. Journal version of CALCO'17 conference paper below.

## Abstract

The rational fixed point of a set functor is well-known to capture the behaviour of finite coalgebras. In this paper we consider functors on algebraic categories. For them the rational fixed point may no longer be fully abstract, i.e.~a subcoalgebra of the final coalgebra. Inspired by Ésik and Maletti's notion of a proper semiring, we introduce the notion of a proper functor. We show that for proper functors the rational fixed point is determined as the colimit of all coalgebras with a free finitely generated algebra as carrier and it is a subcoalgebra of the final coalgebra. Moreover, we prove that a functor is proper if and only if that colimit is a subcoalgebra of the final coalgebra. These results serve as technical tools for soundness and completeness proofs for coalgebraic regular expression calculi, e.g.~for weighted automata.

## Bibtex

@article{milius18, author = {Stefan Milius}, title = {Proper Functors and Fixed Points for Finite Behaviour}, journal = {Log. Methods Comput. Sci.}, year = {2018}, volume = {14}, number = {3:22}, pages = {32 pp.}, }
Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages
In: Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18),
Lecture Notes Comput. Sci., vol. 11202, pp. 56-77.

## Abstract

We introduce a generic expression language describing behaviours of finite coalgebras over sets; besides relational systems, this covers, e.g., weighted, probabilistic, and neighbourhood-based system types. We prove a generic Kleene-type theorem establishing a correspondence between our expressions and finite systems. Our expression language is similar to one introduced in previous work by Myers but has a semantics defined in terms of a particular form of predicate liftings as used in coalgebraic modal logic; in fact, our expressions can be regarded as a particular type of modal fixed point formulas. The predicate liftings in question are required to satisfy a natural preservation property; we show that this property holds in particular for the Moss liftings introduced by Marti and Venema in work on lax extensions.

## Bibtex

@inproceedings{dmst18, author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann}, title = {Predicate Liftings and Functor Presentations in Coalgebraic Expression Languages}, booktitle = {Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18)}, year = {2018}, series = {Lecture Notes Comput. Sci.}, volume = {11202}, pages = {56--77}, }
On Algebras with Effectful Iteration
In: Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18),
Lecture Notes Comput. Sci., vol. 11202, pp. 144-166.

## Abstract

For every finitary monad T on sets and every endofunctor F on the category of T-algebras we introduce the concept of an ffg-Elgot algebra for F, that is, an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad T. The goal of this paper is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point $\phi F$, the colimit of all F-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of T-algebras.

## Bibtex

@inproceedings{amu18_cmcs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat}, title = {On Algebras with Effectful Iteration}, booktitle = {Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS'18)}, year = {2018}, series = {Lecture Notes Comput. Sci.}, volume = {11202}, pages = {144--166}, }
A Categorical Approach to Syntactic Monoids
Log. Methods Comput. Sci., vol. 14 (2:9), 34 pp., 2018. Journal version of CALCO'15 conference paper below.

## Bibtex

@article{amv_secalg, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On second-order iterative monads}, journal = {Theoret. Comput. Sci.}, year = {2011}, volume = {412}, number = {38}, pages = {4969--4988}, }
Semantics of higher-order recursion schemes
Log. Methods Comput. Sci., vol. 7 (1:15), 43 pp., 2011.

## Abstract

Higher-order recursion schemes are recursive equations defining new operations from given ones called terminals''. Every such recursion scheme is proved to have a least interpreted semantics in every Scott's model of λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in λ-calculus by an endofunctor H_λ and they explained simultaneous substitution of λ-terms by proving that the presheaf of λ-terms is an initial H_λ-monoid. Here we work with the presheaf of rational infinite λ-terms and prove that this is an initial iterative H_λ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.

## Bibtex

@article{amv_highord, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Semantics of higher-order recursion schemes}, journal = {Log. Methods Comput. Sci.}, year = {2011}, volume = {7}, number = {1:15}, pages = {43 pp.}, }
Elgot theories: a new perspective of the equational properties of iteration
Math. Structures Comput. Sci., vol. 21 (2), pp. 417-480, 2011. © Cambridge University Press.

## Abstract

The concept of iteration theory of Bloom and Ésik summarizes all equational properties that iteration has in usual applications, e.g., in Domain Theory where to every system of recursive equations the least solution is assigned. This paper shows that in the more general coalgebraic approach to iteration the more suitable concept is that of a functorial iteration theory (called Elgot theory). These theories have a particularly simple axiomatization, and all well-known examples of iteration theories are functorial. Elgot theories are proved to be monadic over the category of sets in context (or, more generally, the category of finitary endofunctors of a locally finitely presentable category). This demonstrates that functoriality is an equational property from the perspective of sets in context. In contrast, Bloom and Ésik worked in the base category of signatures in lieu of sets in context, where iteration theories are monadic but Elgot theories are not. This explains why functoriality was not included into the definition of iteration theories.

## Bibtex

@article{amv_em2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot theories: a new perspective of the equational properties of iteration}, journal = {Math. Structures Comput. Sci.}, year = {2011}, volume = {21}, number = {2}, pages = {417--480}, }
Ilyas Daskaya, Michaela Huhn and Stefan Milius
Formal Safety Analysis in Industrial Practice
In: Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11),
Lecture Notes Comput. Sci., vol. 6959, pp. 68-84.

## Abstract

We report on a comparative study on formal verification of two level crossing controllers that were developed using SCADE by a rail automation manufacturer. Deductive Cause-Consequence Analysis of Ortmeier et al. is applied for formal safety analysis and in addition, safety requirements are proven. Even with these medium size industrial case studies we observed intense complexity problems that could not be overcome by employing different heuristics like abstraction and compositional verification. In particular, we failed to prove a crucial liveness property within the SCADE framework stating that an unsafe state will not be persistent. We finally succeeded to prove this property by combining abstraction and model transformation from SCADE to UPPAAL timed automata. In addition, we found that the modeling style has a significant impact on the complexity of the verification task.

## Bibtex

@inproceedings{dhm11, author = {Ilyas Daskaya and Michaela Huhn and Stefan Milius}, title = {Formal Safety Analysis in Industrial Practice}, booktitle = {Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'11)}, year = {2011}, series = {Lecture Notes Comput. Sci.}, volume = {6959}, pages = {68--84}, }

## 2010

Recursive Program Schemes and Context-Free Monads
In: Proc. Coalgebraic Methods in Computer Science (CMCS'10),
Electron. Notes Theor. Comput. Sci., vol. 264, pp. 3-23.

## Abstract

Solutions of recursive program schemes over a given signature Σ were characterized by Bruno Courcelle as precisely the context-free (or algebraic) Σ-trees. These are the finite and infinite Σ-trees yielding, via labelling of paths, context-free languages. Our aim is to generalize this to finitary endofunctors H of general categories: we construct a monad C^H “generated” by solutions of recursive program schemes of type H, and prove that this monad is ideal. In case of polynomial endofunctors of Set our construction precisely yields the monad of context-free Σ-trees of Courcelle. Our result builds on a result by N. Ghani et al on solutions of algebraic systems.

## Bibtex

@inproceedings{amv_algtrees, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Recursive Program Schemes and Context-Free Monads}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'10)}, year = {2010}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {264}, pages = {3--23}, }
Math. Structures Comput. Sci., vol. 20 (3), pp. 419-452, 2010. © Cambridge University Press.

## Abstract

Iterative monads were introduced by Calvin Elgot in the 1970’s and are those ideal monads in which every guarded system of recursive equations has a unique solution. We prove that every ideal monad M has an iterative reflection, that is, an embedding into an iterative monad with the expected universal property. We also introduce the concept of iterativity for algebras for the monad M, following in the footsteps of Evelyn Nelson and Jerzy Tiuryn, and prove that M is iterative if and only if all free algebras for M are iterative algebras.

## Bibtex

@article{amv_ref, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative reflections of monads}, journal = {Math. Structures Comput. Sci.}, year = {2010}, volume = {20}, number = {3}, pages = {419--452}, }
Inform. and Comput., vol. 208 (12), pp. 1306-1348, 2010.

## Abstract

Iterative monads of Calvin Elgot were introduced to treat the semantics of recursive equations purely algebraically. They are Lawvere theories with the property that all ideal systems of recursive equations have unique solutions. We prove that the unique solutions in iterative monads satisfy all the equational properties of iteration monads of Stephen Bloom and ZoltánÉsik, whenever the base category is hyper-extensive and locally finitely presentable. This result is a step towards proving that functorial iteration monads form a monadic category over sets in context. This shows that functoriality is an equational property when considered w.r.t. sets in context.

## Bibtex

@article{amv_em1, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Equational Properties of Iterative Monads}, journal = {Inform. and Comput.}, year = {2010}, volume = {208}, number = {12}, pages = {1306--1348}, }
Stefan Milius
A Sound and Complete Calculus for finite Stream Circuits
In: Proc. 25th Annual Symposium on Logic in Computer Science (LICS'10), pp. 449-458.

## Abstract

Stream circuits are a convenient graphical way to represent streams (or stream functions) computed by finite dimensional linear systems. We present a sound and complete expression calculus that allows us to reason about the semantic equivalence of finite closed stream circuits. For our proof of the soundness and completeness we build on recent ideas of Bonsangue, Rutten and Silva. They have provided a “Kleene theorem” and a sound and complete expression calculus for coalgebras for endofunctors of the category of sets. The key ingredient of the soundness and completeness proof is a syntactic characterization of the final locally finite coalgebra. In the present paper we extend this approach to the category of real vector spaces. We also prove that a final locally finite (dimensional) coalgebra is, equivalently, an initial iterative algebra. This makes the connection to existing work on the semantics of recursive specifications.

## Bibtex

@inproceedings{m_linexp, author = {Stefan Milius}, title = {A Sound and Complete Calculus for finite Stream Circuits}, booktitle = {Proc. 25th Annual Symposium on Logic in Computer Science (LICS'10)}, year = {2010}, pages = {449--458}, }
CIA Structures and the Semantics of Recursion
In: Proc. Foundations of Software Science and Computation Structures (FoSSaCS'10),
Lecture Notes Comput. Sci., vol. 6014, pp. 312-327.

## Abstract

Final coalgebras for a functor serve as semantic domains for state based systems of various types. For example, formal languages, streams, non-well-founded sets and behaviors of CCS processes form final coalgebras. We present a uniform account of the semantics of recursive definitions in final coalgebras by combining two ideas: (1) final coalgebras are also initial completely iterative algebras (cia); (2) additional algebraic operations on final coalgebras may be presented in terms of a distributive law λ. We first show that a distributive law leads to new extended cia structures on the final coalgebra. Then we formalize recursive function definitions involving operations given by λ as recursive program schemes for λ, and weprove that unique solutions exist in theextended cias. We illustrate our results by the four concrete final coalgebras mentioned above, e.g., a finite stream circuit defines a unique stream function and we show how to define new process combinators from given ones by sos rules involving recursion.

## Bibtex

@inproceedings{mms10, author = {Stefan Milius and Lawrence S. Moss and Daniel Schwencke}, title = {CIA Structures and the Semantics of Recursion}, booktitle = {Proc. Foundations of Software Science and Computation Structures (FoSSaCS'10)}, year = {2010}, series = {Lecture Notes Comput. Sci.}, volume = {6014}, pages = {312--327}, }

## 2009

A description of iterative reflections of monads (Extended Abstract)
In: Proc. Foundations of Software Science and Computation Structures (FoSSaCS'09),
Lecture Notes Comput. Sci., vol. 5504, pp. 152-166.

## Bibtex

@inproceedings{amv_refl2_09, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {A description of iterative reflections of monads (Extended Abstract)}, booktitle = {Proc. Foundations of Software Science and Computation Structures (FoSSaCS'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5504}, pages = {152--166}, }
Elgot theories: a new perspective on iteration theories
In: Proc. Mathematical Foundations of Programming Science (MFPS XXV),
Electron. Notes Theor. Comp. Sci., vol. 249, pp. 407-427.

## Abstract

The concept of iteration theory of Bloom and Ésik summarizes all equational properties that iteration has in usual applications, e.g., in Domain Theory where to every system of recursive equations the least solution is assigned. However, this assignment in Domain Theory is also functorial. Yet, functoriality is not included in the definition of iteration theory. Pity: functorial iteration theories have a particularly simple axiomatization, and most of examples of iteration theories are functorial. The reason for excluding functoriality was the view that this property cannot be called equational. This is true from the perspective of the category Sgn of signatures as the base category: whereas iteration theories are monadic (thus, equationally presentable) over Sgn, functorial iteration theories are not. In the present paper we propose to change the perspective and work, in lieu of Sgn, in the category of sets in context (the presheaf category of finite sets and functions). We prove that Elgot theories, which is our name for functorial iteration theories, are monadic over sets in context. Shortly: from the new perspective functoriality is equational.

## Bibtex

@inproceedings{amv_em2_mfps, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot theories: a new perspective on iteration theories}, booktitle = {Proc. Mathematical Foundations of Programming Science (MFPS XXV)}, year = {2009}, series = {Electron. Notes Theor. Comp. Sci.}, volume = {249}, pages = {407--427}, }
Semantics of Higher-Order Recursion Schemes
In: Proc. 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO'09),
Lecture Notes Comput. Sci., vol. 5728, pp. 49-63.

## Abstract

Higher-order recursion schemes are equations defining recursively new operations from given ones called “terminals”. Every such recursion scheme is proved to have a least interpreted semantics in every Scott’s model of λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Whereas Fiore et al proved that the presheaf F_λ of λ-terms is an initial H_λ-monoid, we work with the presheaf R_λ of rational infinite λ-terms and prove that this is an initial iterative Hλ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in R_λ.

## Bibtex

@inproceedings{amv_horps, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Semantics of Higher-Order Recursion Schemes}, booktitle = {Proc. 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5728}, pages = {49--63}, }
Complete Iterativity for Algebras with Effects
In: Proc. Coalgebraic and Algebraic Methods in Computer Science (CALCO'09),
Lecture Notes Comput. Sci., vol. 5728, pp. 34-48.

## Abstract

Completely iterative algebras (cias) are those algebras in which recursive equations have unique solutions. In this paper we study complete iterativity for algebras with computational effects (described by a monad). First, we prove that for every analytic endofunctor on Set there exists a canonical distributive law over any commutative monad M, hence a lifting of that endofunctor to the Kleisli category of M. Then, for an arbitrary distributive law λ of an endofunctor H on Set over a monad M we introduce λ-cias. The cias for the corresponding lifting of H (called Kleisli-cias) form a full subcategory of the category of λ-cias. For various monads of interest we prove that free Kleisli-cias coincide with free λ-cias, and these free algebras are given by free algebras for H. Finally, for three concrete examples of monads we prove that Kleisli-cias and λ-cias coincide and give a characterisation of those algebras.

## Bibtex

@inproceedings{mps, author = {Stefan Milius and Thorsten Palm and Daniel Schwencke}, title = {Complete Iterativity for Algebras with Effects}, booktitle = {Proc. Coalgebraic and Algebraic Methods in Computer Science (CALCO'09)}, year = {2009}, series = {Lecture Notes Comput. Sci.}, volume = {5728}, pages = {34--48}, }
Heike Burghardt, Ralf Pinger and Stefan Milius
Modellbasierte Softwareentwicklung: Herausforderungen und Erfahrungen
Signal+Draht, vol. 101 (1+2), pp. 35-37, 2009.

## Abstract

Modellbasierte Entwicklung verspricht eine Steigerung der Effizienz in der Entwicklung. Gründe für die Effizienzsteigerung sind das frühe Aufdecken von Fehlern und die höhere Qualität der Software. Damit können Entwicklungsschleifen durch spät erkannte Fehler eingespart werden. Letztendlich wird erreicht, dass Produkte schnell und in hoher Qualität beim Kunden vorliegen.

## Bibtex

@article{bpm-sd, author = {Heike Burghardt and Ralf Pinger and Stefan Milius}, title = {Modellbasierte Softwareentwicklung: Herausforderungen und Erfahrungen}, journal = {Signal+Draht}, year = {2009}, volume = {101}, number = {1+2}, pages = {35--37}, }
Equational Properties of Recursive Program Scheme Solutions
Cah. Topol. Géom. Différ. Catég., vol. 50 (1), pp. 23-66, 2009.

## Abstract

In previous work, the authors proposed a general account of recursive program scheme solutions. This work generalized the time-honored approaches that using complete partial orders or metric spaces by offering an account using final coalgebras, Elgot algebras, and much of what is known about them. The account provided an existence and uniqueness result for the solution of a very general kind of uninterpreted recursive program scheme. In addition, it also provided a theory of interpreted solutions. This paper continues the development of the theory by deriving useful general principles which may be used to show that two recursive program schemes in our sense have the same (or related) uninterpreted solution, or that they have the same or related solutions in appropriately related interpretations.

## Bibtex

@article{mm_prop, author = {Stefan Milius and Lawrence S. Moss}, title = {Equational Properties of Recursive Program Scheme Solutions}, journal = {Cah. Topol. G\'{e}om. Diff\'{e}r. Cat\'{e}g.}, year = {2009}, volume = {50}, number = {1}, pages = {23--66}, }

## 2008

Heike Burghardt, Ralf Pinger and Stefan Milius
Modellbasierte Softwareentwicklung in der Bahntechnik
elektronik industrie, 8/9 2008.

## Abstract

Die moderne Bahntechnik weist heutzutage einen hohen Grad an Automatisierung auf. So wird mit nur sieben Betriebsleitzentralen der gesamte Bahnfernverkehr auf Deutschlands Hauptstrecken gesteuert und überwacht. Elek- tronische Stellwerke müssen daher höchsten Anforderungen an Sicherheit, Verfügbarkeit und Wartbarkeit genügen.

## Bibtex

@article{bmp08, author = {Heike Burghardt and Ralf Pinger and Stefan Milius}, title = {Modellbasierte Softwareentwicklung in der Bahntechnik}, journal = {elektronik industrie}, year = {2008}, month = {8/9}, pages = {24--26}, }
Iterative algebras: How iterative are they?
Theory Appl. Categ., vol. 19 (5), pp. 61-92, 2008.

## Abstract

Iterative algebras, defined by the property that every guarded system of recursive equations has a unique solution, are proved to have a much stronger property: every system of recursive equations has a unique strict solution. Those systems that have a unique solution in every iterative algebra are characterized.

## Bibtex

@article{abmv_how, author = {Ji\v{r}\'i Ad\'amek and Reinhard B\"orger and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative algebras: How iterative are they?}, journal = {Theory Appl. Categ.}, year = {2008}, volume = {19}, number = {5}, pages = {61--92}, }
Corrigendum to: "The Category Theoretic Solution of Recursive Program Schemes"
Theoret. Comput. Sci., vol. 403 (2-3), pp. 409-415, 2008. Corrigendum of Theoret. Comput. Sci. 366 (2006), 3-59.

## Abstract

This is a corrigendum for our paper [S. Milius, L.S. Moss, The category theoretic solution of recursive program schemes, Theoret. Comput. Sci. 366 (2006) 3–59]. The main results are correct, but we offer some changes to the definitions and proofs concerning interpreted recursive program schemes.

## Bibtex

@article{mm_corr, author = {Stefan Milius and Lawrence S. Moss}, title = {Corrigendum to: "The Category Theoretic Solution of Recursive Program Schemes"}, journal = {Theoret. Comput. Sci.}, year = {2008}, volume = {403}, number = {2-3}, pages = {409--415}, }
On Algebras with Iteration
J. Logic. Comput., vol. 18 (6), pp. 1047-1085, 2008.

## Abstract

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Ésik, and iteration algebras are a special case of the recently introduced Elgot algebras (which are the monadic algebras for the free iterative monad). Another special case of iteration algebras are the iterative algebras of E. Nelson and J. Tiuryn, which are algebras with unique solutions of all guarded systems. For each of the above classes of algebras an example is provided showing that the inclusion in a wider class is proper.

## Bibtex

@article{abm_iteration, author = {Ji\v{r}\'i Ad\'amek and Stephen L. Bloom and Stefan Milius}, title = {On Algebras with Iteration}, journal = {J. Logic. Comput.}, year = {2008}, volume = {18}, number = {6}, pages = {1047--1085}, }
Stefan Milius and Uwe Steinke
Modelbasierte Softwarentwickung mit SCADE in der Eisenbahnautomatisierung
In: Proc. Fourth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2008), pp. 68-77.

## Abstract

Wir berichten in diesem Beitrag über ein momentan laufendes Pilotprojekt zur modellbasierten Entwicklung sicherheitsrelevanter Software bei Siemens Mobility im Bereich Eisenbahnautomatisierung. In der Pilotierung benutzen wir SCADE Version 6, ein Tool für die modellbasierte Entwicklung sicherheitsrelevanter Software von der Firma Esterel Technologies. Wir stellen kurz die wesentlichen Merkmale von SCADE vor, und wir berichten von den Erkenntnissen, die wir während unserer Pilotierungsphasen gewonnen haben.

## Bibtex

@inproceedings{ms_scade, author = {Stefan Milius and Uwe Steinke}, title = {Modelbasierte Softwarentwickung mit SCADE in der Eisenbahnautomatisierung}, booktitle = {Proc. Fourth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2008)}, year = {2008}, pages = {68--77}, }
Bases for parametrized iterativity
Inform. and Comput., vol. 206 (8), pp. 966-1002, 2008.

## Abstract

Parametrized iterativity of an algebra means the existence of unique solutions of all finitary recursive systems of equations where recursion is allowed to use only some variables (chosen as a parameter). We show how such algebras can be introduced in an arbitrary category A by employing a base, i.e., an operation interpreting objects of A as monads on A. For every base we prove that free base algebras and free iterative base algebras exist. The main result is a coalgebraic construction of the latter: all equation morphisms form a diagram whose colimit is proved to be a free iterative base algebra.

## Bibtex

@article{amv_base2, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Bases for parametrized iterativity}, journal = {Inform. and Comput.}, year = {2008}, volume = {206}, number = {8}, pages = {966--1002}, }

## 2007

What are iteration theories?
In: Proc. 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007),
Lecture Notes Comput. Sci., vol. 4708, pp. 240-252.

## Abstract

We prove that iteration theories can be introduced as algebras for the monad Rat on the category of signatures assigning to every signature Σ the rational Σ-tree signature. This supports the result that iteration theories axiomatize precisely the equational properties of least fixed points in domain theory: Rat is the monad of free rational theories and every free rational theory has a continuous completion.

## Bibtex

@inproceedings{amv_what, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {What are iteration theories?}, booktitle = {Proc. 32nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2007)}, year = {2007}, series = {Lecture Notes Comput. Sci.}, volume = {4708}, pages = {240--252}, }
Algebras with parametrized iterativity
Theoret. Comput. Sci., vol. 388, pp. 130-151, 2007.

## Abstract

Iterative algebras, as studied by Nelson and Tiuryn, are generalized to algebras whose iterativity is parametrized in the sense that only some variables can be used for iteration. For example, in the case of one binary operation, the free iterative algebra is the algebra of all rational binary trees; if only the left-hand variable is allowed to be iterated, then the free iterative algebra is the algebra of all right-well-founded rational binary trees. In order to express such parametrized iterativity, we work with parametrized endofunctors of Set, i.e. finitary endofunctors H : Set × Set → Set, and introduce the concept of iterativity for algebras for the endofunctor X |-> H(X, X). We then describe free iterative H-algebras.

## Bibtex

@article{amv_base1, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Algebras with parametrized iterativity}, journal = {Theoret. Comput. Sci.}, year = {2007}, volume = {388}, pages = {130--151}, }
Jiří Adámek, Dominik Lücke and Stefan Milius
Recursive Coalgebras of Finitary Functors
Theor. Inform. Appl., vol. 41 (4), pp. 447-462, 2007.

## Abstract

For finitary set functors preserving inverse images, recursive coalgebras A of Paul Taylor are proved to be precisely those for which the system described by A always halts in finitely many steps.

## Bibtex

@article{alm_rec, author = {Ji\v{r}\'i Ad\'amek and Dominik L\"ucke and Stefan Milius}, title = {Recursive Coalgebras of Finitary Functors}, journal = {Theor. Inform. Appl.}, year = {2007}, volume = {41}, number = {4}, pages = {447--462}, }

## 2006

Jiří Adámek and Stefan Milius (editors)
Special Issue: Seventh Workshop on Coalgebraic Methods in Computer Science 2004
Information and Computation, vol. 204(4), pp. 435-678, 2006.
Special issue with selected papers of the workshop CMCS'04.

## Bibtex

@proceedings{AM_CMCS04, editor = {Ji\v{r}\'i Ad\'amek and Stefan Milius}, title = {Special Issue: Seventh Workshop on Coalgebraic Methods in Computer Science 2004}, publisher = {Elsevier}, series = {Information and Computation}, year = {2006}, volume = {204}, number = {4}, pages = {435--678}, }
Iterative Algebras at Work
Math. Structures Comput. Sci., vol. 16 (6), pp. 1085-1131, 2006. © Cambridge University Press.

## Abstract

Iterative theories, which were introduced by Calvin Elgot, formalise potentially infinite computations as unique solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with ‘iterative algebras’, that is, algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. Despite this, our result is much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category.

## Bibtex

@article{amv_atwork, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative Algebras at Work}, journal = {Math. Structures Comput. Sci.}, year = {2006}, volume = {16}, number = {6}, pages = {1085--1131}, }
Elgot Algebras
Log. Methods Comput. Sci., vol. 2 (5:4), 31 pp., 2006.

## Abstract

Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot to base denotational semantics on iterative theories instead, i.e., theories in which abstract recursive specifications are required to have unique solutions. Later Bloom and \'Esik studied iteration theories and iteration algebras in which a specified solution has to obey certain axioms. We propose so-called Elgot algebras as a convenient structure for semantics in the present paper. An Elgot algebra is an algebra with a specified solution for every system of flat recursive equations. That specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are stable under renaming of recursion variables) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg-Moore category of the monad given by a free iterative theory.

## Bibtex

@article{amv_elgot, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot Algebras}, journal = {Log. Methods Comput. Sci.}, year = {2006}, volume = {2}, number = {5:4}, pages = {31 pp.}, }
Elgot Algebras (extended abstract)
In: Proc. Mathematical Foundations of Programming Science (MFPS XXI),
Electron. Notes Theor. Comput. Sci., vol. 155, pp. 87-109.

## Abstract

Iterative algebras, i. e., algebras A in which flat recursive equations e have unique solutions e†, are generalized to Elgot algebras, where a choice e→e† of solutions of all such equations e is specified. This specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are “uniform”) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg–Moore category of the free iterative monad.

## Bibtex

@inproceedings{amv_elgot_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Elgot Algebras (extended abstract)}, booktitle = {Proc. Mathematical Foundations of Programming Science (MFPS XXI)}, year = {2006}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {155}, pages = {87--109}, }
Terminal Coalgebras and Free Iterative Theories
Inform. and Comput., vol. 204 (7), pp. 1139-1172, 2006.

## Abstract

Every finitary endofunctor H of Set can be represented via a finitary signature Σ and a collection of equations called “basic”. We describe a terminal coalgebra for H as the terminal Σ-coalgebra (of all Σ-trees) modulo the congruence of applying the basic equations potentially infinitely often. As an application we describe a free iterative theory on H (in the sense of Calvin Elgot) as the theory of all rational Σ-trees modulo the analogous congruence. This yields a number of new examples of iterative theories, e.g., the theory of all strongly extensional, rational, finitely branching trees, free on the finite power-set functor, or the theory of all binary, rational unordered trees, free on one commutative binary operation.

## Bibtex

@article{am_term, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius}, title = {Terminal Coalgebras and Free Iterative Theories}, journal = {Inform. and Comput.}, year = {2006}, volume = {204}, number = {7}, pages = {1139--1172}, }
How Iterative are Iterative Algebras
In: Proc. Coalgebraic Methods in Computer Science (CMCS'06),
Electron. Notes Theor. Comp. Sci., vol. 164, pp. 157-175.

## Abstract

Iterative algebras are defined by the property that every guarded system of recursive equations has a unique solution. We prove that they have a much stronger property: every system of recursive equations has a unique strict solution. And we characterize those systems that have a unique solution in every iterative algebra.

## Bibtex

@inproceedings{amv_how_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {How Iterative are Iterative Algebras}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'06)}, year = {2006}, series = {Electron. Notes Theor. Comp. Sci.}, volume = {164}, pages = {157--175}, }
The Category Theoretic Solution of Recursive Program Schemes
Theoret. Comput. Sci., vol. 366, pp. 3-59, 2006. Fundamental study; a corrigendum appeared in Theoret. Comput. Sci. 403 (2008), 409-415.

## Abstract

This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with “enough final coalgebras” we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme.

## Bibtex

@article{mm, author = {Stefan Milius and Lawrence S. Moss}, title = {The Category Theoretic Solution of Recursive Program Schemes}, journal = {Theoret. Comput. Sci.}, year = {2006}, volume = {366}, pages = {3--59}, }

## 2005

Iterative Algebras for a Base
In: Proc. Category Theory and Computer Science (CTCS'04),
Electron. Notes Theor. Comput.Sci., vol. 122, pp. 147-170.

## Abstract

For algebras A whose type is given by an endofunctor, iterativity means that every flat equation morphism in A has a unique solution. In our previous work we proved that every object generates a free iterative algebra, and we provided a coalgebraic construction of those free algebras. Iterativity w.r.t. an endofunctor was generalized by Tarmo Uustalu to iterativity w.r.t. a “base”, i.e., a functor of two variables yielding finitary monads in one variable. In the current paper we introduce iterative algebras in this general setting, and provide again a coalgebraic construction of free iterative algebras.

## Bibtex

@inproceedings{amv_base_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Iterative Algebras for a Base}, booktitle = {Proc. Category Theory and Computer Science (CTCS'04)}, year = {2005}, series = {Electron. Notes Theor. Comput.Sci.}, volume = {122}, pages = {147--170}, }
A General Final Coalgebra Theorem
Math. Structures Comput. Sci., vol. 15 (3), pp. 409-432, 2005. © Cambridge University Press.

## Abstract

By the Final Coalgebra Theorem of Aczel and Mendler, every endofunctor of the category of sets has a final coalgebra, which, however, may be a proper class. We generalise this to all ‘well-behaved’ categories K . The role of the category of classes is played by a free cocompletion K∞ of K under transfinite colimits, that is, colimits of ordinal-indexed chains. Every endofunctor F of K has a canonical extension to an endofunctor F∞ of K∞ which is proved to have a final coalgebra (and an initial algebra). Based on this, we prove a general solution theorem: for every endofunctor of a locally presentable category K all guarded equation-morphisms have unique solutions. The last result does not need the extension K∞: the solutions are always found within the category K .

## Bibtex

@article{amv_general, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {A General Final Coalgebra Theorem}, journal = {Math. Structures Comput. Sci.}, year = {2005}, volume = {15}, number = {3}, pages = {409--432}, }
Stefan Milius
Completely Iterative Algebras and Completely Iterative Monads
Inform. and Comput., vol. 196, pp. 1-41, 2005.

## Abstract

Completely iterative theories of Calvin Elgot formalize (potentially infinite) computations as solutions of recursive equations. One of the main results of Elgot and his coauthors is that infinite trees form a free completely iterative theory. Their algebraic proof of this result is extremely complicated. We present completely iterative algebras as a new approach to the description of free completely iterative theories. Examples of completely iterative algebras include algebras on complete metric spaces. It is shown that a functor admits an initial completely iterative algebra iff it has a final coalgebra. The monad given by free completely iterative algebras is proved to be the free completely iterative monad on the given endofunctor. This simplifies substantially all previous descriptions of these monads. Moreover, the new approach is much more general than the classical one of Elgot et al. A necessary and sufficient condition for the existence of a free completely iterative monad is proved.

## Bibtex

@article{m_cia, author = {Stefan Milius}, title = {Completely Iterative Algebras and Completely Iterative Monads}, journal = {Inform. and Comput.}, year = {2005}, volume = {196}, pages = {1--41}, }
The Category Theoretic Solution of Recursive Program Schemes
In: Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO'05),
Lecture Notes in Comput. Sci., vol. 3629, pp. 293-312.

## Abstract

This paper provides a general account of the notion of recursive program schemes, their uninterpreted and interpreted solutions, and related concepts. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with “enough final coalgebras” we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study recursion, e.g., substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes at all. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme. In this short version of our paper we can only sketch some proofs.

## Bibtex

@inproceedings{mm_abs, author = {Stefan Milius and Lawrence S. Moss}, title = {The Category Theoretic Solution of Recursive Program Schemes}, booktitle = {Proc. 1st Conference on Algebra and Coalgebra in Computer Science (CALCO'05)}, year = {2005}, series = {Lecture Notes in Comput. Sci.}, volume = {3629}, pages = {293--312}, }

## 2004

From Iterative Algebras to Iterative Theories
In: Proc. Coalgebraic Methods in Computer Science (CMCS'04),
Electron. Notes Theor. Comput. Sci., vol. 106, pp. 3-24.

## Abstract

Iterative theories introduced by Calvin Elgot formalize potentially infinite computations as solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with “iterative algebras”, i.e., algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. And our result is, nevertheless, much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category A. This allows us, e.g., to consider iterative algebras over any equationally specified class A of finitary algebras.

## Bibtex

@inproceedings{amv_mccoy_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {From Iterative Algebras to Iterative Theories}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'04)}, year = {2004}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {106}, pages = {3--24}, }
On coalgebra based on Classes
Theoret. Comput. Sci., vol. 316, pp. 3-23, 2004.

## Abstract

The category Class of classes and functions is proved to have a number of properties suitable for algebra and coalgebra: every endofunctor is set-based, it has an initial algebra and a terminal coalgebra, the categories of algebras and coalgebras are complete and cocomplete, and every endofunctor generates a free completely iterative monad. A description of a terminal coalgebra for the power-set functor is provided.

## Bibtex

@article{amv_classes, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On coalgebra based on Classes}, journal = {Theoret. Comput. Sci.}, year = {2004}, volume = {316}, pages = {3--23}, }

## 2003

Infinite Trees and Completely Iterative Theories: A Coalgebraic View
Theoret. Comput. Sci., vol. 300, pp. 1-45, 2003. Fundamental study.

## Abstract

Infinite trees form a free completely iterative theory over any given signature—this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(-) + X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees. This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H \tensor - + I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors.

## Bibtex

@article{aamv, author = {Peter Aczel and Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Infinite Trees and Completely Iterative Theories: A Coalgebraic View}, journal = {Theoret. Comput. Sci.}, year = {2003}, volume = {300}, pages = {1--45}, }
Some Remarks on Finitary and Iterative Monads
Appl. Categ. Structures, vol. 11 (6), pp. 521-541, 2003.

## Abstract

For every locally finitely presentable category A we introduce finitary Kleisli triples on A and show that they bijectively correspond to finitary monads on A. We illustrate this on free monads and free iterative monads.

## Bibtex

@article{amv_finkleisli, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Some Remarks on Finitary and Iterative Monads}, journal = {Appl. Categ. Structures}, year = {2003}, volume = {11}, number = {6}, pages = {521--541}, }
Free Iterative Theories: a coalgebraic view
Math. Structures Comput. Sci., vol. 13 (2), pp. 259-320, 2003. © Cambridge University Press.

## Abstract

Every finitary endofunctor of Set is proved to generate a free iterative theory in the sense of Elgot. This work is based on coalgebras, specifically on parametric corecursion, and the proof is presented for categories more general than just Set.

## Bibtex

@article{amv_62, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Free Iterative Theories: a coalgebraic view}, journal = {Math. Structures Comput. Sci.}, year = {2003}, volume = {13}, number = {2}, pages = {259--320}, }
Stefan Milius
On Colimits in Categories of Relations
Appl. Categ. Structures, vol. 11 (3), pp. 287-312, 2003.

## Abstract

We study (finite) coproducts and colimits of omega-chains in Rel(C), the 2-category of relations over a given category C. The former exist and are "the same" as in C provided that C is extensive. The latter do not exist for example in Rel(Set). However, the canonical construction of those colimits in the category of sets can be generalized to Rel(Set). The canonical cocone is shown to satisfy a 2-categorical universal property, namely that of an lax adjoint cooplimit. Sufficient conditions for any base category C to admit the construction are given. A necessary and sufficient condition for the construction to yield colimits of omega-chains in the category of maps of Rel(C) is also given.

## Bibtex

@article{m_rel, author = {Stefan Milius}, title = {On Colimits in Categories of Relations}, journal = {Appl. Categ. Structures}, year = {2003}, volume = {11}, number = {3}, pages = {287--312}, }

## 2002

On Rational Monads and Free Iterative Theories
In: Proc. Category Theory and Computer Science (CTCS'02),
Electron. Notes Theor. Comput. Sci., vol. 69, pp. 23-46.

## Abstract

For every finitary endofunctor H of Set a rational algebraic theory (or a rational finitary monad) R is defined by means of solving all finitary flat systems of recursive equations over H. This generalizes the result of Elgot and his coauthors, describing a free iterative theory of a polynomial endofunctor H as the theory R of all rational infinite trees. We present a coalgebraic proof that R is a free iterative theory on H for every finitary endofunctor H, which is substantially simpler than the previous proof by Elgot et al., as well as our previous proof. This result holds for more general categories than Set.

## Bibtex

@inproceedings{amv_62_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {On Rational Monads and Free Iterative Theories}, booktitle = {Proc. Category Theory and Computer Science (CTCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {69}, pages = {23--46}, }
Stefan Milius
On Iteratable Endofunctors
In: Proc. Category Theory and Computer Science (CTCS'02),
Electron. Notes Theor. Comput. Sci., vol. 69, pp. 287-304.

## Abstract

Completely iterative monads of Elgot et al. are the monads such that every guarded iterative equation has a unique solution. Free completely iterative monads are known to exist on every iteratable endofunctor H, i.e., one with final coalgebras of all functors H(-) + X. We show that conversely, if H generates a free completely iterative monad, then it is iteratable.

## Bibtex

@inproceedings{m_iter_abs, author = {Stefan Milius}, title = {On Iteratable Endofunctors}, booktitle = {Proc. Category Theory and Computer Science (CTCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {69}, pages = {287--304}, }
Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors
In: Proc. Coalgebraic Methods in Computer Science (CMCS'02),
Electron. Notes Theor. Comput. Sci., vol. 65, pp. 1-28.

## Abstract

Every endofunctor F of Set has an initial algebra and a final coalgebra, but they are classes in general. Consequently, the endofunctor F∞ of the category of classes that F induces generates a completely iterative monad T. And solutions of arbitrary guarded systems of iterative equations w.r.t. F exist, and can be found in naturally defined subsets of the classes TY. More generally, starting from any category K, we can form a free cocompletion K∞ of K under small-filtered colimits (e.g., Set∞ is the category of classes), and we give sufficient conditions to obtain analogous results for arbitrary endofunctors of K.

@inproceedings{amv_general_abs, author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil}, title = {Final Coalgebras And a Solution Theorem for Arbitrary Endofunctors}, booktitle = {Proc. Coalgebraic Methods in Computer Science (CMCS'02)}, year = {2002}, series = {Electron. Notes Theor. Comput. Sci.}, volume = {65}, pages = {1--28}, }`