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 ()

Click on titles to see abstracts and pdf's.

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

In:
Proc. 7th International Conference on Formal Structures for Computation and Deduction
(FSCD 2022),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
??,
pp.
??,
to appear.

*stateful SOS* rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the *cool* GSOS formats of Bloom and van Glabbeek, we obtain the *streamlined* and *cool* stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

```
@inproceedings{gmstu22,
```

author = {Sergey Goncharov and Stefan Milius and Lutz Schr\"oder and Stelios Tsampas and Henning Urbat},

title = {Stateful Structural Operational Semantics},

booktitle = {Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},

year = {2022},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {??},

pages = {??},

}

In:
Proc. 37th Annual Symposium on Logic in Computer Science
(LICS 2022),
to appear.

*graded semantics*uses graded monads to capture behavioural equivalences of varying granularity, for example as found on the linear-time/branching-time spectrum, over general system types. We describe a generic Spoiler-Duplicator game for graded semantics that is extracted from the given graded monad, and may be seen as playing out an equational proof; instances include standard pebble games for simulation and bisimulation as well as games for trace-like equivalences and coalgebraic behavioural equivalence. Considerations on an infinite variant of such games lead to a novel notion of *infinite-depth graded semantics*. Under reasonable restrictions, the infinite-depth graded semantics associated to a given graded equivalence can be characterized in terms of a determinization construction for coalgebras under the equivalence at hand.

```
@inproceedings{fbkms22,
```

author = {Chase Ford and Harsh Beohar and Barbara K\"onig and Stefan Milius and Lutz Schr\"oder},

title = {Graded Monads and Behavioural Equivalence Games},

booktitle = {Proc. 37th Annual Symposium on Logic in Computer Science (LICS 2022)},

year = {2022},

pages = {},

}

In:
Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
(TACAS 2022),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
13244,
pp.
159-177.

```
@inproceedings{bdm22,
```

author = {Fabian Birkmann and Hans-Peter Deifel and Stefan Milius},

title = {Distributed Coalgebraic Partition Refinement},

booktitle = {Proc. 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022)},

year = {2022},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {13244},

pages = {159--177},

}

In:
Proc. Fifteenth International Workshop on Coalgebraic Methods in Computer Science
(CMCS 2022),

*Lecture Notes Comput. Sci.*,
vol.
??,
pp.
??,
to appear.

```
@inproceedings{fmu22,
```

author = {Florian Frank and Stefan Milius and Henning Urbat},

title = {Coalgebraic Semantics for Nominal Automata},

booktitle = {Proc. Fifteenth International Workshop on Coalgebraic Methods in Computer Science (CMCS 2022)},

year = {2022},

series = {Lecture Notes Comput. Sci.},

volume = {??},

pages = {??},

}

```
@article{afms21,
```

author = {Ji\v{r}\'i Ad\'amek and Chase Ford and Stefan Milius and Lutz Schr\"oder},

title = {Finitary Monads on the Category of Posets},

journal = {Math. Structures Comput. Sci.},

year = {2021},

volume = {31},

number = {Special Issue in honor of John Power},

pages = {799--821},

}

