text:
@book{Pierce2002,
author = {Pierce, Benjamin C.},
isbn = {0-262-16209-1},
publisher = {MIT Press},
title = {Types and Programming Languages},
year = {2002}
}
@article{Kock1970,
author = {Kock, Anders},
doi = {10.1007/BF01220868},
issn = {0003-889X},
journal = {Arch. der Math.},
month = dec,
number = {1},
pages = {1--10},
title = {Monads on symmetric monoidal closed categories},
volume = {21},
year = {1970}
}
@article{Carboni1984a,
author = {Carboni, Aurelio and Kasangian, Stefano and Street, Ross},
doi = {10.1016/0022-4049(84)90061-6},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = sep,
number = {3},
pages = {259--267},
title = {Bicategories of spans and relations},
volume = {33},
year = {1984}
}
@article{Fiore2006,
abstract = {We study three operational models of name-passing process calculi: coalgebras on (pre)sheaves, indexed labelled transition systems, and history dependent automata. The coalgebraic model is considered both for presheaves over the category of finite sets and injections, and for its subcategory of atomic sheaves known as the Schanuel topos. Each coalgebra induces an indexed labelled transition system. Such transition systems are characterised, relating the coalgebraic approach to an existing model of name-passing. Further, we consider internal labelled transition systems within the sheaf topos, and axiomatise a class that is in precise correspondence with the coalgebraic and the indexed labelled transition system models. By establishing and exploiting the equivalence of the Schanuel topos with a category of named-sets, these internal labelled transition systems are also related to the theory of history dependent automata. ?? 2006 Elsevier Inc. All rights reserved.},
author = {Fiore, Marcelo P. and Staton, Sam},
doi = {10.1016/j.ic.2005.08.004},
issn = {08905401},
journal = {Inf. Comput.},
month = apr,
number = {4},
pages = {524--560},
title = {Comparing operational models of name-passing process calculi},
volume = {204},
year = {2006}
}
@article{Street1972,
author = {Street, Ross},
doi = {10.1016/0022-4049(72)90019-9},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jul,
number = {2},
pages = {149--168},
title = {The formal theory of monads},
volume = {2},
year = {1972}
}
@article{Gumm2001,
author = {Gumm, H. Peter and Schr{\"{o}}der, Tobias},
doi = {10.1016/S1571-0661(04)80908-3},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {bisimulation,coalgebra,distributive lattice,fuzzy transition,monoid,multiset,refinable,transition system,weak pullback preservation},
month = may,
number = {1},
pages = {185--204},
title = {Monoid-labeled transition systems},
volume = {44},
year = {2001}
}
@incollection{Kohlas2009,
abstract = {According to Shannon's classical information theory [19] information is measured by the reduction of uncertainty and the latter is measured by entropy. This theory is concerned with the transmission of symbols from a finite alphabet. The uncertainty concerns the question which symbol is sent and the information is given by a probabilistic model of the transmission channel and the symbol observed at the output of the channel. This leads to a statistical communication theory which is still the main subject of communication theory today.},
author = {Kohlas, J{\"{u}}rg and Schneuwly, Cesar},
booktitle = {Form. Theor. Inf.},
doi = {10.1007/978-3-642-00659-3_5},
editor = {Sommaruga, Giovanni},
isbn = {3642006582},
issn = {03029743},
pages = {95--127},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Information algebra},
volume = {5363},
year = {2009}
}
@article{Seal2013,
abstract = {We exhibit sufficient conditions for a monoidal monad T on a monoidal category C to induce a monoidal structure on the Eilenberg--Moore category C^T that represents bimorphisms. The category of actions in C^T is then shown to be monadic over the base category C.},
archivePrefix = {arXiv},
arxivId = {1205.0101},
author = {Seal, Gavin J.},
eprint = {1205.0101},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Action,Bimorphism,Eilenberg-Moore category,Monad,Monoidal category},
number = {15},
pages = {403--433},
title = {Tensors, monads and actions},
volume = {28},
year = {2013}
}
@incollection{Mulry1994a,
abstract = {Monads, comonads and categories of algebras have become increasingly important tools in formulating and interpreting concepts in programming language semantics. A natural question that arises is how various categories of algebras for different monads relate functorially. In this paper we investigate when functors between categories with monads or comonads can be lifted to their corresponding Kleisli categories. Determining when adjoint pairs of functors can be lifted or inherited is of particular interest. The results lead naturally to various applications in both extensional and intensional semantics, including work on partial maps and data types and the work of Brookes/Geva on computational comonads.},
author = {Mulry, Philip S.},
booktitle = {Math. Found. Program. Semant.},
doi = {10.1007/3-540-58027-1_15},
editor = {Brookes, Stephen and Main, Michael and Melton, Austin and Mislove, Michael and Schmidt, David},
isbn = {9783540580270},
issn = {16113349},
keywords = {category_theory,functor_lifting,kleisli_category},
pages = {304--319},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Lifting theorems for Kleisli categories},
volume = {802},
year = {1994}
}
@article{Gehrke2005,
abstract = {In this paper we consider distributive modal logic, a setting in which we may add modalities, such as classical types of modalities as well as weak forms of negation, to the fragment of classical propositional logic given by conjunction, disjunction, true, and false. For these logics we define both algebraic semantics, in the form of distributive modal algebras, and relational semantics, in the form of ordered Kripke structures. The main contributions of this paper lie in extending the notion of Sahlqvist axioms to our generalized setting and proving both a correspondence and a canonicity result for distributive modal logics axiomatized by Sahlqvist axioms. Our proof of the correspondence result relies on a reduction to the classical case, but our canonicity proof departs from the traditional style and uses the newly extended algebraic theory of canonical extensions.},
author = {Gehrke, Mai and Nagahashi, Hideo and Venema, Yde},
doi = {10.1016/j.apal.2004.04.007},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {Canonical extensions,Canonical logic,Canonical varieties,Correspondence theory,Distributive modal algebras,Distributive modal logic,Duality,Lattice expansions},
month = jan,
number = {1-3},
pages = {65--102},
publisher = {Elsevier},
title = {A Sahlqvist theorem for distributive modal logic},
volume = {131},
year = {2005}
}
@article{Yasuoka2014,
abstract = {We employ Clarkson and Schneider's "hyperproperties" to classify various verification problems of quantitative information flow. The results of this paper unify and extend the previous results on the hardness of checking and inferring quantitative information flow. In particular, we identify a subclass of liveness hyperproperties, which we call ". k-observable hyperproperties", that can be checked relative to a reachability oracle via self composition.},
author = {Yasuoka, Hirotoshi and Terauchi, Tachio},
doi = {10.1016/j.tcs.2013.07.031},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Hyperproperties,Quantitative information flow,Verification},
number = {C},
pages = {167--182},
publisher = {Elsevier B.V.},
title = {Quantitative information flow as safety and liveness hyperproperties},
volume = {538},
year = {2014}
}
@incollection{Cirstea2007a,
abstract = {We present a coalgebraic semantics for reasoning about information update in multi-agent systems. The novelty is that we have one structure for both states and actions and thus our models do not involve the "change-of- model" phenomena that arise when using Kripke models. However, we prove that the usual models can be constructed from ours by categorical adjunction. The generality and abstraction of our coalgebraic model turns out to be extremely useful in proving preservation properties of update. In particular, we prove that positive knowledge is preserved and acquired as a result of epistemic update. We also prove common and nested knowledge properties of epistemic updates induced by specific epistemic actions such as public and private announcements, lying, and in particular unsafe actions of security protocols. Our model directly gives rise to a coalgebraic logic with both dynamic and epistemic modalities. We prove a soundness and completeness result for this logic, and illustrate the applicability of the logic by deriving knowledge properties of a simple security protocol. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.},
address = {Berlin, Heidelberg},
author = {C{\^{i}}rstea, Corina and Sadrzadeh, Mehrnoosh},
booktitle = {Proc. 2nd Int. Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-540-73859-6_11},
editor = {Mossakowski, Till and Montanari, Ugo and Haveraaen, Magne},
isbn = {9783540738572},
issn = {03029743 16113349},
pages = {158--172},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Cmoputer Science},
title = {Coalgebraic epistemic update without change of model},
volume = {4624},
year = {2007}
}
@article{Bonsangue2012,
abstract = {Coalgebras provide a uniform framework to study dynamical systems, including several types of automata. In this paper, we make use of the coalgebraic view on systems to investigate, in a uniform way, under which conditions calculi that are sound and complete with respect to behavioral equivalence can be extended to a coarser coalgebraic language equivalence, which arises from a generalised powerset construction that determinises coalgebras. We show that soundness and completeness are established by proving that expressions modulo axioms of a calculus form the rational fixpoint of the given type functor. Our main result is that the rational fixpoint of the functor $FT$, where $T$ is a monad describing the branching of the systems (e.g. non-determinism, weights, probability etc.), has as a quotient the rational fixpoint of the "determinised" type functor $\bar F$, a lifting of $F$ to the category of $T$-algebras. We apply our framework to the concrete example of weighted automata, for which we present a new sound and complete calculus for weighted language equivalence. As a special case, we obtain non-deterministic automata, where we recover Rabinovich's sound and complete calculus for language equivalence.},
archivePrefix = {arXiv},
arxivId = {1104.2803},
author = {Bonsangue, Marcello M. and Milius, Stefan and Silva, Alexandra},
doi = {10.1145/0000000.0000000},
eprint = {1104.2803},
journal = {ArXiv e-prints},
month = apr,
title = {Sound and complete axiomatizations of coalgebraic language equivalence},
year = {2012}
}
@article{Jansen2015,
abstract = {In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.},
archivePrefix = {arXiv},
arxivId = {1504.00198},
author = {Jansen, Nils and Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Olmedo, Federico and Gretz, Friedrich and McIver, Annabelle},
doi = {10.1016/j.entcs.2015.12.013},
eprint = {1504.00198},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Conditional Probabilities,Probabilistic Programming,Program Transformation,Semantics},
month = dec,
pages = {199--216},
publisher = {Elsevier B.V.},
title = {Conditioning in Probabilistic Programming},
volume = {319},
year = {2015}
}
@inproceedings{Chu2016,
abstract = {Machine learning techniques based on neural networks are achieving remarkable results in a wide variety of domains. Often, the training of models requires large, representative datasets, which may be crowdsourced and contain sensitive information. The models should not expose private information in these datasets. Addressing this goal, we develop new algorithmic techniques for learning and a refined analysis of privacy costs within the framework of differential privacy. Our implementation and experiments demonstrate that we can train deep neural networks with non-convex objectives, under a modest privacy budget, and at a manageable cost in software complexity, training efficiency, and model quality.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {arXiv:1607.00133v1},
author = {Abadi, Martin and Chu, Andy and Goodfellow, Ian and McMahan, H. Brendan and Mironov, Ilya and Talwar, Kunal and Zhang, Li},
booktitle = {Proc. 2016 ACM SIGSAC Conf. Comput. Commun. Secur. - CCS'16},
doi = {10.1145/2976749.2978318},
eprint = {arXiv:1607.00133v1},
isbn = {9781450341394},
issn = {9781450321389},
pages = {308--318},
publisher = {ACM Press},
title = {Deep Learning with Differential Privacy},
year = {2016}
}
@article{Adamek1998,
abstract = {Analogously to the fact that Lawvere's algebraic theories of (finitary) varieties are precisely the small categories with finite products, we prove that (i) algebraic theories of many-sorted quasivarieties are precisely the small, left exact categories with enough regular injectives and (ii) algebraic theories of many-sorted Horn classes are precisely the small left exact categories with enough -injectives, where is a class of monomorphisms closed under finite products and containing all regular monomorphisms. We also present a Gabriel–Ulmer-type duality theory for quasivarieties and Horn classes.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Porst, Hans-E.},
doi = {10.1006/jabr.1998.7499},
issn = {00218693},
journal = {J. Algebr.},
month = oct,
number = {2},
pages = {379--398},
title = {Algebraic Theories of Quasivarieties},
volume = {208},
year = {1998}
}
@article{Lucyshyn-wright2016,
author = {Lucyshyn-wright, Rory B. B.},
journal = {Theory Appl. Categ.},
keywords = {2016,algebraic theory,and phrases,b,c rory b,enriched cate-,free cocompletion,gory theory,lawvere theory,lucyshyn-wright,monad,permission to copy for,private use granted,universal algebra},
number = {5},
pages = {101--137},
title = {Enriched Algebraic Theories and Monads for a System of Arities},
volume = {31},
year = {2016}
}
@article{Adamek2014b,
abstract = {An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as coproducts of the terminal coalgebra (considered as an algebra) and free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.},
archivePrefix = {arXiv},
arxivId = {1407.4425},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Haddadi, Mahdie and Milius, Stefan},
doi = {10.2168/LMCS-10(3:19)2014},
eprint = {1407.4425},
journal = {Log. Methods Comput. Sci.},
month = jul,
number = {3:19},
pages = {1--51},
title = {Corecursive algebras, corecursive monads and Bloom monads},
volume = {10},
year = {2014}
}
@inproceedings{Lindley2014,
abstract = {Plotkin and Power's algebraic effects combined with Plotkin and Pretnar's effect handlers provide a foundation for modular programming with effects. We present a generalisation of algebraic effects and effect handlers to support other kinds of effectful computations corresponding to McBride and Paterson's idioms and Hughes' arrows.},
address = {New York, New York, USA},
author = {Lindley, Sam},
booktitle = {Proc. 10th ACM SIGPLAN Work. Generic Program. - WGP '14},
doi = {10.1145/2633628.2633636},
isbn = {9781450330428},
keywords = {algebraic effects,applicative functors,arrows,call-by-push-value,effect handlers,efficient implementa-,idioms,in both cases providing,monads,more space and time,tions than monadic alternatives},
pages = {47--58},
publisher = {ACM Press},
title = {Algebraic effects and effect handlers for idioms and arrows},
year = {2014}
}
@inproceedings{Tews2004,
abstract = {Relation lifting [6] extends an endofunctor F : C???C to a functor Rel(F) : Rel(C)???Rel(C), where Rel(C) is a suitable category of relations over C. The relation lifting for the functor F can be used to define the notion of bisimulation for coalgebras X???F(X). The related notion of predicate lifting can be used to define invariants for F-coalgebras. Predicate and relation lifting can be directly defined for a rich class of polynomial functors [5,6,19]. In this paper I investigate the case where the functor F is defined as the initial semantics of a (single sorted) parametric algebraic specification.},
author = {Tews, Hendrik},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/j.entcs.2004.02.040},
issn = {15710661},
keywords = {Algebraic specification,Bisimulation,Coalgebra,Endofunctor,Polynomial functor,Relation lifting},
pages = {335--353},
title = {Predicate and relation lifting for parametric algebraic specifications},
volume = {107},
year = {2004}
}
@article{Bonchi2011a,
author = {Bonchi, Filippo and K{\"{o}}nig, Barbara and H{\"{u}}lsbusch, Mathias},
pages = {10},
title = {A coalgebraic perspective on minimization, determinization and behavioural metrics},
type = {Journal article},
volume = {9},
year = {2011}
}
@article{Hyland2007a,
author = {Hyland, Martin and Power, A. John},
doi = {10.1016/j.entcs.2007.02.019},
issn = {1571-0661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Universal algebra,algebra,universal},
mendeley-tags = {algebra,universal},
number = {0},
pages = {437--458},
title = {The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads},
type = {Journal article},
volume = {172},
year = {2007}
}
@article{Cirstea2017,
abstract = {{\textcopyright} C. C{\^{i}}rstea.We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that by suitably adapting the definition of coalgebraic bisimulation, one obtains a general and uniform account of the linear-time behaviour of a state in such a coalgebra. By moving away from a boolean universe of truth values, our approach can measure the extent to which a state in a system with branching is able to exhibit a particular linear-time behaviour. This instantiates to measuring the probability of a specific behaviour occurring in a probabilistic system, or measuring the minimal cost of exhibiting a specific behaviour in the case of weighted computations.},
author = {C{\^{i}}rstea, Corina},
doi = {10.3233/FI-2017-1474},
editor = {Baelde, David and Carayol, Arnaud and Matthes, Ralph and Walukiewicz, Igor},
issn = {01692968},
journal = {Fundam. Informaticae},
keywords = {coalgebra,linear time,trace},
month = mar,
number = {3-4},
pages = {379--406},
title = {From branching to linear time, coalgebraically},
volume = {150},
year = {2017}
}
@inproceedings{Adamek2012c,
abstract = {For set functors preserving intersections, a new description of the final coalgebra and the initial algebra is presented: the former consists of all well-pointed coalgebras. These are the pointed coalgebras having no proper subobject and no proper quotient. And the initial algebra consists of all well-pointed coalgebras that are well-founded in the sense of Taylor [16]. Finally, the initial iterative algebra consists of all finite well-pointed coalgebras. Numerous examples are discussed e.g. automata, graphs, and labeled transition systems.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Moss, Lawrence S. and Sousa, Lurdes},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-28729-9_6},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {89--103},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Well-Pointed Coalgebras (Extended Abstract)},
volume = {7213},
year = {2012}
}
@article{Biering2007,
author = {Biering, Bodil and Birkedal, Lars and Torp-Smith, Noah},
doi = {10.1145/1275497.1275499},
issn = {01640925},
journal = {ACM Trans. Program. Lang. Syst.},
month = aug,
number = {5},
pages = {24--es},
title = {BI-hyperdoctrines, higher-order separation logic, and abstraction},
volume = {29},
year = {2007}
}
@article{Cleaveland2005,
abstract = {This paper presents a mu-calculus-based modal logic for describing properties of reactive probabilistic labeled transition systems (RPLTSs) and develops a model-checking algorithm for determining whether or not states in finite-state RPLTSs satisfy formulas in the logic. The logic is based on the distinction between (probabilistic) "systems" and (nonprobabilistic) "observations": using the modal mu-calculus, one may specify sets of observations, and the semantics of our logic then enable statements to be made about the measures of such sets at various system states. The logic may be used to encode a variety of probabilistic modal and temporal logics; in addition, the model-checking problem for it may be reduced to the calculation of solutions to systems of non-linear equations. Finally, the logic induces an equivalence on RPLTSs that coincides with accepted notions of probabilistic bisimulation in the literature. {\textcopyright} 2005 Published by Elsevier B.V.},
author = {Cleaveland, Rance and Iyer, S. Purushothaman and Narasimha, Murali},
doi = {10.1016/j.tcs.2005.03.048},
isbn = {3-540-65719-3},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Model-checking,Probabilistic bisimulation,Probabilistic temporal logic,Probabilistic transition systems,Reactive systems},
number = {2-3},
pages = {316--350},
title = {Probabilistic temporal logics via the modal mu-calculus},
volume = {342},
year = {2005}
}
@techreport{Kupke2003,
abstract = {We argue that the category of Stone spaces forms an interesting base category for coalgebras, in particular, if one considers the Vietoris functor as an analogue to the power set functor on the category of sets. We prove that the so-called descriptive general frames, which play a fundamental role in the semantics of modal logics, can be seen as Stone coalgebras in a natural way. This yields a duality between modal algebras and coalgebras for the Vietoris functor. Building on this idea, we introduce the notion of a Vietoris polynomial functor over the category of Stone spaces. For each such functor T we provide an adjunction between T-sorted Boolean algebras with operators and the Stone coalgebras for T. We also identify the subcategory of algebras on which the adjunction restricts to an equivalence and show that the final T-coalgebra is the dual of the initial T-BAO.},
author = {Kupke, Clemens and Kurz, Alexander and Venema, Yde},
booktitle = {Theor. Comput. Sci.},
doi = {10.1016/j.tcs.2004.07.023},
issn = {0304-3975},
keywords = {In this paper we argue that the category of Stone,Kripke polynomial functors,can be seen as Stone coalgebras in a natural way.,coalgebra,descriptive general,frames,functors,if one considers the Vietoris functor as an analog,in particular,kripke,kripke polynomial functors,modal logic,polynomial,stone spaces,this shows that Coalg(T)^op is a full reflective s,vietoris topology,we introduce the notion of a Vietoris polynomial f,which play a fundamental role in the semantics of},
mendeley-tags = {In this paper we argue that the category of Stone,can be seen as Stone coalgebras in a natural way.,functors,if one considers the Vietoris functor as an analog,in particular,kripke,polynomial,this shows that Coalg(T)^op is a full reflective s,we introduce the notion of a Vietoris polynomial f,which play a fundamental role in the semantics of},
month = oct,
number = {1--2},
pages = {109--134},
title = {Stone coalgebras},
type = {Journal article},
volume = {327},
year = {2003}
}
@article{Corfield2011,
author = {Corfield, David},
doi = {10.1016/j.shpsa.2011.09.013},
issn = {00393681},
journal = {Stud. Hist. Philos. Sci. Part A},
month = dec,
number = {4},
pages = {571--579},
publisher = {Elsevier Ltd},
title = {Understanding the infinite II: Coalgebra},
volume = {42},
year = {2011}
}
@article{Mclarty1990,
abstract = {The view that toposes originated as generalized set theory is a figment of set theoretically educated common sense. This false history obstructs understanding of category theory and especially of categorical foundations for mathematics. Problems in geometry, topology, and related algebra led to categories and toposes. Elementary toposes arose when Lawvere's interest in the foundations of physics and Tierney's in the foundations of topology led both to study Grothendieck's foundations for algebraic geometry. I end with remarks on a categorical view of the history of set theory, including a false history plausible from that point of view that would make it helpful to introduce toposes as a generalization from set theory.},
author = {Mclarty, Colin},
doi = {10.1093/bjps/41.3.351},
isbn = {0007-0882},
issn = {00070882},
journal = {Br. J. Philos. Sci.},
number = {3},
pages = {351--375},
title = {The uses and abuses of the history of topos theory},
volume = {41},
year = {1990}
}
@article{Zhang2016,
abstract = {We study how to communicate findings of Bayesian inference to third parties, while preserving the strong guarantee of differential privacy. Our main contributions are four different algorithms for private Bayesian inference on proba-bilistic graphical models. These include two mechanisms for adding noise to the Bayesian updates, either directly to the posterior parameters, or to their Fourier transform so as to preserve update consistency. We also utilise a recently introduced posterior sampling mechanism, for which we prove bounds for the specific but general case of discrete Bayesian networks; and we introduce a maximum-a-posteriori private mechanism. Our analysis includes utility and privacy bounds, with a novel focus on the influence of graph structure on privacy. Worked examples and experiments with Bayesian na{\"i}ve Bayes and Bayesian linear regression illustrate the application of our mechanisms.},
archivePrefix = {arXiv},
arxivId = {1512.06992},
author = {Zhang, Zuhe and Rubinstein, Benjamin and Dimitrakakis, Christos},
eprint = {1512.06992},
isbn = {9781577357605},
journal = {Proc. 30th Conf. Artif. Intell. (AAAI 2016)},
keywords = {Technical Papers: Machine Learning Methods},
pages = {1--23},
title = {On the Differential Privacy of Bayesian Inference},
year = {2016}
}
@article{Castro2011,
abstract = {In this paper, we investigate formal mechanisms to enable designers to decompose specifications (stated in a given logic) into several interacting components in such a way that the composition of these components preserves their encapsulation and internal non-determinism. The preservation of encapsulation (or locality) enables a modular form of reasoning over specifications, while the conservation of the internal non-determinism is important to guarantee that the branching time properties of components are not lost when the entire system is obtained. The basic ideas come from the work of Fiadeiro and Maibaum where notions from category theory are used to structure logical specifications. As the work of Fiadeiro and Maibaum is stated in a linear temporal logic, here we investigate how to extend these notions to a branching time logic, which can be used to reason about systems where non-determinism is present. To illustrate the practical applications of these ideas, we introduce deontic operators in our logic and we show that the modularization of specifications also allows designers to maintain the encapsulation of deontic prescriptions; this is in particular useful to reason about fault-tolerant systems, as we demonstrate with a small example.},
author = {Castro, Pablo F. and Maibaum, Thomas S.E.},
doi = {10.1016/j.tcs.2011.12.016},
issn = {0304-3975},
journal = {Theor. Comput. Sci.},
keywords = {Category theory},
number = {0},
pages = {--},
title = {Encapsulating deontic and branching time specifications},
type = {Journal article},
year = {2011}
}
@inproceedings{Gehrke2010,
address = {Bordeaux},
author = {Gehrke, Mai and Grigorieff, Serge and Pin, Jean-{\'{E}}ric},
booktitle = {Proc. ICALP 2010 Part II},
doi = {10.1007/978-3-642-14162-1},
editor = {Abramsky, Samson and Gavoille, Cyril and Kirchner, Claude and {Meyer auf der Heide}, Friedhelm and Spirakis, Paul G.},
isbn = {978-3-642-14161-4},
pages = {151--162},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A topological approach to Recognition},
volume = {6199},
year = {2010}
}
@article{Blaauw2013,
abstract = {Privacy is valued by many. But what it means to have privacy remains less than clear. In this paper, I argue that the notion of privacy should be understood in epistemic terms. What it means to have (some degree of) privacy is that other persons do not stand in significant epistemic relations to those truths one wishes to keep private.},
author = {Blaauw, Martijn},
doi = {10.1017/epi.2013.12},
isbn = {9780494603031},
issn = {1742-3600},
journal = {Episteme},
month = jun,
number = {02},
pages = {167--177},
title = {THE EPISTEMIC ACCOUNT OF PRIVACY},
volume = {10},
year = {2013}
}
@article{Swierstra2008,
author = {Swierstra, Wouter},
doi = {10.1017/S0956796808006758},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = mar,
number = {04},
pages = {423--436},
title = {Data types {\`{a}} la carte},
volume = {18},
year = {2008}
}
@article{Lack2002,
author = {Lack, Stephen and Street, Ross},
doi = {10.1016/S0022-4049(02)00137-8},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1-3},
pages = {243--265},
title = {The formal theory of monads II},
volume = {175},
year = {2002}
}
@misc{Admek2004,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
booktitle = {Stud. Log.},
doi = {10.1007/s11225-005-7033-6},
issn = {0039-3215},
keywords = {exact generator,pseudoequivalence,quasivariety,regular generator,variety},
number = {1-2},
pages = {7--33},
title = {On quasivarieties and varieties as categories},
volume = {78},
year = {2004}
}
@article{Birkedal2011,
author = {Birkedal, Lars and Reus, Bernhard and Schwinghammer, Jan and St{\o}vring, Kristian and Thamsborg, Jacob and Yang, Hongseok},
doi = {10.1145/1925844.1926401},
isbn = {9781450304900},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {capability calculus,els,frame rules,indirection theory,kripke models,step-indexed mod-,ultrametric spaces},
month = jan,
number = {1},
pages = {119},
title = {Step-indexed kripke models over recursive worlds},
volume = {46},
year = {2011}
}
@article{Pare1974,
abstract = {Given a cartesian closed category E with subobject classifier t:l->$\Omega$, it is shown that the functor $\Omega$^( ) : E^op->E is tripleable. Standard results from the theory of triples are then used to show that E has I-colimits if and only if it has I^op-limits. This gives a new proof of Mikkelsen's theorem which states that E has all finite colimits.},
author = {Par{\'{e}}, Robert},
doi = {10.1090/S0002-9904-1974-13497-X},
issn = {0002-9904},
journal = {Bull. Am. Math. Soc.},
keywords = {Colimits,Elementary topos,Limits,Triple},
month = may,
number = {3},
pages = {556--562},
title = {Colimits in Topoi},
volume = {80},
year = {1974}
}
@book{Flu2008,
editor = {Flum, Jörg and Grädel, Erich and Wilke, Thomas},
pages = {736},
publisher = {Amsterdam University Press},
series = {Texts in Logic and Games},
title = {Logic and Automata: History and Perspectives},
year = {2008}
}
@article{Adamek2011d,
abstract = {B. Courcelle studied algebraic trees as precisely the solutions of all recursive program schemes for a given signature in Set. He proved that the corresponding monad is iterative. We generalize this to recursive program schemes over a given finitary endofunctor H of a "suitable" category. A monad is called second-order iterative if every guarded recursive program scheme has a unique solution in it. We construct two second-order iterative monads: one, called the second-order rational monad, SH, is proved to be the initial second-order iterative monad. The other one, called the context-free monad, CH, is a quotient of SH and in the original case of a polynomial endofunctor H of Set we prove that CH is the monad studied by B. Courcelle. The question whether these two monads are equal is left open. ?? 2011 Elsevier B.V. All rights reserved.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1016/j.tcs.2011.04.027},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Algebraic trees,Ideal theory,Monads,Recursive program schemes},
number = {38},
pages = {4969--4988},
publisher = {Elsevier B.V.},
title = {On second-order iterative monads},
volume = {412},
year = {2011}
}
@article{Bauer2012b,
abstract = {Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel ways. We give a denotational semantics of eff and discuss a prototype implementation based on it. Through examples we demonstrate how the standard effects are treated in eff, and how eff supports programming techniques that use various forms of delimited continuations, such as backtracking, breadth-first search, selection functionals, cooperative multi-threading, and others.},
archivePrefix = {arXiv},
arxivId = {1203.1539},
author = {Bauer, Andrej and Pretnar, Matija},
eprint = {1203.1539},
journal = {ArXiv e-prints},
keywords = {()},
month = mar,
pages = {1--25},
title = {Programming with Algebraic Effects and Handlers},
year = {2012}
}
@book{MacLane1978,
author = {{Mac Lane}, Saunders},
doi = {10.1007/978-1-4757-4721-8},
isbn = {978-1-4419-3123-8},
publisher = {Springer New York},
series = {Graduate Texts in Mathematics},
title = {Categories for the Working Mathematician},
type = {Book},
volume = {5},
year = {1978}
}
@article{Plotkin2004,
author = {Plotkin, Gordon D. and Power, A. John},
doi = {10.1016/j.entcs.2004.08.008},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = oct,
pages = {149--163},
title = {Computational Effects and Operations: An Overview},
volume = {73},
year = {2004}
}
@article{Dunn1995,
author = {Dunn, J. Michael},
doi = {10.1007/BF01061239},
journal = {Stud. Log.},
number = {2},
pages = {301--317},
title = {Positive modal logic},
volume = {55},
year = {1995}
}
@article{Kurz2006a,
author = {Kurz, Alexander},
doi = {10.1145/1140612.1140628},
journal = {SIGACT News},
number = {2},
pages = {57--77},
title = {Coalgebras and their logics},
type = {Journal article},
volume = {37},
year = {2006}
}
@incollection{Adamek2011b,
abstract = {An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as a coproduct of the final coalgebra (considered as an algebra) and with free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Haddadi, Mahdie and Milius, Stefan},
booktitle = {Proceeding CALCO'11 Proc. 4th Int. Conf. Algebr. coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-22944-2_5},
editor = {Corradini, Andrea and Klin, Bartek and C{\^{i}}rstea, Corina},
pages = {55--69},
publisher = {Springer Berlin Heidelberg},
title = {From corecursive algebras to corecursive Monads},
year = {2011}
}
@article{Nakamoto2008,
abstract = {Abstract. A purely peer-to-peer version of electronic cash would allow online payments to be sent directly from one party to another without going through a financial institution. Digital signatures provide part of the solution, but the main benefits are lost if a trusted third party is still required to prevent double-spending. We propose a solution to the double-spending problem using a peer-to-peer network. The network timestamps transactions by hashing them into an ongoing chain of hash-based proof-of-work, forming a record that cannot be changed without redoing the proof-of-work. The longest chain not only serves as proof of the sequence of events witnessed, but proof that it came from the largest pool of CPU power. As long as a majority of CPU power is controlled by nodes that are not cooperating to attack the network, they'll generate the longest chain and outpace attackers. The network itself requires minimal structure. Messages are broadcast on a best effort basis, and nodes can leave and rejoin the network at will, accepting the longest proof-of-work chain as proof of what happened while they were gone.},
archivePrefix = {arXiv},
arxivId = {43543534534v343453},
author = {Nakamoto, Satoshi},
doi = {10.1007/s10838-008-9062-0},
eprint = {43543534534v343453},
isbn = {978-972-757-716-3},
issn = {09254560},
journal = {www.Bitcoin.Org},
pages = {9},
pmid = {14533183},
title = {Bitcoin: A Peer-to-Peer Electronic Cash System},
year = {2008}
}
@inproceedings{Bonchi2014a,
author = {Bonchi, Filippo and Petrişan, Daniela and Pous, Damien and Rot, Jurriaan},
booktitle = {Proc. Jt. Meet. Twenty-Third Annu. Conf. Comput. Sci. Log. Twenty-Ninth Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1145/2603088.2603149},
isbn = {9781450328869},
keywords = {bialgebras,bisimulation up-to,coinductive predicates,fibrations,gsos,nominal automata,similarity,up-to techniques},
title = {Coinduction up-to in a fibrational setting},
year = {2014}
}
@article{Chiribella2018,
abstract = {Dividing the world into subsystems is an important component of the scientific method. The choice of subsystems, however, is not defined a priori. Typically, it is dictated by our experimental capabilities, and, in general, different agents may have different capabilities. Here we propose a construction that associates every agent with a subsystem, equipped with its set of states and its set of transformations. In quantum theory, this construction accommodates the traditional notion of subsystems as factors of a tensor product, as well as the notion of classical subsystems of quantum systems. We then restrict our attention to systems where all physical transformations act invertibly. For such systems, the future states are a faithful encoding of the past states, in agreement with a requirement known as the Conservation of Information. For systems satisfying the Conservation of Information, we propose a dynamical definition of pure states, and show that all the states of all subsystems admit a canonical purification. This result extends the purification principle to a broader setting, in which coherent superpositions can be interpreted as purifications of incoherent mixtures. As an example, we illustrate the general construction for subsystems associated with group representations.},
archivePrefix = {arXiv},
arxivId = {1804.01943},
author = {Chiribella, Giulio},
eprint = {1804.01943},
keywords = {1,2,agent,and in the,and operations is a,commuting subalgebras,conservation of information,fundamental ingredient of our,group representations,in depth in quantum,information theory,it has been investigated,modelling of,purification,subsystem,the composition of systems,the world},
month = apr,
number = {1},
pages = {1--34},
title = {Agents, subsystems, and the conservation of information},
year = {2018}
}
@incollection{Clouston2005,
abstract = {Coalgebras provide effective models of data structures and state-transition systems. A virtual covariety is a class of coalgebras closed under coproducts, images of coalgebraic morphisms, and subcoalgebras defined by split equalisers. A covariety has the stronger property of closure under all subcoalgebras, and is behavioural if it is closed under domains of morphisms, or equivalently under images of bisimulations. There are many computationally interesting properties that define classes of these kinds. We identify conditions on the underlying category of a comonad  which ensure that there is an exact correspondence between (behavioural/virtual) covarieties of  -coalgebras and subcomonads of  defined by comonad morphisms to  with natural categorical properties. We also relate this analysis to notions of coequationally defined classes of coalgebras.},
author = {Clouston, Ranald and Goldblatt, Robert},
booktitle = {Theor. Asp. Comput. – ICTAC 2005},
doi = {10.1007/11560647_19},
editor = {Hung, Dang Van and Wirsing, Martin},
isbn = {978-3-540-29107-7},
pages = {288--302},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Covarieties of Coalgebras : Comonads and Coequations},
year = {2005}
}
@inproceedings{Pin2009,
author = {Pin, Jean-{\'{E}}ric},
booktitle = {26th Int. Symp. Theor. Asp. Comput. Sci.},
doi = {10.4230/LIPIcs.STACS.2009.1856},
editor = {Albers, Susanne and Marion, Jean-Yves},
isbn = {9783939897095},
issn = {18688969},
pages = {31--50},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Profinite methods in automata theory},
volume = {3},
year = {2009}
}
@article{Kozen1988,
abstract = {We prove a finite model theorem and infinitary completeness result for the propositional $\mu$-calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.},
author = {Kozen, Dexter},
doi = {10.1007/BF00370554},
issn = {0039-3215},
journal = {Stud. Log.},
month = sep,
number = {3},
pages = {233--241},
title = {A finite model theorem for the propositional $\mu$-calculus},
volume = {47},
year = {1988}
}
@inproceedings{Gaboardi2013,
abstract = {Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity---how much its result can change when a single record is added or removed. A variety of tools have been developed for certifying that a given query differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation; it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically. We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.},
address = {New York, New York, USA},
author = {Gaboardi, Marco and Haeberlen, Andreas and Hsu, Justin and Narayan, Arjun and Pierce, Benjamin C.},
booktitle = {Proc. 40th Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '13},
doi = {10.1145/2429069.2429113},
isbn = {9781450318327},
issn = {07308566},
keywords = {depen-,differential privacy,linear logic,type systems},
pages = {357},
publisher = {ACM Press},
title = {Linear dependent types for differential privacy},
year = {2013}
}
@article{Abramsky2013a,
abstract = {We use a simple relational framework to develop the key notions and results on hidden variables and non-locality. The extensive literature on these topics in the foundations of quantum mechanics is couched in terms of probabilistic models, and properties such as locality and no-signalling are formulated probabilistically. We show that to a remarkable extent, the main structure of the theory, through the major No-Go theorems and beyond, survives intact under the replacement of probability distributions by mere relations.},
archivePrefix = {arXiv},
arxivId = {1007.2754},
author = {Abramsky, Samson},
doi = {10.1007/s11225-013-9477-4},
eprint = {1007.2754},
isbn = {1122501394774},
issn = {0039-3215},
journal = {Stud. Log.},
keywords = {Hidden variables,Non-locality,Possibilistic models,Probabilistic models,Quantum mechanics},
month = apr,
number = {2},
pages = {411--452},
title = {Relational Hidden Variables and Non-Locality},
volume = {101},
year = {2013}
}
@inproceedings{Daviaud2016,
author = {Daviaud, Laure and Kuperberg, Denis and Pin, Jean-{\'{E}}ric},
booktitle = {Proc. 33rd Int. Symp. Theor. Asp. Comput. Sci.},
doi = {10.4230/LIPIcs.STACS.2016.30},
keywords = {and phrases cost functions,regular language,syntactic algebra,varieties},
pages = {30:1----30:14},
publisher = {Schloss Dagstuhl–Leibniz-Zentrum f{\"{u}}r Informatik},
series = {LIPIcs},
title = {Varieties of cost functions},
volume = {47},
year = {2016}
}
@article{Kelly1993,
abstract = {A right adjoint functor is said to be of descent type if the counit of the adjunction is pointwise a coequalizer. Building on the results of Tholen's doctoral thesis, we give necessary and sufficient conditions for a composite to be of descent type when each factor is so. We apply this to show that every finitary monad on a locally-finitely-presentable enriched category admits a presentation in terms of basic operations and equations between derived operations, the arties here being the finitely-presentable objects of .},
author = {Kelly, Gregory Maxwell and Power, A. John},
doi = {10.1016/0022-4049(93)90092-8},
journal = {J. Pure Appl. Algebr.},
number = {1-2},
pages = {163--179},
title = {Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads},
volume = {89},
year = {1993}
}
@techreport{Jones2017,
author = {Jones, Prof Mark W and Roach, Matt},
title = {Data Aggregation Impacts Report},
year = {2017}
}
@article{Bezhanishvili2015,
author = {Bezhanishvili, Guram and Bezhanishvili, Nick and Harding, John},
doi = {10.1007/s10485-013-9332-9},
isbn = {1048501393329},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
keywords = {06d22,2010,54b20,54e05,b,bezhanishvili,compact hausdorff space,compact regular frame,de vries algebra,g,mathematics subject classifications,modal operator,vietoris space},
number = {3},
pages = {365--379},
title = {Modal Operators on Compact Regular Frames and de Vries Algebras},
volume = {23},
year = {2015}
}
@inproceedings{Corradini1998,
abstract = {This paper relates labeled transition systems and coalgebras with the motivation of comparing and combining their complementary contributions to the theory of concurrent systems. The well-known mismatch between these two notions for what concerns the morphisms is resolved by extending the coalgebraic framework by lax cohomomorphisms. Enriching both labeled transition systems and coalgebras with algebraic structure for an algebraic specification, the correspondence is lost again. This leads to the introduction of lax coalgebras, where the coalgebra structure is given by a lax homomorphism. The resulting category of lax coalgebras and lax cohomomorphisms for a suitable endofunctor is shown to be isomorphic to the category of structured transition systems, where both states and transitions form algebras. The framework is also presented on a more abstract categorical level using monads and comonads, extending the bialgebraic approach recently introduced by Turi and Plotkin. {\textcopyright} 1998 Published by Elsevier Science B.V.},
author = {Corradini, Andrea and Gro{\ss}e-Rhode, Martin and Heckel, Reiko},
booktitle = {First Work. Coalgebraic Methods Comput. Sci.},
doi = {10.1016/S1571-0661(04)00051-9},
issn = {15710661},
pages = {22--41},
title = {Structured transition systems as lax coalgebras},
volume = {11},
year = {1998}
}
@article{Gabbay2002,
abstract = {In this paper we improve the results of [2] by proving the product f.m.p. for the product of minimal n-modal and minimal n-temporal logic. For this case we modify the finite depth method introduced in [1]. The main result is applied to identify new fragments of classical first-order logic and of the equational theory of relation algebras, that are decidable and have the finite model property.},
author = {Gabbay, Dov and Shehtman, Valentin},
doi = {10.1023/A:1021304426509},
journal = {Stud. Log.},
keywords = {classical first-order logic,decidability,finite depth method,finite model property,product finite model property,product of modal logics,relation algebra,temporal logic},
number = {2},
pages = {157--183},
publisher = {Kluwer Academic Publishers},
title = {Products of Modal Logics. Part 3: Products of Modal and Temporal Logics},
volume = {72},
year = {2002}
}
@article{Goguen1975,
abstract = {This paper develops a minimal realization theory for discrete-time machines with structure in a suitable closed monoidal category. By specifying the category a number of applications arise, most of them new. Minimal realization is stated as an adjunction between an input-output behavior functor and a realization functor. The very existence of an adjunction yields several new structural results on minimal realization. As preliminaries, certain aspects of categorical algebra are reviewed, and a theory of discrete-time transition systems is developed. The concept of an X-module and an initial object theorem are especially important. A number of examples of suitable categories is given, but discussion of the resulting machine theories is deferred to a subsequent paper. {\textcopyright} 1975 Academic Press, Inc.},
author = {Goguen, J. a.},
doi = {10.1016/S0022-0000(75)80012-2},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
pages = {1--43},
title = {Discrete-time machines in closed monoidal categories. I},
volume = {10},
year = {1975}
}
@article{Ulmer1968,
author = {Ulmer, Friedrich},
doi = {10.1016/0021-8693(68)90036-7},
issn = {00218693},
journal = {J. Algebr.},
month = jan,
number = {1},
pages = {77--95},
title = {Properties of dense and relative adjoint functors},
volume = {8},
year = {1968}
}
@article{Brengos2014,
abstract = {In the first part of the paper we recall the coalgebraic approach to handling the so-called invisible transitions that appear in different state-based systems semantics. We claim that these transitions are always part of the unit of a certain monad. Hence, coalgebras with internal moves are exactly coalgebras over a monadic type. The rest of the paper is devoted to supporting our claim by studying two important behavioural equivalences for state-based systems with internal moves, namely: weak bisimulation and trace semantics. We continue our research on weak bisimulations for coalgebras over order enriched monads. The key notions used in this paper and proposed by us in our previous work are the notions of an order saturation monad and a saturator. A saturator operator can be intuitively understood as a reflexive, transitive closure operator. There are two approaches towards defining saturators for coalgebras with internal moves. Here, we give necessary conditions for them to yield the same notion of weak bisimulation. Finally, we propose a definition of trace semantics for coalgebras with silent moves via a uniform fixed point operator. We compare strong and weak bisimilation together with trace semantics for coalgebras with internal steps.},
archivePrefix = {arXiv},
arxivId = {1402.6281},
author = {Brengos, Tomasz},
eprint = {1402.6281},
journal = {ArXiv e-prints},
keywords = {bisimulation,coalgebra,conway operator,epsilon transition,fixed,internal transition,logic,monad,point operator,saturation,tics,trace,trace seman-,traced monoidal category,uniform fixed point operator,van glabbeek spectrum,weak bisimulation,weak trace semantics},
month = feb,
number = {504},
pages = {23},
title = {On coalgebras with internal moves},
year = {2014}
}
@article{McLarty1986,
author = {McLarty, Colin},
doi = {10.1016/0022-4049(86)90100-3},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jan,
pages = {63--66},
title = {Left exact logic},
volume = {41},
year = {1986}
}
@incollection{Muralidhar2010,
abstract = {The concept of differential privacy was motivated through the example of Terry Gross' height in Dwork (2006). In this paper, we show that when a procedure based on differential privacy is implemented, it neither protects Terry Gross' privacy nor does it provide meaningful responses to queries. We also provide an additional illustration using income data from the US Census. These illustrations raise serious questions regarding the efficacy of using differential privacy based masking mechanism for numerical data.},
author = {Muralidhar, Krish and Sarathy, Rathindra},
booktitle = {Priv. Stat. Databases},
doi = {10.1007/978-3-642-15838-4_18},
editor = {Domingo-Ferrer, Josep and Magkos, Emmanouil},
isbn = {3642158374},
issn = {03029743},
keywords = {Differential privacy,Laplace noise addition,Numerical data},
pages = {200--209},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Does Differential Privacy Protect Terry Gross' Privacy?},
volume = {6344},
year = {2010}
}
@article{Ellerman2014,
abstract = {Classical logic is usually interpreted as the logic of propositions. But from Boole's original development up to modern categorical logic, there has always been the alternative interpretation of classical logic as the logic of subsets of any given (nonempty) universe set. Partitions on a universe set are dual to subsets of a universe set in the sense of the reverse-the-arrows category-theoretic duality--which is reflected in the duality between quotient objects and subobjects throughout algebra. Hence the idea arises of a dual logic of partitions. That dual logic is described here. Partition logic is at the same mathematical level as subset logic since models for both are constructed from (partitions on or subsets of) arbitrary unstructured sets with no ordering relations, compatibility or accessibility relations, or topologies on the sets.\r\nJust as Boole developed logical finite probability theory as a quantitative treatment of subset logic, applying the analogous mathematical steps to partition logic yields a logical notion of entropy so that information theory can be refounded on partition logic. But the biggest application is that when partition logic and the accompanying logical information theory are "lifted" to complex vector spaces, then the mathematical framework of quantum mechanics is obtained. Partition logic models indefiniteness (i.e., numerical attributes on a set become more definite as the inverse-image partition becomes more refined) while subset logic models the definiteness of classical physics (an entity either definitely has a property or definitely does not). Hence partition logic provides the backstory so the old idea of "objective indefiniteness" in QM can be fleshed out to a full interpretation of quantum mechanics.},
author = {Ellerman, David},
doi = {10.1093/jigpal/jzt036},
issn = {1367-0751},
journal = {Log. J. IGPL},
keywords = {Logical entropy,Partition logic,Partition tautologies,Quantum mechanics,Subset logic,Subset-partition duality},
month = feb,
number = {1},
pages = {94--125},
title = {An introduction to partition logic},
volume = {22},
year = {2014}
}
@article{Jay1988,
abstract = {The concept of a local adjunction between bicategories A and B focuses on a family of adjunctions. B(FA, B)???A(A, GB) between hom-categories; hence the name local adjunction. When bicategories of spans, or (bi-)modules for some monoidal category are created, ordinary adjunctions induce local adjunctions between the resulting bicategories. Other examples include bi-adjunctions, lax adjunctions, strict quasi-adjunctions and monoidal adjunctions. ?? 1988.},
author = {Jay, C. Barry},
doi = {10.1016/0022-4049(88)90124-7},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = sep,
number = {3},
pages = {227--238},
title = {Local adjunctions},
volume = {53},
year = {1988}
}
@article{Goldreich1991,
abstract = {In this paper the generality and wide applicability of Zero-knowledge\nproofs, a notion introduced by Goldwasser, Micali, and Rackoff is\ndemonstrated. These are probabilistic and interactive proofs that,\nfor the members of a language, efficiently demonstrate membership\nin the language without conveying any additional knowledge. All previously\nknown zero-knowledge proofs were only for number-theoretic languages\nin NP fl CONP.\n\nUnder the assumption that secure encryption functions exist or by\nusing “physical means for hiding information, ‘‘ it is shown that\nall languages in NP have zero-knowledge proofs. Loosely speaking,\nit is possible to demonstrate that a CNF formula is satisfiable without\nrevealing any other property of the formula, in particular, without\nyielding neither a satis@ing assignment nor properties such as whether\nthere is a satisfying assignment in which xl = X3 etc.\n\nIt is also demonstrated that zero-knowledge proofs exist “outside\nthe domain of cryptography and number theory. ” Using no assumptions.\nit is shown that both graph isomorphism and graph nonisomorphism\nhave zero-knowledge interactive proofs. The mere existence of an\ninteractive proof for graph nonisomorphism is interesting, since\ngraph nonisomorphism is not known to be in NP and hence no efficient\nproofs were known before for demonstrating that two graphs are not\nisomorphic.},
author = {Goldreich, Oded and Micali, Silvio and Wigderson, Avi},
doi = {10.1145/116825.116852},
isbn = {0004-5411},
issn = {00045411},
journal = {J. ACM},
keywords = {Journal of the ACM},
number = {3},
pages = {690--728},
title = {Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems},
volume = {38},
year = {1991}
}
@article{Bloom1997,
abstract = {This paper is concerned with the questions of the existence or the construction of ﬁxed points. We are concerned with the properties of ﬁxed point solutions, especially equational properties.},
author = {Bloom, Stephen L. and {\'{E}}sik, Zolt{\'{a}}n},
doi = {10.1016/S0304-3975(96)00248-4},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = jun,
number = {1-2},
pages = {1--60},
title = {The equational logic of fixed points},
volume = {179},
year = {1997}
}
@article{Sweeney2002a,
author = {Sweeney, Latanya},
doi = {10.1142/S0218488502001648},
journal = {Int. J. Uncertainty, Fuzziness Knowledge-Based Syst.},
number = {05},
pages = {557--570},
title = {$k$-Anonymity: A model for protecting Privacy},
volume = {10},
year = {2002}
}
@article{Schwichtenberg1976,
author = {Schwichtenberg, H.},
journal = {Arch. Logik Grundlagenforsch.},
pages = {113--114},
title = {Definierbare Funktionen im Lambda-Kalkul mit Typen},
volume = {17},
year = {1976}
}
@incollection{Antoniou2001,
author = {Antoniou, Grigoris and Billington, David},
booktitle = {AI 2001 Adv. Artif. Intell.},
doi = {10.1007/3-540-45656-2_2},
editor = {Stumptner, Markus and Corbett, Dan and Brooks, Mike},
isbn = {9783540429609},
issn = {16113349},
pages = {13--24},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Relating Defeasible and Default Logic},
volume = {2256},
year = {2001}
}
@article{Roelleke2008,
abstract = {This paper presents a probabilistic relational modelling (implementation) of the major probabilistic retrieval models. Such a high-level implementation is useful since it supports the ranking of any object, it allows for the reasoning across structured and unstructured data, and it gives the software (knowledge) engineer control over ranking and thus supports customisation. The contributions of this paper include the specification of probabilistic SQL (PSQL) and probabilistic relational algebra (PRA), a new relational operator for probability estimation (the relational Bayes), the probabilistic relational modelling of retrieval models, a comparison of modelling retrieval with traditional SQL versus modelling retrieval with PSQL, and a comparison of the performance of probability estimation with traditional SQL versus PSQL. The main findings are that the PSQL/PRA paradigm allows for the description of advanced retrieval models, is suitable for solving large-scale retrieval tasks, and outperforms traditional SQL in terms of abstraction and performance regarding probability estimation.},
author = {Roelleke, Thomas and Wu, Hengzhi and Wang, Jun and Azzam, Hany},
doi = {10.1007/s00778-007-0073-y},
issn = {1066-8888},
journal = {VLDB J.},
keywords = {DB + IR integration,Probabilistic databases,Probabilistic relational modelling,Retrieval models},
month = nov,
number = {1},
pages = {5--37},
title = {Modelling retrieval models in a probabilistic relational algebra with a new operator: the relational Bayes},
volume = {17},
year = {2008}
}
@incollection{Honda2014,
abstract = {Session types are types for distributed communicating pro- cesses. They were born from process encodings of data structures and typical interaction scenarios in an asynchronous version of the $\pi$-calculus, and are being studied and developed as a potential basis for structuring concurrent and distributed computing, as well as in their own right. In this paper, we introduce basic ideas of sessions and session types, outline their key technical elements, and discuss how they may be usable for programming, drawing from our experience and comparing with existing paradigms, especially concurrent objects such as actors. We discuss how session types can offer a programming framework in which communica- tions are structured both in program text and at run-time.},
author = {Honda, Kohei and Hu, Raymond and Neykova, Rumyana and Chen, Tzu-chun and Demangeon, Romain and Deni{\'{e}}lou, Pierre-malo and Yoshida, Nobuko},
booktitle = {Concurr. Objects Beyond Pap. Dedic. to Akinori Yonezawa Occas. His 65th Birthd.},
doi = {10.1007/978-3-662-44471-9_5},
isbn = {978-3-662-44471-9},
issn = {16113349},
pages = {105--127},
title = {Structuring Communication with Session Types},
year = {2014}
}
@inproceedings{Pretnar2015,
author = {Pretnar, Matija},
booktitle = {MFPS XXXI},
keywords = {16,18,a set of operations,algebraic effects,algebraic effects are an,approach to computational effects,based on a premise,effect system,handlers,impure behaviour arises from,logic,or raise for exceptions,output,print for interactive input,read,semantics,set for mutable store,such as get,that,this nat-,tutorial},
title = {An Introduction to Algebraic Effects and Handlers Invited tutorial paper},
year = {2015}
}
@incollection{Chen2012,
abstract = {Probabilistic bisimilarity is a fundamental notion of equivalence on labelled Markov chains. It has a natural generalisation to a probabilistic bisimilarity pseudometric, whose definition involves the Kantorovich metric on probability distributions. The pseudometric has discounted and undiscounted variants, according to whether one discounts the future in observing discrepancies between states. This paper is concerned with the complexity of computing probabilistic bisimilarity and the probabilistic bisimilarity pseudometric on labelled Markov chains. We show that the problem of computing probabilistic bisimilarity is P -hard by reduction from the monotone circuit value problem. We also show that the discounted pseudometric is rational and can be computed exactly in polynomial time using the network simplex algorithm and the continued fraction algorithm. In the undiscounted case we show that the pseudometric is again rational and can be computed exactly in polynomial time using the ellipsoid algorithm. Finally, using the notion of couplings on Markov chains, we show that the pseudometric can be used to compute bounds on the variational distance of trace distributions, which is NP -hard to compute directly.},
author = {Chen, Di and van Breugel, Franck and Worrell, James},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {437--451},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On the Complexity of Computing Probabilistic Bisimilarity},
volume = {7213},
year = {2012}
}
@article{Ward1977,
abstract = {It is shown that, for the discrete space X of positive integers, V$\omega$;X (= V$\beta$X) is not naturally homeomorphic either to \\aeVX or to $\beta$VX (V, $\omega$ and $\beta$ denoting the Vietoris, Wallman and Stone- \\v Cech operators respectively). The example gives a negative answer to two problems recently posed by A. G. Hitchcock, and also disproves a statement attributed by him to V. M. lvanova.},
author = {Ward, A. J.},
doi = {10.1112/jlms/s2-16.3.539},
journal = {J. London Math. Soc.},
number = {3},
pages = {539--540},
title = {The Stone-{\v{C}}ech and Vietoris Operators are not Commutative},
type = {Journal article},
volume = {s2-16},
year = {1977}
}
@inproceedings{Wadler1989,
address = {New York, NY, USA},
author = {Wadler, Philip},
booktitle = {Proc. 4th Int. Conf. Funct. Program. Lang. Comput. Archit.},
doi = {10.1145/99370.99404},
isbn = {0897913280},
pages = {347--359},
publisher = {ACM Press},
title = {Theorems for free!},
year = {1989}
}
@article{Lack,
archivePrefix = {arXiv},
arxivId = {arXiv:0802.1946v2},
author = {Lack, Stephen},
doi = {10.1007/s10485-008-9167-y},
eprint = {arXiv:0802.1946v2},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
month = oct,
number = {1},
pages = {17--29},
title = {Note on the Construction of Free Monoids},
volume = {18},
year = {2008}
}
@incollection{Johnstone1978,
author = {Johnstone, Peter T. and Wraith, Gavin C.},
booktitle = {Index. Categ. Their Appl.},
doi = {10.1007/BFb0061360},
isbn = {978-3-540-08914-8},
pages = {141--242},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Algebraic theories in toposes},
year = {1978}
}
@incollection{Melton1982,
abstract = {For any category K we investigate the family of all factorization structures on K . In particular, for each such structure, (E,M), we investigate the complete lattice of all factorization structures on K with left factor a subclass of E; this investigation is based on a Galois connection between all such structures and the lattice of all full isomorphism-closed subcategories of K . The Galois-closed families are precisely all the E-reflective subcategories of K and all the (E,M)-dispersed factorization structures of Herrlich, Salicrup and Vazquez.},
author = {Melton, Austin C. and Strecker, George E. and Kamps, Klaus and Pumpl{\"{u}}n, Dieter and Tholen, Walter},
booktitle = {Categ. Theory},
doi = {10.1007/BFb0066878},
editor = {Kamps, Klaus Heiner and Pumpl{\"{u}}n, Dieter and Tholen, Walter},
isbn = {978-3-540-11961-6},
keywords = {Mathematics and Statistics},
pages = {197--208},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {On the structure of factorization structures},
volume = {962},
year = {1982}
}
@inproceedings{Pavlovic1998,
author = {Pavlovic, D. and Escardo, M.H.},
booktitle = {Proceedings. Thirteen. Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.1998.705675},
isbn = {0-8186-8506-9},
pages = {408--417},
publisher = {IEEE Comput. Soc},
title = {Calculus in coinductive form},
year = {1998}
}
@article{Rosicky1981,
author = {Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1016/0022-4049(81)90105-5},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {3},
pages = {309--339},
title = {Concrete categories and infinitary languages},
volume = {22},
year = {1981}
}
@article{Uustalu2016,
author = {Uustalu, Tarmo},
doi = {10.1016/j.jlamp.2016.06.004},
issn = {23522208},
journal = {J. Log. Algebr. Methods Program.},
number = {5},
pages = {1086--1094},
publisher = {Elsevier Inc.},
title = {A divertimento on MonadPlus and nondeterminism},
volume = {85},
year = {2016}
}
@article{Abel2005,
address = {New York, New York, USA},
author = {Abel, Andreas M. and Benke, Marcin and Bove, Ana and Hughes, John and Norell, Ulf},
doi = {10.1145/1088348.1088355},
isbn = {159593071X},
journal = {Proc. 2005 ACM SIGPLAN Work. Haskell - Haskell '05},
keywords = {ghc core,haskell,monadic transla-,partiality,tion,type theory,verification},
pages = {62--73},
publisher = {ACM Press},
title = {Verifying haskell programs using constructive type theory},
year = {2005}
}
@article{Urabe2017,
abstract = {We introduce notions of simulation between semiring-weighted automata as models of quantitative systems. Our simulations are instances of the categorical/coalgebraic notions previously studied by Hasuo—hence soundness against language inclusion comes for free—but are concretely presented as matrices that are subject to linear inequality constraints. Pervasiveness of these formalisms allows us to exploit existing algorithms in: searching for a simulation, and hence verifying quantitative correctness that is formulated as language inclusion. Transformations of automata that aid search for simulations are introduced, too. This verification workflow is implemented for the plus-times and max-plus semirings. Furthermore, an extension to weighted tree automata is presented and implemented.},
author = {Urabe, Natsuki and Hasuo, Ichiro},
doi = {10.1016/j.ic.2016.03.007},
issn = {10902651},
journal = {Inf. Comput.},
keywords = {Kleisli category,Language inclusion,Simulation,Tropical semiring,Weighted automaton},
month = feb,
number = {Concur 2014},
pages = {110--137},
publisher = {Elsevier Inc.},
title = {Quantitative simulations by matrices},
volume = {252},
year = {2017}
}
@book{Hobby1988,
author = {Hobby, David and McKenzie, Ralph},
doi = {10.1090/conm/076},
publisher = {American Mathematical Society},
series = {Contemporary Mathematics},
title = {The Structure of Finite Algebras},
year = {1988}
}
@incollection{Ryan2001,
abstract = {In this chapter I present a process algebraic approach to the modelling of security properties and policies. I will concentrate on the concept of secrecy, also known as confidentiality, and in particular on the notion of non-interference. Non-interference seeks to characterise the absence of information flows through a system and, as such, is a fundamental concept in information security. A central thesis of these lectures is that, viewed from a process algebraic point of view, the problem of characterising non-interference is essentially equivalent to that of characterising the equivalence of processes. The latter is itself a fundamental and delicate question at the heart of process algebra and indeed theoretical computer science: the semantics of a process is intimately linked to the question of which processes should be regarded as equivalent. We start, by way of motivation and to set the context, with a brief historical background. A much fuller exposition of security policies in the wider sense, embracing properties other than secrecy, can be found in the chapter by Pierangela Samarati in this volume. We then cover some elements of process algebra, in particular CSP (Communicating Sequential Processes), that we need and present a formulation of noninterference, along with some more operational presentations of process algebra, including the idea of bi-simulation. I argue that the classical notion of unwinding found in the security literature is really just bisimulation in another guise. Finally, I propose some generalisations of the process algebraic formulations designed to encompass a richer class of policies and examples.},
author = {Ryan, Peter Y. A.},
booktitle = {Found. Secur. Anal. Des. Tutor. Lect.},
doi = {10.1007/3-540-45608-2_1},
isbn = {978-3-540-45608-7},
pages = {1--62},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Mathematical models of computer security},
volume = {2171},
year = {2001}
}
@article{Kerstan2013,
archivePrefix = {arXiv},
arxivId = {1310.7417},
author = {Jacobs, Bart},
doi = {10.2168/LMCS-9(3:23)2013},
editor = {Klin, Bartek},
eprint = {1310.7417},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {Coalgebra,Markov processes,Probabilistic transition systems,Trace semantics},
month = sep,
number = {3},
pages = {1--21},
title = {Bases as Coalgebras},
volume = {9},
year = {2013}
}
@inproceedings{Jacobs2015a,
author = {Jacobs, Bart},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci. (CALCO 2015)},
doi = {10.4230/LIPIcs.CALCO.2015.116},
editor = {Sobocinski, Lawrence S. Moss and Pawel},
isbn = {9783939897842},
issn = {18688969},
keywords = {and phrases duality,predicate transformer,state transformer,state-and-effect tri-},
pages = {116--129},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {A recipe for state-and-effect triangles},
volume = {35},
year = {2015}
}
@article{Ulidowski2004,
author = {Plotkin, Gordon D.},
doi = {10.1016/j.jlap.2004.05.001},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
month = jul,
pages = {17--139},
title = {A structural approach to operational semantics},
volume = {60-61},
year = {2004}
}
@incollection{Shenoy1990a,
author = {Shenoy, Prakash P. and Shafer, Glenn},
booktitle = {Uncertain. Artif. Intell. 4},
doi = {10.1016/B978-0-444-88650-7.50019-6},
editor = {Shachter, Ross D. and Levitt, Tod S. and Kanal, Laveen N. and Lemmer, John F.},
issn = {0923-0459},
pages = {169--198},
publisher = {North-Holland},
series = {Machine Intelligence and Pattern Recognition},
title = {Axioms for Probability and Belief-Function Propagation},
volume = {9},
year = {1990}
}
@book{Jech2003,
author = {Jech, Thomas},
doi = {10.1007/3-540-44761-X},
edition = {3rd rev.},
isbn = {978-3-540-44085-7},
publisher = {Springer Berlin Heidelberg},
series = {Springer Monographs in Mathematics},
title = {Set Theory},
year = {2003}
}
@article{Street1980,
author = {Street, Ross},
doi = {10.1090/S0002-9947-1980-0558176-3},
issn = {0002-9947},
journal = {Trans. Am. Math. Soc.},
keywords = {cartesian closed,category,fibred,gabriel theory,internal full subcategory,internally complete,locally presentable category,locally small,multiple,site,sketched structures},
month = feb,
number = {2},
pages = {271--271},
title = {Cosmoi of internal categories},
volume = {258},
year = {1980}
}
@inproceedings{Lane2012,
abstract = {Underpinning many recent advances in sensing applications (e.g., mHealth) is the ability to safely collect and share mobile sensor data. Research has shown that even from seemingly harmless sensors (e.g., accelerometers, gyroscopes, or magnetometers) an ever expanding set of potentially sensitive user behavior can be inferred. Providing robust anonymity assurances is a principal mechanism for protecting users when data is shared (e.g., with medical professionals or friends). In this paper, we study the feasibility of user de-anonymization from mobile sensor datasets routinely collected on commodity devices (e.g., smartphones). We perform a systematic investigation to quantify the threat of de-anonymization using existing sparsity-based techniques adapted to exploit mobile sensor data characteristics. This preliminary study indicates significant threats to user anonymity exist within shared mobile sensor data and further investigation is warranted.},
address = {New York, New York, USA},
author = {Lane, Nicholas D. and Xie, Junyuan and Moscibroda, Thomas and Zhao, Feng},
booktitle = {Proc. Third Int. Work. Sens. Appl. Mob. Phones - PhoneSense '12},
doi = {10.1145/2389148.2389151},
isbn = {9781450317788},
pages = {1--5},
publisher = {ACM Press},
title = {On the feasibility of user de-anonymization from shared mobile sensor data},
year = {2012}
}
@inproceedings{Leal2008,
author = {Leal, Raul Andres},
booktitle = {Proc. Ninth Work. Coalgebraic Methods Comput. Sci.},
doi = {10.1016/j.entcs.2008.05.026},
issn = {15710661},
keywords = {coalgebra,logical translator,modal logic,modality,moss,predicate lifting,singleton lifting},
number = {5},
pages = {195--220},
publisher = {Elsevier},
series = {ENTCS},
title = {Predicate Liftings Versus Nabla Modalities},
volume = {203},
year = {2008}
}
@incollection{Venema2014,
author = {Venema, Yde},
booktitle = {Johan van Benthem Log. Inf. Dyn.},
doi = {10.1007/978-3-319-06025-5_2},
editor = {Baltag, Alexandru and Smets, Sonja},
isbn = {978-3-319-06024-8},
pages = {33--65},
publisher = {Springer International Publishing},
series = {Outstanding Contributions to Logic},
title = {Expressiveness Modulo Bisimilarity: A Coalgebraic Perspective},
volume = {5},
year = {2014}
}
@article{Pawlak2007,
abstract = {Worldwide, there has been a rapid growth in interest in rough set theory and its applications in recent years. Evidence of this can be found in the increasing number of high-quality articles on rough sets and related topics that have been published in a variety of international journals, symposia, workshops, and international conferences in recent years. In addition, many international workshops and conferences have included special sessions on the theory and applications of rough sets in their programs. Rough set theory has led to many interesting applications and extensions. It seems that the rough set approach is fundamentally important in artificial intelligence and cognitive sciences, especially in research areas such as machine learning, intelligent systems, inductive reasoning, pattern recognition, mereology, knowledge discovery, decision analysis, and expert systems. In the article, we present the basic concepts of rough set theory and point out some rough set-based research directions and applications. {\textcopyright} 2006 Elsevier Inc. All rights reserved.},
author = {Pawlak, Zdzis{\l}aw and Skowron, Andrzej},
doi = {10.1016/j.ins.2006.06.003},
isbn = {0020-0255},
issn = {00200255},
journal = {Inf. Sci. (Ny).},
keywords = {(in)Discernibility,Approximation spaces,Boolean reasoning,Decision rules,Dependencies of attributes,Information and decision systems,Reducts,Rough membership functions,Rough sets,Set approximations,Vague concepts},
month = jan,
number = {1},
pages = {3--27},
pmid = {22796804},
title = {Rudiments of rough sets},
volume = {177},
year = {2007}
}
@article{Zangurashvili1999,
abstract = {Several results on the translation of factorization systems along adjunctions are proved. The first of these results is the answer to the question posed by G.Janelidze.},
author = {Zangurashvili, Dali},
doi = {10.1023/A:1022180801295},
issn = {1072-947X},
journal = {Georg. Math. J.},
keywords = {Mathematics and Statistics},
month = mar,
number = {2},
pages = {191--200},
publisher = {Springer Netherlands},
title = {Factorization Systems and Adjunctions},
volume = {6},
year = {1999}
}
@phdthesis{Battenfeld2008,
author = {Battenfeld, Ingo},
keywords = {Computational Effects,Computer Science,Denotational Semantics,Domain Theory,Topology},
pages = {174},
school = {University of Edinburgh},
title = {Topological domain theory},
year = {2008}
}
@article{Zangurashvili2004,
author = {Zangurashvili, Dali},
journal = {Theory Appl. Categ.},
number = {11},
pages = {326--354},
title = {Several constructions for factorization systems},
volume = {12},
year = {2004}
}
@incollection{Jacobs2011,
author = {Jacobs, Bart and Rutten, Jan J.M.M.},
booktitle = {Adv. Top. bisimulation coinduction},
editor = {Sangiorgi, Davide and Rutten, Jan J.M.M.},
isbn = {9781107004979},
pages = {38--99},
publisher = {Cambridge University Press},
series = {Cambridge Tracts in Theoretical Computer Science},
title = {An introduction to (co)algebra and (co)induction},
year = {2011}
}
@incollection{Rot2013,
abstract = {Bisimulation-up-to enhances the bisimulation proof method for process equivalence. We present its generalization from labelled transition systems to arbitrary coalgebras, and show that for a large class of systems, enhancements such as bisimulation up to bisimilarity, up to equivalence and up to context are sound proof techniques. This allows for simplified bisimulation proofs for many different types of state-based systems.},
author = {Rot, Jurriaan and Bonsangue, Marcello M. and Rutten, Jan J.M.M.},
booktitle = {SOFSEM 2013 Theory Pract. Comput. Sci.},
doi = {10.1007/978-3-642-35843-2_32},
editor = {{van Emde Boas}, Peter and Groen, Frans C. A. and F., Italiano Giuseppe and Nawrocki, Jerzy and Sack, Harald},
pages = {1--13},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Coalgebraic Bisimulation-up-to},
year = {2013}
}
@book{Emerson2001,
abstract = {In this paper, we consider the model checking problem for the $\mu$-calculus and show that it is succinctly equivalent to the non-emptiness problem of finite-state automata on infinite binary trees with the parity acceptance condition. We also present efficient model checking algorithms for two rich subclasses of the $\mu$-calculus formulas and relate their expressive power to well-known extensions of branching time temporal logics. {\textcopyright} 2001 Elsevier Science B.V. All rights reserved.},
author = {Emerson, E. Allen and Jutla, Charanjit S. and Sistla, A. Prasad},
booktitle = {Theor. Comput. Sci.},
doi = {10.1016/S0304-3975(00)00034-7},
isbn = {0036580650199},
issn = {03043975},
keywords = {Expressiveness,Model checking,Temporal logic,Tree automata,$\mu$-calculus},
number = {1-2},
pages = {491--522},
title = {On model checking for the $\mu$-calculus and its fragments},
volume = {258},
year = {2001}
}
@article{Adamek2015a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Moss, Lawrence S. and Urbat, Henning},
doi = {10.1016/j.jcss.2014.12.002},
journal = {J. Comput. Syst. Sci.},
keywords = {Finitary functors,Hausdorff functor,presentation of functors},
number = {5},
pages = {813--833},
title = {On finitary functors and their presentations},
volume = {81},
year = {2015}
}
@article{Street1978,
author = {Street, Ross and Walters, Robert},
doi = {10.1016/0021-8693(78)90160-6},
issn = {00218693},
journal = {J. Algebr.},
number = {1978},
pages = {350--379},
title = {Yoneda structures on 2-categories},
volume = {50},
year = {1978}
}
@article{Vardi2007,
author = {Vardi, Moshe Y},
doi = {10.1007/978-3-642-01702-5_2},
isbn = {978-3-540-69735-0},
issn = {03029743},
journal = {Hardw. Softw. Verif. Test.},
pages = {137--150},
title = {Automata-theoretic model checking revisited},
volume = {5394},
year = {2007}
}
@article{Alur1994,
abstract = {We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words–infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both B{\"{u}}chi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable ($\Pi$11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.},
author = {Alur, Rajeev and Dill, David L.},
doi = {10.1016/0304-3975(94)90010-8},
isbn = {0304-3975},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = apr,
number = {2},
pages = {183--235},
title = {A theory of timed automata},
volume = {126},
year = {1994}
}
@article{Machanavajjhala2007,
author = {Machanavajjhala, Ashwin and Kifer, Daniel and Gehrke, Johannes and Venkitasubramaniam, Muthuramakrishnan},
doi = {10.1145/1217299.1217302},
issn = {15564681},
journal = {ACM Trans. Knowl. Discov. Data},
month = mar,
number = {1},
pages = {3},
title = {$l$-diversity: Privacy Beyond $k$-Anonymity},
volume = {1},
year = {2007}
}
@article{Barak2012,
abstract = {Informally, an obfuscator O is an (efficient, probabilistic) " compiler " that takes as input a program (or circuit) P and produces a new program O(P) that has the same functionality as P yet is " unintel-ligible " in some sense. Obfuscators, if they exist, would have a wide vari-ety of cryptographic and complexity-theoretic applications, ranging from software protection to homomorphic encryption to complexity-theoretic analogues of Rice's theorem. Most of these applications are based on an interpretation of the " unintelligibility " condition in obfuscation as mean-ing that O(P) is a " virtual black box, " in the sense that anything one can efficiently compute given O(P), one could also efficiently compute given oracle access to P . In this work, we initiate a theoretical investigation of obfuscation. Our main result is that, even under very weak formalizations of the above in-tuition, obfuscation is impossible. We prove this by constructing a family of functions F that are inherently unobfuscatable in the following sense: there is a property $\pi$ : F → {0, 1} such that (a) given any program that computes a function f ∈ F, the value $\pi$(f) can be efficiently computed, yet (b) given oracle access to a (randomly selected) function f ∈ F, no efficient algorithm can compute $\pi$(f) much better than random guessing. We extend our impossibility result in a number of ways, including even obfuscators that (a) are not necessarily computable in polynomial time, (b) only approximately preserve the functionality, and (c) only need to work for very restricted models of computation (TC 0). We also rule out several potential applications of obfuscators, by constructing " unob-fuscatable " signature schemes, encryption schemes, and pseudorandom function families.},
author = {Barak, Boaz and Goldreich, Oded and Impagliazzo, Russell and Rudich, Steven and Sahai, Amit and Vadhan, Salil and Yang, Ke},
doi = {10.1145/2160158.2160159},
isbn = {3540424563},
issn = {00045411},
journal = {J. ACM},
month = apr,
number = {2},
pages = {1--48},
title = {On the (im)possibility of obfuscating programs},
volume = {59},
year = {2012}
}
@phdthesis{Holohan2016,
author = {Holohan, Naoise},
school = {Trinity College Dublin},
title = {Mathematical Foundations of Differential Privacy},
year = {2016}
}
@article{Harmanec1996,
author = {Harmanec, David and Klir, George J and Wang, Zhenyuan},
doi = {10.1016/0888-613X(95)00111-S},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {1,belief,dempster-shafer theory,dempster-shafer theory and,especially,i n t r,measures,modal logic,necessity measures,o d u c,plausibility measures,possibility measures,possibility the-,possibility theory,t i o n,the idea of connecting},
month = feb,
number = {2-3},
pages = {81--93},
title = {Modal logic interpretation of Dempster-Shafer theory: An infinite case},
volume = {14},
year = {1996}
}
@article{Freyd2008,
author = {Freyd, Peter},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Algebraic real analysis,Chromatic scale,Closed interval,Closed midpoint algebra,Coalgebraic real analysis,Complete scale,Finitely presented scale,Free scale,Harmonic scale,Injective scale,Lattice-ordered abelian group,Linear logic,Lipschitz extension},
number = {10},
pages = {215--306},
title = {Algebraic real analysis},
volume = {20},
year = {2008}
}
@incollection{Bezhanishvili2012a,
author = {Bezhanishvili, Nick and Kupke, Clemens and Panangaden, Prakash},
booktitle = {Work. Logic, Lang. Inf. Comput.},
doi = {10.1007/978-3-540-73445-1_5},
editor = {Ong, Luke and de Queiroz, Ruy},
pages = {191--205},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Minimization via duality},
year = {2012}
}
@article{Adamek2003,
abstract = {Continuous endofunctors F of locally finitely presentable categories carry a natural metric on their final coalgebra. Whenever F(0) has an element, this metric is proved to be a Cauchy completion of the initial algebra of F. This is illustrated on the poset of real numbers represented as a final coalgebra of an endofunctor of Pos by Pavlovi{\'{c}} and Pratt. Under additional assumptions on the locally finitely presentable category, all finitary endofunctors are proved to have a final coalgebra constructed in $\omega$+$\omega$ steps of the natural iteration construction.},
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
doi = {10.1016/S0304-3975(01)00240-7},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {cauchy completion,complete metric space,continuous functor,final coalgebra},
month = feb,
number = {1-2},
pages = {3--29},
title = {On final coalgebras of continuous functors},
volume = {294},
year = {2003}
}
@book{Burris1981,
author = {Burris, Stanley and Sankappanavar, H. P.},
isbn = {3-540-90578-2},
issn = {00029890},
month = jan,
pages = {276},
publisher = {Springer},
title = {A Course in Universal Algebra},
year = {1981}
}
@incollection{Dubuco1968,
author = {Dubuc, Eduardo J.},
booktitle = {Reports Midwest Categ. Semin. II},
doi = {10.1007/BFb0077113},
editor = {{Mac Lane}, Saunders},
isbn = {978-3-540-04231-0},
pages = {69--91},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Adjoint triangles},
volume = {61},
year = {1968}
}
@phdthesis{Velebil1998,
author = {Velebil, Jiř{\'{i}}},
pages = {142},
school = {Czech Technical University},
title = {Categorical Domain Theory},
year = {1998}
}
@incollection{Jacobs2002a,
abstract = {An introduction to coalgebraic specification is presented via examples. A coalgebralc specification describes a collection of coalgebras satisfying certain assertions. It is thus an axiomatic description of a particular class of mathematical structures. Such specifications are especially suitable for state-based dynamical systems in general, and for classes in object-oriented programming languages in particular. This chapter will gradually introduce the notions of bisimilarity, invariance, component classes, temporal logic and refinement in a coalgebraic setting. Besides the running example of the coalgebraic specification of (possibly infinite) binary trees, a specification of Peterson's mutual exclusion algorithm is elaborated in detail.},
author = {Jacobs, Bart},
booktitle = {Algebr. Coalgebraic Methods Math. Progr. Constr.},
doi = {10.1007/3-540-47797-7_7},
editor = {Backhouse, Roland and Crole, Roy and Gibbons, Jeremy},
isbn = {3-540-43613-8},
pages = {237--280},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Exercises in coalgebraic specification},
volume = {2297},
year = {2002}
}
@book{Almeida1995,
author = {Almeida, Jorge},
pages = {532},
publisher = {World Scientific},
series = {Series in Algebra},
title = {Finite Semigroups and Universal Algebra},
year = {1995}
}
@article{Martin-Lof1987,
author = {Martin-Löf, Per},
journal = {Synthese},
number = {3},
pages = {407--420},
title = {Truth of a Proposition, Evidence of a Judgement, Validity of a Proof},
volume = {73},
year = {1987}
}
@inproceedings{Milius2015,
author = {Milius, Stefan and Pattinson, Dirk and Schr{\"{o}}der, Lutz},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.253},
editor = {Sobocinski, Lawrence S. Moss and Pawel},
isbn = {978-3-939897-84-2},
issn = {1868-8969},
pages = {253--269},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Generic trace semantics and graded monads},
volume = {35},
year = {2015}
}
@article{Dobbertin1986,
author = {Dobbertin, Hans},
doi = {10.1016/0022-4049(86)90003-4},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1},
pages = {27--51},
title = {Vaught measures and their applications in lattice theory},
volume = {43},
year = {1986}
}
@article{Lack2004a,
abstract = {A PROP is a way of encoding structure borne by an object of a symmetric monoidal category. We describe a notion of distributive law for PROPs, based on Beck's distributive laws for monads. A distributive law between PROPs allows them to be composed, and an algebra for the composite PROP consists of a single object with an algebra structure for each of the original PROPs, subject to compatibility conditions encoded by the distributive law. An example is the PROP for bialgebras, which is a composite of the PROP for coalgebras and that for algebras.},
author = {Lack, Stephen},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Algebra,Bialgebra,Distributive law,Monad,PROP,Symmetric monoidal category},
number = {9},
pages = {147--163},
title = {Composing PROPs},
volume = {13},
year = {2004}
}
@article{Gumm2009,
author = {Gumm, H. Peter},
journal = {AJSE-Mathematics},
pages = {105--130},
title = {Universal coalgebras and their logics},
volume = {1},
year = {2009}
}
@article{Lee1998,
abstract = {The Hindley/Milner let-polymorphic type inference system has two different algorithms: one is the de facto standard Algorithm W that is bottom-up (or context-insensitive), and the other is a folklore algorithm that is top-down (or context-sensitive). Because the latter algorithm has not been formally presented with its soundness and completeness proofs, and its relation with the W algorithm has not been rigorously investigated, its use in place of (or in combination with) W is not well founded. In this article, we formally define the context-sensitive, top-down type inference algorithm (named M), prove its soundness and completeness, and show a distinguishing property that M always stops earlier than W if the input program is ill typed. Our proofs can be seen as theoretical justifications for various type-checking strategies being used in practice.},
author = {Lee, Oukseh and Yi, Kwangkeun},
doi = {10.1145/291891.291892},
issn = {01640925},
journal = {ACM Trans. Program. Lang. Syst.},
month = jul,
number = {4},
pages = {707--723},
title = {Proofs about a folklore let-polymorphic type inference algorithm},
volume = {20},
year = {1998}
}
@incollection{Barr1970,
author = {Barr, Michael},
booktitle = {Reports Midwest Categ. Semin. IV},
doi = {10.1007/BFb0060439},
editor = {{Mac Lane}, Saunders and Applegate, H. and Barr, Michael and Day, B. and Dubuc, Eduardo J. and Phreilambud and Pultr, A. and Street, Ross and Tierney, M. and Swierczkowski, S.},
isbn = {978-3-540-04926-5},
pages = {39--55},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Relational algebras},
year = {1970}
}
@article{Goldwasser1982,
abstract = {This paper proposes an Encryption Scheme that possess the following property : An adversary, who knows the encryption algorithm and is given the cyphertext, cannot obtain any information about the clear-text. Any implementation of a Public Key Cryptosystem, as proposed by Diffie and Hellman in 8, should possess this property. Our Encryption Scheme follows the ideas in the number theoretic implementations of a Public Key Cryptosystem due to Rivest, Shamir and Adleman 13, and Rabin 12.},
author = {Goldwasser, Shaft and Micali, Silvio},
doi = {10.1145/800070.802212},
isbn = {0897910672},
journal = {STOC '82 Proc. fourteenth Annu. ACM Symp. Theory Comput.},
pages = {365--377},
title = {Probabilistic encryption & how to play mental poker keeping secret all partial information},
year = {1982}
}
@book{Kelly1974c,
address = {Berlin, Heidelberg},
author = {Kelly, Gregory Maxwell},
doi = {10.1007/BFb0063096},
editor = {Kelly, Gregory M.},
isbn = {978-3-540-06966-9},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Category Seminar},
volume = {420},
year = {1974}
}
@article{Capretta2011,
author = {Capretta, Venanzio},
doi = {10.1016/j.tcs.2011.04.024},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = sep,
number = {38},
pages = {5006--5024},
publisher = {Elsevier B.V.},
title = {Coalgebras in functional programming and type theory},
volume = {412},
year = {2011}
}
@book{Makkai1989,
author = {Makkai, Michael and Par{\'{e}}, Robert},
isbn = {082185111X},
pages = {176},
publisher = {American Mathematical Society},
series = {Contemporary Mathematics},
title = {Accessible Categories: The Foundations of Categorical Model Theory},
year = {1989}
}
@article{Taylor1977,
author = {Taylor, Walter},
doi = {10.1007/BF00968693},
issn = {00374466},
journal = {J. Aust. Math. Soc. (Series A)},
number = {02},
pages = {207--241},
title = {Varieties of topological algebras},
volume = {23},
year = {1977}
}
@incollection{Adamek2007a,
address = {Berlin, Heidelberg},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
booktitle = {Proc. 32nd Int. Symp. Math. Found. Comput. Sci.},
doi = {10.1007/978-3-540-74456-6_23},
isbn = {9783540744559},
issn = {03029743},
keywords = {eilenberg-moore alge-,iteration theory,monad,rational theory},
pages = {240--252},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {What Are Iteration Theories?},
volume = {4708},
year = {2007}
}
@article{Abbott2005,
abstract = {We introduce the notion of a Martin-L{\"{o}}f category - a locally cartesian closed category with disjoint coproducts and initial algebras of container functors (the categorical analogue of W-types) - and then establish that nested strictly positive inductive and coinductive types, which we call strictly positive types, exist in any Martin-L{\"{o}}f category. Central to our development are the notions of containers and container functors. These provide a new conceptual analysis of data structures and polymorphic functions by exploiting dependent type theory as a convenient way to define constructions in Martin-L{\"{o}}f categories. We also show that morphisms between containers can be full and faithfully interpreted as polymorphic functions (i.e. natural transformations) and that, in the presence of W-types, all strictly positive types (including nested inductive and coinductive types) give rise to containers. {\textcopyright} 2005 Elsevier B.V. All rights reserved.},
author = {Abbott, Michael and Altenkirch, Thorsten and Ghani, Neil},
doi = {10.1016/j.tcs.2005.06.002},
isbn = {03043975},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Category theory,Coinduction,Container functors,Final coalgebras,Induction,Initial algebras,Type theory,W-Types},
pages = {3--27},
title = {Containers: Constructing strictly positive types},
volume = {342},
year = {2005}
}
@article{Adamek2011,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1017/S0960129510000496},
isbn = {0960129510},
journal = {Math. Struct. Comput. Sci.},
number = {Special Issue 02},
pages = {417--480},
title = {Elgot theories: a new perspective on the equational properties of iteration},
volume = {21},
year = {2011}
}
@article{Adamek2005a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1017/S0960129505004731},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = jun,
number = {3},
pages = {409--432},
title = {A general final coalgebra theorem},
volume = {15},
year = {2005}
}
@incollection{Pin1998,
author = {Pin, Jean-{\'{E}}ric},
booktitle = {LATIN'98 Theor. Informatics},
doi = {10.1007/BFb0054312},
editor = {Lucchesi, Cl{\'{a}}udio L. and Moura, Arnaldo V.},
pages = {76--87},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Positive varieties and infinite words},
year = {1998}
}
@article{Abramsky2011,
abstract = {We give multiple descriptions of a topological universe of finitary sets, which can be seen as a natural limit completion of the hereditarily finite sets. This universe is characterized as a metric completion of the hereditarily finite sets; as a Stone space arising as the solution of a functorial fixed-point equation involving the Vietoris construction; as the Stone dual of the free modal algebra; and as the subspace of maximal elements of a domain equation involving the Plotkin (or convex) powerdomain. These results illustrate the methods developed in the author's 'Domain theory in logical form', and related literature, and have been taken up in recent work on topological coalgebras. The set-theoretic universe of finitary sets also supports an interesting form of set theory. It contains non-well founded sets and a universal set; and is closed under positive versions of the usual axioms of set theory.},
archivePrefix = {arXiv},
arxivId = {1111.7148},
author = {Abramsky, Samson},
eprint = {1111.7148},
journal = {ArXiv e-prints},
keywords = {computer,logic,mathematics,physics,quantum,science},
mendeley-tags = {computer,logic,mathematics,physics,quantum,science},
month = nov,
title = {A cook's tour of the finitary non-well-founded sets},
type = {Journal article},
year = {2011}
}
@article{Hinze2013,
abstract = {Folds over inductive datatypes are well understood and widely used. In their plain form, they are quite restricted; but many disparate generalisations have been proposed that enjoy similar calculational benefits. There have also been attempts to unify the various generalisations: two prominent such unifications are the 'recursion schemes from comonads' of Uustalu, Vene and Pardo, and our own 'adjoint folds'. Until now, these two unified schemes have appeared incompatible. We show that this appearance is illusory: in fact, adjoint folds subsume recursion schemes from comonads. The proof of this claim involves standard constructions in category theory that are nevertheless not well known in functional programming: Eilenberg-Moore categories and bialgebras.},
author = {Hinze, Ralf and Wu, Nicolas and Gibbons, Jeremy},
doi = {10.1145/2544174.2500578},
isbn = {9781450323260},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {adjunctions,bialge-,bras,comonads,distributive laws,recursion schemes},
number = {9},
pages = {209--220},
title = {Unifying structured recursion schemes},
volume = {48},
year = {2013}
}
@article{Celani1997a,
author = {Celani, Sergio A. and Jansana, Ramon},
journal = {Notre Dame J. Form. Log.},
number = {1},
pages = {1--18},
publisher = {University of Notre Dame},
title = {A new semantics for positive modal logic},
type = {Journal article},
volume = {38},
year = {1997}
}
@article{Kurz2005a,
author = {Kurz, Alexander and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1017/S0960129504004402},
isbn = {0960129504004},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = feb,
number = {1},
pages = {149--166},
title = {Operations and equations for coalgebras},
volume = {15},
year = {2005}
}
@article{Elgot1978,
author = {Elgot, Calvin C. and Bloom, Stephen L. and Tindell, Ralph},
doi = {10.1016/0022-0000(78)90024-7},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
number = {3},
pages = {362--399},
title = {On the algebraic structure of rooted trees},
volume = {16},
year = {1978}
}
@incollection{Bonizzoni2009,
author = {Bonizzoni, Paola and {Della Vedova}, Gianluca and Dondi, Riccardo},
booktitle = {Fundam. Comput. Theory},
doi = {10.1007/978-3-642-0340

repository: anqurvanillapy/Type-Theory

repo_name: anqurvanillapy/Type-Theory