Open Access. Powered by Scholars. Published by Universities.^{®}
Other Computer Engineering Commons^{™}
Open Access. Powered by Scholars. Published by Universities.^{®}
 Keyword

 Coalgebra (13)
 Modal logic (6)
 Coalgebras (3)
 Display calculus (3)
 Coalgebraic logic (3)

 Variety (2)
 Dynamic epistemic logic (2)
 Stone duality (2)
 Duality (2)
 Vietoris topology (2)
 Stone spaces (2)
 Cover modality (2)
 Descriptive general frames (2)
 Modularity (2)
 Relation lifting (2)
 Positive modal logic (2)
 Kripke polynomial functors (2)
 Nominal sets (2)
 Modal Logic (2)
 Algebras over a monad (1)
 Bisimilarity (1)
 Bekic lemma (1)
 Category Theory (1)
 Categorical Semantics (1)
 Algebra (1)
 Abstract GSOS (1)
 Algebraic theories (1)
 Boolean algebra (1)
 Bitopologies (1)
 Algebraic models (1)
Articles 1  30 of 45
FullText Articles in Other Computer Engineering
Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz
Quasivarieties And Varieties Of Ordered Algebras: Regularity And Exactness, Alexander Kurz
Engineering Faculty Articles and Research
We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets.
We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).
Features Of AgentBased Models, Reiko Heckel, Alexander Kurz, Edmund ChattoeBrown
Features Of AgentBased Models, Reiko Heckel, Alexander Kurz, Edmund ChattoeBrown
Engineering Faculty Articles and Research
The design of agentbased models (ABMs) is often adhoc when it comes to defining their scope. In order for the inclusion of features such as network structure, location, or dynamic change to be justified, their role in a model should be systematically analysed. We propose a mechanism to compare and assess the impact of such features. In particular we are using techniques from software engineering and semantics to support the development and assessment of ABMs, such as graph transformations as semantic representations for agentbased models, feature diagrams to identify ingredients under consideration, and extension relations between graph transformation systems to ...
Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz
Foreword: Special Issue On Coalgebraic Logic, Alexander Kurz
Engineering Faculty Articles and Research
The second Dagstuhl seminar on coalgebraic logics took place from October 712, 2012, in the Leibniz Forschungszentrum Schloss Dagstuhl, following a successful earlier one in December 2009. From the 44 researchers who attended and the 30 talks presented, this collection highlights some of the progress that has been made in the field. We are grateful to Giuseppe Longo and his interest in a special issue in Mathematical Structures in Computer Science.
The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz
The Positivication Of Coalgebraic Logics, Fredrik Dahlqvist, Alexander Kurz
Engineering Faculty Articles and Research
We present positive coalgebraic logic in full generality, and show how to obtain a positive coalgebraic logic from a boolean one. On the model side this involves canonically computing a endofunctor T': Pos>Pos from an endofunctor T: Set>Set, in a procedure previously defined by the second author et alii called posetification. On the syntax side, it involves canonically computing a syntaxbuilding functor L': DL>DL from a syntaxbuilding functor L: BA>BA, in a dual procedure which we call positivication. These operations are interesting in their own right and we explicitly compute posetifications and positivications in the case ...
Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Tool Support For Reasoning In Display Calculi, Samuel Balco, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set ...
MultiType Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
MultiType Display Calculus For Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
Engineering Faculty Articles and Research
In the present paper, we introduce a multitype display calculus for dynamic epistemic logic, which we refer to as Dynamic Calculus. The displayapproach is suitable to modularly chart the space of dynamic epistemic logics on weakerthanclassical propositional base. The presence of types endows the language of the Dynamic Calculus with additional expressivity, allows for a smooth prooftheoretic treatment, and paves the way towards a general methodology for the design of proof systems for the generality of dynamic logics, and certainly beyond dynamic epistemic logic. We prove that the Dynamic Calculus adequately captures BaltagMossSolecki’s dynamic epistemic logic, and enjoys Belnapstyle ...
MultiType Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
MultiType Display Calculus For Propositional Dynamic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
We introduce a multitype display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnapstyle cutelimination and subformula property.
Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil
Positive Fragments Of Coalgebraic Logics, Adriana Balan, Alexander Kurz, Jirí Velebil
Engineering Faculty Articles and Research
Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras for weakpullback preserving functors. To facilitate this analysis we prove a number of category theoretic results ...
Extensions Of Functors From Set To VCat, Adriana Balan, Alexander Kurz, Jirí Velebil
Extensions Of Functors From Set To VCat, Adriana Balan, Alexander Kurz, Jirí Velebil
Engineering Faculty Articles and Research
We show that for a commutative quantale V every functor Set > Vcat has an enriched left Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over Vcat. Moreover, one can build functors on Vcat by equipping Setfunctors with a metric.
Approximation Of Nested Fixpoints, Alexander Kurz
Approximation Of Nested Fixpoints, Alexander Kurz
Engineering Faculty Articles and Research
The question addressed in this paper is how to correctly approximate infinite data given by systems of simultaneous corecursive definitions. We devise a categorical framework for reasoning about regular datatypes, that is, datatypes closed under products, coproducts and fixpoints. We argue that the right methodology is on one hand coalgebraic (to deal with possible nontermination and infinite data) and on the other hand 2categorical (to deal with parameters in a disciplined manner). We prove a coalgebraic version of Bekic lemma that allows us to reduce simultaneous fixpoints to a single fix point. Thus a possibly infinite object of interest is ...
Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot
Presenting Distributive Laws, Marcello M. Bonsangue, Helle H. Hansen, Alexander Kurz, Jurriaan Rot
Engineering Faculty Articles and Research
Distributive laws of a monad T over a functor F are categorical tools for specifying algebracoalgebra interaction. They proved to be important for solving systems of corecursive equations, for the specification of wellbehaved structural operational semantics and, more recently, also for enhancements of the bisimulation proof method. If T is a free monad, then such distributive laws correspond to simple natural transformations. However, when T is not free it can be rather difficult to prove the defining axioms of a distributive law. In this paper we describe how to obtain a distributive law for a monad with an equational presentation ...
Coalgebraic Semantics Of Reflexive Economics (Dagstuhl Seminar 15042), Samson Abramsky, Alexander Kurz, Pierre Lescanne, Viktor Winschel
Coalgebraic Semantics Of Reflexive Economics (Dagstuhl Seminar 15042), Samson Abramsky, Alexander Kurz, Pierre Lescanne, Viktor Winschel
Engineering Faculty Articles and Research
This report documents the program and the outcomes of Dagstuhl Seminar 15042 “Coalgebraic Semantics of Reflexive Economics”.
A ProofTheoretic Semantic Analysis Of Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
A ProofTheoretic Semantic Analysis Of Dynamic Epistemic Logic, Sabine Frittella, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano, Vlasta Sikimić
Engineering Faculty Articles and Research
The present paper provides an analysis of the existing proof systems for dynamic epistemic logic from the viewpoint of prooftheoretic semantics. Dynamic epistemic logic is one of the best known members of a family of logical systems which have been successfully applied to diverse scientific disciplines, but the proof theoretic treatment of which presents many difficulties. After an illustration of the prooftheoretic semantic principles most relevant to the treatment of logical connectives, we turn to illustrating the main features of display calculi, a prooftheoretic paradigm which has been successfully employed to give a prooftheoretic semantic account of modal and substructural ...
Epistemic Updates On Algebras, Alexander Kurz, Alessandra Palmigiano
Epistemic Updates On Algebras, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
We develop the mathematical theory of epistemic updates with the tools of duality theory. We focus on the Logic of Epistemic Actions and Knowledge (EAK), introduced by BaltagMossSolecki, without the common knowledge operator. We dually characterize the product update construction of EAK as a certain construction transforming the complex algebras associated with the given model into the complex algebra associated with the updated model. This dual characterization naturally generalizes to much wider classes of algebras, which include, but are not limited to, arbitrary BAOs and arbitrary modal expansions of Heyting algebras (HAOs). As an application of this dual characterization, we ...
Dynamic Sequent Calculus For The Logic Of Epistemic Actions And Knowledge, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Dynamic Sequent Calculus For The Logic Of Epistemic Actions And Knowledge, Giuseppe Greco, Alexander Kurz, Alessandra Palmigiano
Engineering Faculty Articles and Research
"Dynamic Logics (DLs) form a large family of nonclassical logics, and perhaps the one enjoying the widest range of applications. Indeed, they are designed to formalize change caused by actions of diverse nature: updates on the memory state of a computer, displacements of moving robots in an environment, measurements in models of quantum physics, belief revisions, knowledge updates, etc. In each of these areas, DLformulas express properties of the model encoding the present state of affairs, as well as the pre and postconditions of a given action. Actions are semantically represented as transformations of one model into another, encoding the ...
Relation Lifting, With An Application To The ManyValued Cover Modality, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jirí Velebil
Relation Lifting, With An Application To The ManyValued Cover Modality, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jirí Velebil
Engineering Faculty Articles and Research
We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the “powerset monad” on categories, one is the preservation by T of “exactness” of certain squares. Both characterisations are generalisations of the “classical” results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks.
The results presented in this paper ...
Nominal Coalgebraic Data Types With Applications To Lambda Calculus, Alexander Kurz, Daniela Petrişan, Paula Severi, FerJan De Vries
Nominal Coalgebraic Data Types With Applications To Lambda Calculus, Alexander Kurz, Daniela Petrişan, Paula Severi, FerJan De Vries
Engineering Faculty Articles and Research
We investigate final coalgebras in nominal sets. This allows us to define types of infinite data with binding for which all constructions automatically respect alpha equivalence. We give applications to the infinitary lambda calculus.
Nominal Regular Expressions For Languages Over Infinite Alphabets, Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto
Nominal Regular Expressions For Languages Over Infinite Alphabets, Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto
Engineering Faculty Articles and Research
We propose regular expressions to abstractly model and study properties of resourceaware computations. Inspired by nominal techniques – as those popular in process calculi – we extend classical regular expressions with names (to model computational resources) and suitable operators (for allocation, deallocation, scoping of, and freshness conditions on resources). We discuss classes of such nominal regular expressions, show how such expressions have natural interpretations in terms of languages over infinite alphabets, and give Kleene theorems to characterise their formal languages in terms of nominal automata.
Nominal Computation Theory (Dagstuhl Seminar 13422), Mikołaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts
Nominal Computation Theory (Dagstuhl Seminar 13422), Mikołaj Bojanczyk, Bartek Klin, Alexander Kurz, Andrew M. Pitts
Engineering Faculty Articles and Research
This report documents the program and the outcomes of Dagstuhl Seminar 13422 “Nominal Computation Theory”. The underlying theme of the seminar was nominal sets (also known as sets with atoms or FraenkelMostowski sets) and they role and applications in three distinct research areas: automata over infinite alphabets, program semantics using nominal sets and nominal calculi of concurrent processes.
Coalgebraic Logics (Dagstuhl Seminar 12411), ErnstErich Doberkat, Alexander Kurz
Coalgebraic Logics (Dagstuhl Seminar 12411), ErnstErich Doberkat, Alexander Kurz
Engineering Faculty Articles and Research
This report documents the program and the outcomes of Dagstuhl Seminar 12411 “Coalgebraic Logics”. The seminar deals with recent developments in the area of coalgebraic logic, a branch of logics which combines modal logics with coalgebraic semantics. Modal logic finds its uses when reasoning about behavioural and temporal properties of computation and communication, coalgebras have evolved into a general theory of systems. Consequently, it is natural to combine both areas for a mathematical description of system specification. Coalgebraic logics are closely related to the broader categories semantics/formal methods and verification/logic.
Completeness For The Coalgebraic Cover Modality, Clemens Kupke, Alexander Kurz, Yde Venema
Completeness For The Coalgebraic Cover Modality, Clemens Kupke, Alexander Kurz, Yde Venema
Engineering Faculty Articles and Research
We study the finitary version of the coalgebraic logic introduced by L. Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a socalled coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation.
As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic ...
Strongly Complete Logics For Coalgebras, Alexander Kurz, Jiří Rosický
Strongly Complete Logics For Coalgebras, Alexander Kurz, Jiří Rosický
Engineering Faculty Articles and Research
Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for setbased coalgebras. In particular, a general construction of a logic from an arbitrary setfunctor is given and proven to be strongly complete under additional assumptions. We proceed in three parts.
Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the ...
Generic Trace Logics, Christian Kissig, Alexander Kurz
Generic Trace Logics, Christian Kissig, Alexander Kurz
Engineering Faculty Articles and Research
We combine previous work on coalgebraic logic with the coalgebraic traces semantics of Hasuo, Jacobs, and Sokolova.
Relation Liftings On Preorders And Posets, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jiří Velebil
Relation Liftings On Preorders And Posets, Marta Bílková, Alexander Kurz, Daniela Petrişan, Jiří Velebil
Engineering Faculty Articles and Research
The category Rel(Set) of sets and relations can be described as a category of spans and as the Kleisli category for the powerset monad. A setfunctor can be lifted to a functor on Rel(Set) iff it preserves weak pullbacks. We show that these results extend to the enriched setting, if we replace sets by posets or preorders. Preservation of weak pullbacks becomes preservation of exact lax squares. As an application we present Moss’s coalgebraic over posets.
Towards Nominal Formal Languages, Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto
Towards Nominal Formal Languages, Alexander Kurz, Tomoyuki Suzuki, Emilio Tuosto
Engineering Faculty Articles and Research
We introduce formal languages over infinite alphabets where words may contain binders.We define the notions of nominal language, nominal monoid, and nominal regular expressions. Moreover, we extend historydependent automata (HDautomata) by adding stack, and study the recognisability of nominal languages.
On Universal Algebra Over Nominal Sets, Alexander Kurz, Daniela Petrişan
On Universal Algebra Over Nominal Sets, Alexander Kurz, Daniela Petrişan
Engineering Faculty Articles and Research
We investigate universal algebra over the category Nom of nominal sets. Using the fact that Nom is a full re ective subcategory of a monadic category, we obtain an HSPlike theorem for algebras over nominal sets. We isolate a `uniform' fragment of our equational logic, which corresponds to the nominal logics present in the literature. We give semantically invariant translations of theories for nominal algebra and NEL into `uniform' theories and systematically prove HSP theorems for models of these theories.
On Coalgebras Over Algebras, Adriana Balan, Alexander Kurz
On Coalgebras Over Algebras, Adriana Balan, Alexander Kurz
Engineering Faculty Articles and Research
We extend Barr’s wellknown characterization of the final coalgebra of a Setendofunctor as the completion of its initial algebra to the EilenbergMoore category of algebras for a Setmonad M for functors arising as liftings. As an application we introduce the notion of commuting pair of endofunctors with respect to the monad M and show that under reasonable assumptions, the final coalgebra of one of the endofunctors involved can be obtained as the free algebra generated by the initial algebra of the other endofunctor.
Families Of Symmetries As Efficient Models Of Resource Binding, Vincenzo Ciancia, Alexander Kurz, Ugo Montanari
Families Of Symmetries As Efficient Models Of Resource Binding, Vincenzo Ciancia, Alexander Kurz, Ugo Montanari
Engineering Faculty Articles and Research
Calculi that feature resourceallocating constructs (e.g. the picalculus or the fusion calculus) require special kinds of models. The bestknown ones are presheaves and nominal sets. But named sets have the advantage of being finite in a wide range of cases where the other two are infinite. The three models are equivalent. Finiteness of named sets is strictly related to the notion of finite support in nominal sets and the corresponding presheaves. We show that named sets are generalisd by the categorical model of families, that is, free coproduct completions, indexed by symmetries, and explain how locality of interfaces gives ...
Bitopological Duality For Distributive Lattices And Heyting Algebras, Guram Bezhanishvili, Nick Bezhanishvili, David Gabelaia, Alexander Kurz
Bitopological Duality For Distributive Lattices And Heyting Algebras, Guram Bezhanishvili, Nick Bezhanishvili, David Gabelaia, Alexander Kurz
Engineering Faculty Articles and Research
We introduce pairwise Stone spaces as a natural bitopological generalization of Stone spaces—the duals of Boolean algebras—and show that they are exactly the bitopological duals of bounded distributive lattices. The category PStone of pairwise Stone spaces is isomorphic to the category Spec of spectral spaces and to the category Pries of Priestley spaces. In fact, the isomorphism of Spec and Pries is most naturally seen through PStone by first establishing that Pries is isomorphic to PStone, and then showing that PStone is isomorphic to Spec. We provide the bitopological and spectral descriptions of many algebraic concepts important for ...
Algebraic Theories Over Nominal Sets, Alexander Kurz, Daniela Petrişan, Jiří Velebil
Algebraic Theories Over Nominal Sets, Alexander Kurz, Daniela Petrişan, Jiří Velebil
Engineering Faculty Articles and Research
We investigate the foundations of a theory of algebraic data types with variable binding inside classical universal algebra. In the first part, a categorytheoretic study of monads over the nominal sets of Gabbay and Pitts leads us to introduce new notions of finitary based monads and uniform monads. In a second part we spell out these notions in the language of universal algebra, show how to recover the logics of GabbayMathijssen and CloustonPitts, and apply classical results from universal algebra.