In:
Proc. 9th Conference on Algebra and Coalgebra in Computer Science
(CALCO 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
211,
pp.
14:1-14:17.

```
@inproceedings{fms21-2,
```

author = {Chase Ford and Stefan Milius and Lutz Schr\"oder},

title = {Monads on Categories of Relational Structures},

booktitle = {Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {211},

pages = {14:1--14:17},

}

In:
Proc. 9th Conference on Algebra and Coalgebra in Computer Science
(CALCO 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
211,
pp.
5:1-5:20.

```
@inproceedings{amm21,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},

title = {Initial algebras without iteration},

booktitle = {Proc. 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {211},

pages = {5:1--5:20},

}

```
@article{amu21,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {On the behaviour of coalgebras with side effects and algebras with effectful iteration},

journal = {J. Logic Comput.},

year = {2021},

volume = {31},

number = {6},

pages = {1429--1481},

}

In:
Proc. 32nd International Conference on Concurrency Theory
(CONCUR 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
203,
pp.
32:1-32:18.

```
@inproceedings{wms21,
```

author = {Thorsten Wißmann and Stefan Milius and Lutz Schr\"oder},

title = {Explaining Behavioural Inequivalence Generically in Quasilinear Time},

booktitle = {Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {203},

pages = {32:1--32:18},

}

In:
Proc. 32nd International Conference on Concurrency Theory
(CONCUR 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
203,
pp.
4:1-4:16.

*infinite bar strings*, i.e.~infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce *regular nominal nondeterministic Büchi automata* (*Büchi RNNAs*), an automata model for languages of infinite bar strings, repurposing the previously introduced *RNNAs* over finite bar strings. Our machines feature explicit binding (i.e.~resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.

```
@inproceedings{uhms21,
```

author = {Henning Urbat and Daniel Hausmann and Stefan Milius and Lutz Schr\"oder},

title = {Nominal Büchi Automata with Name Allocation},

booktitle = {Proc. 32nd International Conference on Concurrency Theory (CONCUR 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {203},

pages = {4:1--4:16},

}

In:
Proc. 46th International Symposium on Mathematical Foundations of Computer Science
(MFCS 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
202,
pp.
58:1-58:18.

*Name-binding* nominal automata models such as *regular nondeterministic nominal automata (RNNAs)* have been shown to be computationally more tractable. In the present paper, we introduce a linear-time fixpoint logic Bar-µTL for finite words over an infinite alphabet, which features full negation and freeze quantification via name binding. We show by a nontrivial reduction to *extended regular nondeterministic nominal automata* that even though Bar-µTL allows unrestricted nondeterminism and unboundedly many registers, model checking Bar-µTL over RNNAs and satisfiability checking both have elementary complexity. For example, model checking is in 2ExpSpace, more precisely in parametrized ExpSpace, effectively with the number of registers as the parameter.

```
@inproceedings{hms21,
```

author = {Daniel Hausmann and Stefan Milius and Lutz Schr\"oder},

title = {A Linear-Time Nominal mu-Calculus with Name Allocation},

booktitle = {Proc. 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {202},

pages = {58:1--58:18},

}

```
@article{acmu21,
```

author = {Ji\v{r}\'i Ad\'amek and Liang-Ting Chen and Stefan Milius and Henning Urbat},

title = {Reiterman's Theorem on Finite Algebras for a Monad},

journal = {ACM Trans. Comput. Log.},

year = {2021},

volume = {22},

number = {4:23},

pages = {1--48},

}

In:
Proc. 36th Annual Symposium on Logic in Computer Science
(LICS 2021).

```
@inproceedings{fms21,
```

author = {Chase Ford and Stefan Milius and Lutz Schr\"oder},

title = {Behavioural Preorders via Graded Monads},

booktitle = {Proc. 36th Annual Symposium on Logic in Computer Science (LICS 2021)},

year = {2021},

pages = {},

}

In:
Proc. 6th International Conference on Formal Structures for Computation and Deduction
(FSCD 2021),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
195,
pp.
28:1-28:19.

```
@inproceedings{dmw21,
```

author = {Hans-Peter Deifel and Stefan Milius and Thorsten Wißmann},

title = {Coalgebra Encoding for Efficient Minimization},

booktitle = {Proc. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},

year = {2021},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {195},

pages = {28:1--28:19},

}

```
@article{wdms21,
```

author = {Thorsten Wißmann and Hans-Peter Deifel and Stefan Milius and Lutz Schr\"oder},

title = {From Generic Partition Refinement to Weighted Tree Automata Minimization},

journal = {Form. Asp. Comput.},

year = {2021},

volume = {30},

pages = {695--727},

}

In:
Proc. 24th International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS 2021),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
12650,
pp.
448--468.

*nondeterministic syntactic complexity*. It is the least degree of any extension of the `canonical boolean representation' of the syntactic monoid. Equivalently, it is the least number of states of any *subatomic* nondeterministic acceptor. It turns out that essentially all previous structural work on nondeterministic state-minimality computes this measure. Our approach rests on an algebraic interpretation of nondeterministic finite automata as deterministic finite automata endowed with semilattice structure. Crucially, the latter form a self-dual category.

```
@inproceedings{mmu21,
```

author = {Rob Myers and Stefan Milius and Henning Urbat},

title = {Nondeterministic Syntactic Complexity},

booktitle = {Proc. 24th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2021)},

year = {2021},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {12650},

pages = {448----468},

}

In:
Proc. 15th International Conference on Language and Automata Theory and Applications
(LATA 2021),

*Lecture Notes Comput. Sci.*,
vol.
12638,
pp.
3--15.

*basic varieties of regular languages*, a weakening of Eilenberg's original concept that does not require closure under any boolean operations, and prove a variety theorem for them. To do so, we investigate the algebraic recognition of languages by *lattice bimodules*, generalizing Klíma and Polák's lattice algebras, and we utilize the duality between algebraic completely distributive lattices and posets.

```
@inproceedings{bmu21,
```

author = {Fabian Birkmann and Stefan Milius and Henning Urbat},

title = {On Language Varieties Without Boolean Operations},

booktitle = {Proc. 15th International Conference on Language and Automata Theory and Applications (LATA 2021)},

year = {2021},

series = {Lecture Notes Comput. Sci.},

volume = {12638},

pages = {3----15},

}

In:
Proc. 20th Annual DFRWS USA
(DFRWS 2020 USA),

*Forensic Science International: Digital Investigation*,
vol.
33,
article 301006.

*metadata-based* reconstruction techniques that interpret metadata structures to precisely reconstruct upper layer content. On the other hand, there are *pattern-based* techniques (*carving*) that focus mainly on deleted files that cannot be reconstructed by other methods. Instances resembling the former approach are Carrier's *The Sleuth Kit* (TSK) as well as many commercial tools, while the latter approach is used by file carvers like Foremost and Scalpel. Based on a formalization of storage abstraction layers, we show that all these techniques can be unified within a modular reconstruction framework. We define composition operators that allow to precisely express complex reconstruction tasks that involve both metadata-based and pattern-based techniques and allow to combine their respective strengths seamlessly in forensic analysis. We present LAYR, an implementation of our approach and show that it can automatically and reliably combine different reconstruction approaches.

```
@inproceedings{sdmf20,
```

author = {Janine Schneider and Hans-Peter Deifel and Stefan Milius and Felix Freiling},

title = {Unifying Metadata-Based Storage Reconstruction and Carving with LAYR},

booktitle = {Proc. 20th Annual DFRWS USA (DFRWS 2020 USA)},

year = {2020},

series = {Forensic Science International: Digital Investigation},

volume = {33},

pages = {},

}

```
@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},

}

*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.

```
@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 = {2020},

volume = {271},

pages = {104456},

}

In:
Proc. 23rd International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS 2020),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
12077,
pp.
17-36.

```
@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 2020)},

year = {2020},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {12077},

pages = {17--36},

}

**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.

```
@article{gms20,
```

author = {Sergey Goncharov and Stefan Milius and Alexandra Silva},

title = {Towards a Uniform Theory of Effectful State Machines},

journal = {ACM Trans. Comput. Log.},

year = {2020},

volume = {21},

number = {3:23},

pages = {63},

}

```
@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},

}

```
@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},

}

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.

```
@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},

}

In:
Proc. International Symposium on Formal Methods
(FM 2019),

*Lecture Notes Comput. Sci.*,
vol.
11800,
pp.
280-297.

```
@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 2019)},

year = {2019},

series = {Lecture Notes Comput. Sci.},

volume = {11800},

pages = {280--297},

}

In:
Proc. 30th International Conference on Concurrency Theory
(CONCUR 2019),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
140,
pp.
36:1-36:16.

*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.

```
@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 2019)},

year = {2019},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {140},

pages = {36:1--36:16},

}

```
@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 = {},

}

In:
Proc. 46th International Colloquium on Automata, Languages, and Programming
(ICALP 2019),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
132,
pp.
130:1--130:14.

```
@inproceedings{um19,
```

author = {Stefan Milius and Henning Urbat},

title = {Varieties of Data Languages},

booktitle = {Proc. 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},

year = {2019},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {132},

pages = {130:1----130:14},

}

In:
Proc. 22nd International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS 2019),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
11425,
pp.
400-417.

```
@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 2019)},

year = {2019},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {11425},

pages = {400--417},

}

```
@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},

}

```
@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},

}

```
@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 = {},

}

```
@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.},

}

In:
Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science
(CMCS'18),

*Lecture Notes Comput. Sci.*,
vol.
11202,
pp.
56-77.

```
@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},

}

In:
Proc. Thirteenth International Workshop on Coalgebraic Methods in Computer Science
(CMCS'18),

*Lecture Notes Comput. Sci.*,
vol.
11202,
pp.
144-166.

```
@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},

}

```
@article{amu18,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {A Categorical Approach to Syntactic Monoids},

journal = {Log. Methods Comput. Sci.},

year = {2018},

volume = {14},

number = {2:9},

pages = {34 pp.},

}

```
@article{amm18,
```

author = {Ji\v{r}\'i Ad\'amek and Lawrence S. Moss and Stefan Milius},

title = {Fixed Points of Functors},

journal = {J. Log. Algebr. Methods Program.},

year = {2018},

volume = {95},

pages = {41--81},

}

In:
Proc. Formal Methods in Computer Aided Design
(FMCAD'17),
pp.
196-203.

```
@inproceedings{ddglms17,
```

author = {Hans-Peter Deifel and Christian Dietrich and Merlin G\"ottlinger and Daniel Lohmann and Stefan Milius and Lutz Schr\"oder},

title = {Automatic Verification of Application-Tailored OSEK Kernels},

booktitle = {Proc. Formal Methods in Computer Aided Design (FMCAD'17)},

year = {2017},

pages = {196--203},

}

In:
Proc. 28th International Conference on Concurrency Theory
(CONCUR 2017),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
85,
pp.
28:1-28:16.

```
@inproceedings{dmsw17,
```

author = {Ulrich Dorsch and Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann},

title = {Efficient coalgebraic partition refinement},

booktitle = {Proc. 28th International Conference on Concurrency Theory (CONCUR 2017)},

year = {2017},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {85},

pages = {28:1--28:16},

}

In:
Proc. 42nd International Symposium on Mathematical Foundations of Computer Science
(MFCS'17),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
83,
pp.
43:1-43:15,
EATCS Best Paper Award.

```
@inproceedings{amu17,
```

author = {Henning Urbat and Ji\v{r}\'i Ad\'amek and Liang-Ting Chen and Stefan Milius},

title = {Eilenberg Theorems For Free},

booktitle = {Proc. 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS'17)},

year = {2017},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {83},

pages = {43:1--43:15},

}

In:
Proc. 7th Conference on Algebra and Coalgebra in Computer Science
(CALCO 2017),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
72,
pp.
18:1-18:15.

```
@inproceedings{milius17,
```

author = {Stefan Milius},

title = {Proper Functors and their Rational Fixed Point},

booktitle = {Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},

year = {2017},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {72},

pages = {18:1--18:15},

}

In:
Proc. 7th Conference on Algebra and Coalgebra in Computer Science
(CALCO'17),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
72,
pp.
3:1-3:15.

```
@inproceedings{am17,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius},

title = {On Corecursive Algebras for Functors Preserving Coproducts},

booktitle = {Proc. 7th Conference on Algebra and Coalgebra in Computer Science (CALCO'17)},

year = {2017},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {72},

pages = {3:1--3:15},

}

```
@article{amv17,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil},

title = {A presentation of bases for parametrized iterativity},

journal = {Theory Appl. Categ.},

year = {2017},

volume = {32},

number = {19},

pages = {682--718},

}

In:
Proc. 20th International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS'17),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
10203,
pp.
124-142.

```
@inproceedings{skmw17,
```

author = {Lutz Schr\"oder and Dexter Kozen and Stefan Milius and Thorsten Wißmann},

title = {Nominal automata with name binding},

booktitle = {Proc. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17)},

year = {2017},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {10203},

pages = {124--142},

}

```
@article{ml17,
```

author = {Stefan Milius and Tadeusz Litak},

title = {Guard your daggers and traces: Properties of guarded (co-)recursion},

journal = {Fund. Inform.},

year = {2017},

volume = {150},

number = {3-4},

pages = {407--449},

}

In:
Proc. International Conference on Information Systems Security
(ICISS'16),

*Lecture Notes Comput. Sci.*,
vol.
10063,
pp.
3-22.

```
@inproceedings{tsm16,
```

author = {Kristof Teichel and Dieter Sibold and Stefan Milius},

title = { An attack possibility on time synchronization protocols secured with TESLA-like mechanisms},

booktitle = {Proc. International Conference on Information Systems Security (ICISS'16)},

year = {2016},

series = {Lecture Notes Comput. Sci.},

volume = {10063},

pages = {3--22},

}

In:
Proc. 32nd Conference on Mathematical Foundations of Programming Science
(MFPS XXXII),

*Electron. Notes Theor. Comput. Sci.*,
vol.
325,
pp.
147-168.

```
@inproceedings{gmr16,
```

author = {Sergey Goncharov and Stefan Milius and Christoph Rauch},

title = {Complete Elgot monads and coalgebraic resumptions},

booktitle = {Proc. 32nd Conference on Mathematical Foundations of Programming Science (MFPS XXXII)},

year = {2016},

series = {Electron. Notes Theor. Comput. Sci.},

volume = {325},

pages = {147--168},

}

```
@article{msw16,
```

author = {Stefan Milius and Lutz Schr\"oder and Thorsten Wißmann},

title = {Regular Behaviours with Names: On Rational Fixpoints of Endofunctors on Nominal Sets},

journal = {Appl. Categ. Structures},

year = {2016},

volume = {24},

number = {5},

pages = {663--701},

}

In:
Proc. 19th International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS'16),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
9634,
pp.
107-125.

*locally finite fixpoint}* (LFF). We prove that if the given endofunctor preserves monomorphisms then the LFF always exists and is a subcoalgebra of the final coalgebra (unlike the rational fixpoint previously studied by Adámek, Milius and Velebil). 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. And we obtain a number of new examples, e.g.~(realtime deterministic resp.~non-deterministic) context-free languages, constructively $S$-algebraic formal power-series (and any other instance of the generalized powerset construction by Silva, Bonchi, Bonsangue, and Rutten) and the monad of Courcelle's algebraic
trees.

```
@inproceedings{mpw16,
```

author = {Stefan Milius and Dirk Pattinson and Thorsten Wißmann},

title = {A New Foundation for Finitary Corecursion: The Locally Finite Fixpoint and its Properties},

booktitle = {Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16)},

year = {2016},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {9634},

pages = {107--125},

}

In:
Proc. 19th International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS'16),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
9634,
pp.
531-547.

```
@inproceedings{acmu16,
```

author = {Liang-Ting Chen and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {Profinite Monads, Profinite Equationa and Reitermann's Theorem},

booktitle = {Proc. 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'16)},

year = {2016},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {9634},

pages = {531--547},

}

```
@proceedings{ah15,
```

editor = {Reiko Heckel and Stefan Milius},

title = {Special Issue with Selected Papers of the 5th International Conference on Algebra and Coalgebra in Computer Science, CALCO 2013},

publisher = {},

series = {Logical Methods in Computer Science},

year = {2015},

volume = {},

number = {},

pages = {},

}

In:
Proc. 2nd International Conference on Research in Security Standardization
(SSR'15),

*Lecture Notes Comput. Sci.*,
vol.
9497,
pp.
218-245.

```
@inproceedings{tsm15,
```

author = {Kristof Teichel and Dieter Sibold and Stefan Milius},

title = { First results of a formal analysis of the network time security specification},

booktitle = {Proc. 2nd International Conference on Research in Security Standardization (SSR'15)},

year = {2015},

series = {Lecture Notes Comput. Sci.},

volume = {9497},

pages = {218--245},

}

```
@article{mamu15,
```

author = {Rob Myers and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {Coalgebraic Constructions of Canonical Nondeterministic Automata},

journal = {Theoret. Comput. Sci.},

year = {2015},

volume = {604},

pages = {81--101},

}

```
@article{amms14,
```

author = {Ji\v{r}\'i Ad\'amek and Paul B. Levy and Stefan Milius and Lawrence S. Moss and Lurdes Sousa},

title = {On Final Coalgebras of Power-Set Functors and Saturated Trees},

journal = {Appl. Categ. Structures},

year = {2015},

volume = {23},

number = {4},

pages = {609--641},

}

```
@article{bmsz15,
```

author = {Filippo Bonchi and Stefan Milius and Alexandra Silva and Fabio Zanasi},

title = {Killing Epsilons with a Dagger: A Coalgebraic Study of Systems with Algebraic Label Structure},

journal = {Theoret. Comput. Sci.},

year = {2015},

volume = {604},

pages = {102--126},

}

In:
Proc. 6th Conference on Algebra and Coalgebra in Computer Science
(CALCO'15),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
35,
pp.
1-16,
CALCO Best Paper Award.

```
@inproceedings{amu15,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {Syntactic Monoids in a Category},

booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)},

year = {2015},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {35},

pages = {1--16},

}

In:
Proc. 6th Conference on Algebra and Coalgebra in Computer Science
(CALCO'15),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
35,
pp.
336-351.

```
@inproceedings{mw15,
```

author = {Stefan Milius and Thorsten Wißmann},

title = {Finitary Corecursion for the Infinitary Lambda Calculus},

booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)},

year = {2015},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {35},

pages = {336--351},

}

In:
Proc. 6th Conference on Algebra and Coalgebra in Computer Science
(CALCO'15),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
35,
pp.
253-269.

```
@inproceedings{mps15,
```

author = {Stefan Milius and Dirk Pattinson and Lutz Schr\"oder},

title = {Generic Trace Semantics and Graded Monads},

booktitle = {Proc. 6th Conference on Algebra and Coalgebra in Computer Science (CALCO'15)},

year = {2015},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {35},

pages = {253--269},

}

In:
Proc. 30th Annual Symposium on Logic in Computer Science
(LICS 2015),
pp.
414-425.

```
@inproceedings{ammu15,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat},

title = {Varieties of Languages in a Category},

booktitle = {Proc. 30th Annual Symposium on Logic in Computer Science (LICS 2015)},

year = {2015},

pages = {414--425},

}

In:
Software, Services, and Systems: Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of Programming and Software Engineering,

*Lecture Notes Comput. Sci.*,
vol.
8950,
pp.
75-90.

```
@inproceedings{,
```

author = {Alexander Kurz and Stefan Milius and Dirk Pattinson and Lutz Schr\"oder},

title = {Simplified Coalgebraic Trace Equivalence},

booktitle = {Software, Services, and Systems: Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of Programming and Software Engineering},

year = {2015},

series = {Lecture Notes Comput. Sci.},

volume = {8950},

pages = {75--90},

}

```
@article{ammu14,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Henning Urbat},

title = {On Finitary Functors and Their Presentations},

journal = {J. Comput. System Sci.},

year = {2015},

volume = {81},

number = {5},

pages = {813--833},

}

In:
Proc. 30th Conference on Mathematical Foundations of Programming Science
(MFPS XXX),

*Electron. Notes Theor. Comput. Sci.*,
vol.
308,
pp.
3-23.

```
@inproceedings{ammu14_2,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat},

title = {On Continuous Nondeterminism and State Minimality},

booktitle = {Proc. 30th Conference on Mathematical Foundations of Programming Science (MFPS XXX)},

year = {2014},

series = {Electron. Notes Theor. Comput. Sci.},

volume = {308},

pages = {3--23},

}

```
@article{ahm14,
```

author = {Ji\v{r}\'i Ad\'amek and Mahdieh Haddadi and Stefan Milius},

title = {Corecursive Algebras, Corecursive Monads and Bloom Monads},

journal = {Log. Methods Comput. Sci.},

year = {2014},

volume = {10},

number = {3:19},

pages = {51 pp.},

}

In:
Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science
(TCS'14),

*Lecture Notes Comput. Sci.*,
vol.
8705,
pp.
265-280.

*generalized powerset construction* to define a generic (trace) semantics for $\BBT$-automata, and we show by numerous examples that it correctly instantiates for some known classes of machines/languages captured by the Chomsky hierarchy. Moreover, our approach provides new generic techniques for studying expressivity power of various machine-based models.

```
@inproceedings{gms14,
```

author = {Sergey Goncharov and Stefan Milius and Alexandra Silva},

title = {Towards a Coalgebraic Chomsky Hierarchy (Extended Abstract)},

booktitle = {Proc. 8th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (TCS'14)},

year = {2014},

series = {Lecture Notes Comput. Sci.},

volume = {8705},

pages = {265--280},

}

In:
Proc. 19th International Workshop on Formal Methods for Industrial Critical Systems
(FMICS'14),

*Lecture Notes Comput. Sci.*,
vol.
6959,
pp.
124-139.

```
@inproceedings{bhmg14,
```

author = {Henning Basold and Michaela Huhn and Stefan Milius and Henning G\"unther},

title = {An Open Alternative for SMT-based Verification of SCADE Models},

booktitle = {Proc. 19th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'14)},

year = {2014},

series = {Lecture Notes Comput. Sci.},

volume = {6959},

pages = {124--139},

}

```
@article{amv14,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil},

title = {Base modules for parametrized iterativity},

journal = {Theoret. Comput. Sci.},

year = {2014},

volume = {523},

pages = {56--85},

}

In:
Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science
(CMCS'14),

*Lecture Notes Comput. Sci.*,
vol.
8446,
pp.
189-210.

```
@inproceedings{mamu14,
```

author = {Rob Myers and Ji\v{r}\'i Ad\'amek and Stefan Milius and Henning Urbat},

title = {Canonical Nondeterministic Automata},

booktitle = {Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14)},

year = {2014},

series = {Lecture Notes Comput. Sci.},

volume = {8446},

pages = {189--210},

}

In:
Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science
(CMCS'14),

*Lecture Notes Comput. Sci.*,
vol.
8446,
pp.
53-74.

```
@inproceedings{bmsz14,
```

author = {Filippo Bonchi and Stefan Milius and Alexandra Silva and Fabio Zanasi},

title = {How to Kill Epsilons With a Dagger: A Coalgebraic Take on Systems with Algebraic Label Structure},

booktitle = {Proc. Twelfth International Workshop on Coalgebraic Methods in Computer Science (CMCS'14)},

year = {2014},

series = {Lecture Notes Comput. Sci.},

volume = {8446},

pages = {53--74},

}

In:
Proc. Seventeenth International Conference on Foundations of Software Science and Computation Structures
(FoSSaCS'14),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
8412,
pp.
366-380.

```
@inproceedings{ammu14_3,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Rob Myers and Henning Urbat},

title = {Generalized Eilenberg Theorem I: Local Varieties of Languages},

booktitle = {Proc. Seventeenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'14)},

year = {2014},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {8412},

pages = {366--380},

}

```
@article{hm14,
```

author = {Michaela Huhn and Stefan Milius},

title = {Observations on Formal Safety Analysis in Industrial Practice},

journal = {Sci. Comput. Programming},

year = {2014},

volume = {80A},

number = {Part A},

pages = {150--168},

}

```
@proceedings{calco13,
```

editor = {Reiko Heckel and Stefan Milius},

title = {Algebra and Coalgebra in Computer Science: 5th International Conference, CALCO 2013 (Proceedings)},

publisher = {Springer},

series = {Lecture Notes in Computer Science},

year = {2013},

volume = {8089},

number = {},

pages = {},

}

In:
Proc. Fixed Points in Computer Science
(FICS'13),

*Electron. Proc. Theoret. Comput. Sci.*,
vol.
126,
pp.
72-86.

```
@inproceedings{ml13,
```

author = {Stefan Milius and Tadeusz Litak},

title = {Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion},

booktitle = {Proc. Fixed Points in Computer Science (FICS'13)},

year = {2013},

series = {Electron. Proc. Theoret. Comput. Sci.},

volume = {126},

pages = {72--86},

}

In:
Proc. 29th Conference on Mathematical Foundations of Programming Science
(MFPS XXIX),

*Electron. Notes Theor. Comput. Sci.*,
vol.
298,
pp.
257-282.

```
@inproceedings{mbmr13,
```

author = {Stefan Milius and Marcello Bonsangue and Rob Myers and Jurriaan Rot},

title = {Rational Operational Models},

booktitle = {Proc. 29th Conference on Mathematical Foundations of Programming Science (MFPS XXIX)},

year = {2013},

series = {Electron. Notes Theor. Comput. Sci.},

volume = {298},

pages = {257--282},

}

*abstract GSOS rules* l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial *completely iterative algebras* (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle *modularity*. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.

```
@article{mms13,
```

author = {Stefan Milius and Lawrence S. Moss and Daniel Schwencke},

title = {Abstract GSOS rules and a Modular Treatment of Recursive Definitions},

journal = {Log. Methods Comput. Sci.},

year = {2013},

volume = {9},

number = {3:28},

pages = {52 pp.},

}

```
@article{amms13,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Lurdes Sousa},

title = {Well-pointed Coalgebras},

journal = {Log. Methods Comput. Sci.},

year = {2013},

volume = {9},

number = {3:2},

pages = {51 pp.},

}

```
@article{amv_refl2_13,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Ji\v{r}\'i Velebil},

title = {How iterative reflections of monads are constructed},

journal = {Inform. and Comput.},

year = {2013},

volume = {225},

pages = {83--118},

}

```
@article{bms13,
```

author = {Marcello Bonsangue and Stefan Milius and Alexandra Silva},

title = {Sound and complete axiomatizations of coalgebraic language equivalence},

journal = {ACM Trans. Comput. Log.},

year = {2013},

volume = {14},

number = {1:7},

pages = {52 pp.},

}

In:
Proc. 31st International Conference on Computer Safety, Reliability and Security
(SafeComp'12),

*Lecture Notes Comput. Sci.*,
vol.
7612,
pp.
291-304.

```
@inproceedings{gmm12,
```

author = {Henning G\"unther and Stefan Milius and M. Oliver M\"oller},

title = {On the Formal Verification of Systems of Synchronous Software Components},

booktitle = {Proc. 31st International Conference on Computer Safety, Reliability and Security (SafeComp'12)},

year = {2012},

series = {Lecture Notes Comput. Sci.},

volume = {7612},

pages = {291--304},

}

In:
Proc. Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics
(EXPRESS/SOS'12),

*Electron. Proc. Theoret. Comput. Sci.*,
vol.
89,
pp.
3-18.

*rational fixpoint* of a functor, which captures the behaviour of \emph{finite} systems. In other words, we show that rational behaviour is closed under operations specified in our format. As applications we consider operations on regular languages, regular processes and finite weighted transition systems.

```
@inproceedings{bmr12,
```

author = {Marcello Bonsangue and Stefan Milius and Jurriaan Rot},

title = {On the specification of operations on the rational behaviour of systems},

booktitle = {Proc. Combined 19th International Workshop on Expressiveness in Concurrency and 9th Workshop on Structural Operational Semantics (EXPRESS/SOS'12)},

year = {2012},

series = {Electron. Proc. Theoret. Comput. Sci.},

volume = {89},

pages = {3--18},

}

In:
Proc. 27th Annual Symposium on Logic in Computer Science
(LICS'12),
pp.
45-54.

Two consistent monads have a coproduct iff either they have arbitrarily large common fixpoints, or one is an exception monad, possibly modified to preserve the empty set. Hence a consistent monad has a coproduct with every monad iff it is an exception monad, possibly modified to preserve the empty set. We also show other fixpoint results, including that a functor (not constant on nonempty sets) is finitary iff every sufficiently large cardinal is a fixpoint.

```
@inproceedings{ablm12,
```

author = {Ji\v{r}\'i Ad\'amek and Nathan Bowler and Paul B. Levy and Stefan Milius},

title = {Coproducts of Monads on Set},

booktitle = {Proc. 27th Annual Symposium on Logic in Computer Science (LICS'12)},

year = {2012},

pages = {45--54},

}

In:
Proc. Eleventh International Workshop on Coalgebraic Methods in Computer Science
(CMCS'12),

*Lecture Notes Comput. Sci.*,
vol.
7399,
pp.
51-70.

```
@inproceedings{amm12,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},

title = {On Finitary Functors and Their Presentations},

booktitle = {Proc. Eleventh International Workshop on Coalgebraic Methods in Computer Science (CMCS'12)},

year = {2012},

series = {Lecture Notes Comput. Sci.},

volume = {7399},

pages = {51--70},

}

In:
Proc. Fifteenth International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS'12),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
7213,
pp.
58-73.

*factorization structures*, there exists an abstract procedure for equivalence checking. Then, we consider coalgebras in categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with *reflections*. This transformation can be thought of as some kind of determinization. We will apply our theory to the following examples: conditional transition systems and (non-deterministic) automata.

```
@inproceedings{ABHKMS12,
```

author = {Ji\v{r}\'i Ad\'amek and Filippo Bonchi and Mathias H\"ulsbusch and Barbara K\"onig and Stefan Milius and Alexandra Silva},

title = {A coalgebraic perspective on minimization and determinization},

booktitle = {Proc. Fifteenth International Conference on
Foundations of Software Science and Computation Structures (FoSSaCS'12)},

year = {2012},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {7213},

pages = {58--73},

}

In:
Proc. Fifteenth International Conference on
Foundations of Software Science and Computation Structures
(FoSSaCS'12),

*Lecture Notes Comput. Sci. (ARCoSS)*,
vol.
7213,
pp.
89-103.

```
@inproceedings{amms12,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss and Lurdes Sousa},

title = {Well-pointed Coalgebras (Extended Abstract)},

booktitle = {Proc. Fifteenth International Conference on
Foundations of Software Science and Computation Structures (FoSSaCS'12)},

year = {2012},

series = {Lecture Notes Comput. Sci. (ARCoSS)},

volume = {7213},

pages = {89--103},

}

In:
Proc. Eighth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme"
(MBEES 2012).

```
@inproceedings{g_etal_12,
```

author = {Henning G\"unther and Ramin Hedayati and Helge L\"oding and Stefan Milius and M. Oliver M\"oller and Jan Peleska and Martin Sulzmann and Axel Zechner},

title = {A framework for formal verification of systems of synchronous components},

booktitle = {Proc. Eighth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme" (MBEES 2012)},

year = {2012},

pages = {},

}

In:
Proc. 4th Conference on Algebra and Coalgebra in Computer Science
(CALCO'11),

*Lecture Notes Comput. Sci.*,
vol.
6859,
pp.
55-69.

```
@inproceedings{ahm11,
```

author = {Ji\v{r}\'i Ad\'amek and Mahdieh Haddadi and Stefan Milius},

title = {From Corecursive Algebras to Corecursive Monads},

booktitle = {Proc. 4th Conference on Algebra and Coalgebra in Computer Science (CALCO'11)},

year = {2011},

series = {Lecture Notes Comput. Sci.},

volume = {6859},

pages = {55--69},

}

In:
Proc. 20th Conference on Computer Science Logic
(CSL'11),

*Leibniz International Proceedings in Informatics (LIPIcs)*,
vol.
12,
pp.
5-19.

```
@inproceedings{amms11,
```

author = {Ji\v{r}\'i Ad\'amek and Stefan Milius and Lawrence S. Moss},

title = {Power-Set Functors and Saturated Trees},

booktitle = {Proc. 20th Conference on Computer Science Logic (CSL'11)},

year = {2011},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {12},

pages = {5--19},

}

```
@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},

}

```
@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.},

}

```
@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},

}

In:
Proc. 16th International Workshop on Formal Methods for Industrial Critical Systems
(FMICS'11),

*Lecture Notes Comput. Sci.*,
vol.
6959,
pp.
68-84.

```
@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},

}

In:
Proc. Coalgebraic Methods in Computer Science
(CMCS'10),

*Electron. Notes Theor. Comput. Sci.*,
vol.
264,
pp.
3-23.

```
@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},

}

```
@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},

}

```
@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},

}

In:
Proc. 25th Annual Symposium on Logic in Computer Science
(LICS'10),
pp.
449-458.

```
@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},

}

In:
Proc. Foundations of Software Science and Computation Structures
(FoSSaCS'10),

*Lecture Notes Comput. Sci.*,
vol.
6014,
pp.
312-327.

```
@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},

}

In:
Proc. Foundations of Software Science and Computation Structures
(FoSSaCS'09),

*Lecture Notes Comput. Sci.*,
vol.
5504,
pp.
152-166.

```
@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},

}

In:
Proc. Mathematical Foundations of Programming Science
(MFPS XXV),

*Electron. Notes Theor. Comp. Sci.*,
vol.
249,
pp.
407-427.

```
@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},

}

In:
Proc. 3rd Conference on Algebra and Coalgebra in Computer Science
(CALCO'09),

*Lecture Notes Comput. Sci.*,
vol.
5728,
pp.
49-63.

```
@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},

}

In:
Proc. Coalgebraic and Algebraic Methods in Computer Science
(CALCO'09),

*Lecture Notes Comput. Sci.*,
vol.
5728,
pp.
34-48.

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

In:
Proc. Fourth Workshop "Modellbasierte Entwicklung Eingebetteter Systeme"
(MBEES 2008),
pp.
68-77.

```
@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},

}

```
@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},

}

In:
Proc. 32nd International Symposium on Mathematical Foundations of Computer Science
(MFCS 2007),

*Lecture Notes Comput. Sci.*,
vol.
4708,
pp.
240-252.

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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.},

}

In:
Proc. Mathematical Foundations of Programming Science
(MFPS XXI),

*Electron. Notes Theor. Comput. Sci.*,
vol.
155,
pp.
87-109.

```
@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},

}

```
@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},

}

In:
Proc. Coalgebraic Methods in Computer Science
(CMCS'06),

*Electron. Notes Theor. Comp. Sci.*,
vol.
164,
pp.
157-175.

```
@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},

}

```
@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},

}

In:
Proc. Category Theory and Computer Science
(CTCS'04),

*Electron. Notes Theor. Comput.Sci.*,
vol.
122,
pp.
147-170.

```
@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},

}

```
@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},

}

```
@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},

}

In:
Proc. 1st Conference on Algebra and Coalgebra in Computer Science
(CALCO'05),

*Lecture Notes in Comput. Sci.*,
vol.
3629,
pp.
293-312.

```
@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},

}

In:
Proc. Coalgebraic Methods in Computer Science
(CMCS'04),

*Electron. Notes Theor. Comput. Sci.*,
vol.
106,
pp.
3-24.

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

```
@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},

}

In:
Proc. Category Theory and Computer Science
(CTCS'02),

*Electron. Notes Theor. Comput. Sci.*,
vol.
69,
pp.
23-46.

```
@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},

}

In:
Proc. Category Theory and Computer Science
(CTCS'02),

*Electron. Notes Theor. Comput. Sci.*,
vol.
69,
pp.
287-304.

```
@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},

}

In:
Proc. Coalgebraic Methods in Computer Science
(CMCS'02),

*Electron. Notes Theor. Comput. Sci.*,
vol.
65,
pp.
1-28.

```
@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},

}