text:
007/3-540-48285-7_20},
isbn = {978-3-540-57600-6 978-3-540-48285-7},
pages = {240--247},
publisher = {Springer Berlin Heidelberg},
title = {On a Limitation of BAN Logic},
volume = {765},
year = {1994}
}
@article{Power1998,
abstract = {We give an axiomatic account of what structure on a category C and an endofunctor H on C yield similar structure on the category H ---Coalg of H-coalgebras. We give conditions under which completeness, cocompleteness, symmetric monoidal closed structure, local presentability, and subobject classifiers lift. Our proof of the latter uses a general result about the existance of a subobject classifier in a category containing a small dense subcategory. Our leading example has C = Set with H the endofunctor for which a coalgebra is a finitely branching (labelled) transition system. We explain that example in detail.},
author = {Power, A. John and Watanabe, Hiroshi},
doi = {10.1016/S1571-0661(04)00057-X},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
number = {0},
pages = {158--175},
title = {An axiomatics for categories of coalgebras},
type = {Journal article},
volume = {11},
year = {1998}
}
@incollection{Schroder2010a,
abstract = {Fixed point logics are widely used in computer science, in particular in artificial intelligence and concurrency. The most expressive logics of this type are the $\mu$-calculus and its relatives. However, popular fixed point logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the $\mu$-calculus. The family of such flat fixed point logics includes, e.g., CTL, the *-nesting-free fragment of PDL, and the logic of common knowledge. Here, we extend this notion to the generic semantic framework of coalgebraic logic, thus covering a wide range of logics beyond the standard $\mu$-calculus including, e.g., flat fragments of the graded $\mu$-calculus and the alternating-time $\mu$-calculus (such as ATL), as well as probabilistic and monotone fixed point logics. Our main results are completeness of the Kozen-Park axiomatization and a timed-out tableaux method that matches ExpTime upper bounds inherited from the coalgebraic $\mu$-calculus but avoids using automata.},
author = {Schr{\"{o}}der, Lutz and Venema, Yde},
booktitle = {CONCUR'10 Concurr. Theory},
doi = {10.1007/978-3-642-15375-4_36},
editor = {Gastin, Paul and Laroussinie, Fran{\c{c}}ois},
pages = {1--15},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Flat coalgebraic fixed point logics},
year = {2010}
}
@article{Szigeti1983,
author = {Szigeti, Jen{\"{o}}},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
keywords = {Eilenberg-Moore category,Kleisli category,cocompleteness,completeness,lifting of adjoint functors},
number = {4},
pages = {381--391},
title = {On limits and colimits in the Kleisli category},
volume = {24},
year = {1983}
}
@inproceedings{Narayanan2008,
author = {Narayanan, Arvind and Shmatikov, Vitaly},
booktitle = {2008 IEEE Symp. Secur. Priv.},
doi = {10.1109/SP.2008.33},
isbn = {978-0-7695-3168-7},
issn = {1081-6011},
month = may,
pages = {111--125},
pmid = {20113465},
publisher = {IEEE},
title = {Robust De-anonymization of Large Sparse Datasets},
year = {2008}
}
@incollection{Denux2010,
author = {Den{\oe}ux, Thierry and Masson, Marie-H{\'{e}}l{\`{e}}ne},
booktitle = {Integr. Uncertain. Manag. Appl.},
doi = {10.1007/978-3-642-11960-6_5},
editor = {Huynh, Van-Nam and Nakamori, Yoshiteru and Lawry, Jonathan and Inuiguchi, Masahiro},
isbn = {978-3-642-11959-0},
pages = {39--54},
publisher = {Springer Berlin Heidelberg},
series = {Advances in Intelligent and Soft Computing},
title = {Dempster-Shafer Reasoning in Large Partially Ordered Sets: Applications in Machine Learning},
volume = {68},
year = {2010}
}
@book{Bramer2005,
author = {Bramer, Max},
isbn = {9781852339388},
pages = {223},
publisher = {Springer},
title = {Logic Programming with Prolog},
year = {2005}
}
@article{Berger2011,
author = {Berger, Ulrich},
doi = {10.2168/LMCS-7(1:8)2011},
editor = {Kahle, Reinhard},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,coinduction,exact real number,program extraction,proof theory,realizability},
month = mar,
number = {1},
pages = {1--24},
title = {From coinductive proofs to exact real arithmetic: theory and applications},
volume = {7},
year = {2011}
}
@book{Manes1986,
address = {New York, NY},
author = {Manes, Ernest G. and Arbib, Michael A.},
doi = {10.1007/978-1-4612-4962-7},
isbn = {978-1-4612-9377-4},
publisher = {Springer New York},
title = {Algebraic Approaches to Program Semantics},
year = {1986}
}
@article{Pelletier1993,
author = {Pelletier, J. Wick and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1007/BF01196099},
issn = {00025240},
journal = {Algebr. Universalis},
pages = {275--284},
title = {On the equational theory of C*-algebras},
volume = {30},
year = {1993}
}
@article{Dostal2015,
author = {Dost{\'{a}}l, Matĕj and Velebil, Jiř{\'{i}}},
doi = {10.1007/s10485-015-9406-y},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
keywords = {2010,cauchy completion,lawvere theory,mathematics subject classifications,morita equivalence,msc 18c10,msc 18d20},
title = {Morita Equivalence for Many-Sorted Enriched Theories},
year = {2015}
}
@book{Huth2000,
author = {Huth, Michael and Ryan, Mark},
edition = {2},
isbn = {9780521543101},
pages = {440},
publisher = {Cambridge University Press},
title = {Logic in Computer Science: Modelling and Reasoning about Systems},
year = {2004}
}
@article{Ponto2012,
abstract = {By the Lefschetz fixed point theorem, if an endomorphism of a topological space is fixed-point-free, then its Lefschetz number vanishes. This necessary condition is not usually sufficient, however; for that we need a refinement of the Lefschetz number called the Reidemeister trace. Abstractly, the Lefschetz number is a trace in a symmetric monoidal category, while the Reidemeister trace is a trace in a bicategory; in this paper we relate these contexts using indexed symmetric monoidal categories. In particular, we will show that for any symmetric monoidal category with an associated indexed symmetric monoidal category, there is an associated bicategory which produces refinements of trace analogous to the Reidemeister trace. This bicategory also produces a new notion of trace for parametrized spaces with dualizable fibers, which refines the obvious "fiberwise" traces by incorporating the action of the fundamental group of the base space. We also advance the basic theory of indexed monoidal categories, including introducing a string diagram calculus which makes calculations much more tractable. This abstract framework lays the foundation for generalizations of these ideas to other contexts.},
archivePrefix = {arXiv},
arxivId = {1211.1555},
author = {Ponto, Kate and Shulman, Michael},
eprint = {1211.1555},
month = nov,
number = {23},
pages = {582--659},
title = {Duality and traces for indexed monoidal categories},
volume = {26},
year = {2012}
}
@article{Vitale1994,
author = {Vitale, Enrico M.},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {4},
pages = {351--358},
title = {On the characterization of monadic categories over set},
volume = {35},
year = {1994}
}
@article{Brengos2014a,
abstract = {We generalize the work by P. Soboci\'nski on relational presheaves and their connection with weak (bi)simulation for labelled transistion systems to a coalgebraic setting. We show that the coalgebraic notion of saturation studied in our previous work can be expressed in the language of lax Kleisli-valued presheaves in terms of existence of a certain adjoint situation between presheaf categories. This observation allows us to generalize the notion of the coalgebraic (weak) bisimulation to lax Kleisli-valued presheaves. At this level of generality interesting properties of strong and weak bisimilarity emerge: in the family of $p$-bisimilarities, which arises naturally in this setting, the former is the finest and the latter is the coarsest relation.},
archivePrefix = {arXiv},
arxivId = {1404.5267},
author = {Brengos, Tomasz},
eprint = {1404.5267},
journal = {ArXiv e-prints},
month = apr,
pages = {1--20},
title = {Lax Kleisli-valued presheaves and coalgebraic weak bisimulation},
year = {2014}
}
@incollection{Milius2013b,
author = {Milius, Stefan and Litak, Tadeusz},
booktitle = {Proc. Ninth Work. Fixed Points Comput. Sci.},
doi = {10.4204/EPTCS.126.6},
editor = {Baelde, David and Carayol, Arnaud},
issn = {2075-2180},
number = {Informatik 8},
pages = {72--86},
title = {Guard your daggers and traces: On the equational properties of guarded (co-)recursion},
volume = {126},
year = {2013}
}
@article{ELLERMAN2013,
author = {ELLERMAN, DAVID},
doi = {10.1142/S1793351X13400059},
issn = {1793-351X},
journal = {Int. J. Semant. Comput.},
keywords = {logical entropy,partition logic,shannon entropy},
month = jun,
number = {02},
pages = {121--145},
title = {AN INTRODUCTION TO LOGICAL ENTROPY AND ITS RELATION TO SHANNON ENTROPY},
volume = {07},
year = {2013}
}
@article{Jacobs2009,
author = {Jacobs, Bart and Sokolova, Ana},
doi = {10.1093/logcom/exn093},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {adjunction,coalgebra,dual,markov chains,markov processes,modal logic},
month = feb,
number = {5},
pages = {1041--1068},
title = {Exemplaric expressivity of modal logics},
volume = {20},
year = {2010}
}
@inproceedings{Aggarwal2005,
abstract = {In recent years, the wide availability of per- sonal data has made the problem of privacy preserving data mining an important one. A number of methods have recently been pro- posed for privacy preserving data mining of multidimensional data records. One of the methods for privacy preserving data mining is that of anonymization, in which a record is released only if it is indistinguishable from k other entities in the data. We note that meth- ods such as k-anonymity are highly dependent upon spatial locality in order to effectively im- plement the technique in a statistically robust way. In high dimensional space the data be- comes sparse, and the concept of spatial local- ity is no longer easy to define from an applica- tion point of view. In this paper, we view the k-anonymization problem from the perspec- tive of inference attacks over all possible com- binations of attributes. We show that when the data contains a large number of attributes which may be considered quasi-identifiers, it becomes difficult to anonymize the data with- out an unacceptably high amount of infor- mation loss. This is because an exponential number of combinations of dimensions can be used to make precise inference attacks, even when individual attributes are partially spec- ified within a range. We provide an analysis of the effect of dimensionality on k-anonymity methods. We conclude that when a data set contains a large number of attributes which are open to inference attacks, we are faced with a choice of either completely suppressing most of the data or losing the desired level of anonymity. Thus, this paper shows that the curse of high dimensionality also applies to the problem of privacy preserving data mining.},
author = {Aggarwal, Charu C.},
booktitle = {Proc. 31st VLDB Conf.},
isbn = {1-59593-154-6},
pages = {901--909},
title = {On $k$-anonymity and the curse of dimensionality},
year = {2005}
}
@article{Bonchi2008,
author = {Bonchi, Filippo and Montanari, Ugo},
doi = {10.1016/j.entcs.2009.02.012},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {coalgebra,labeled transition system,reactive system},
month = apr,
number = {2008},
pages = {201--215},
publisher = {Elsevier B.V.},
title = {A coalgebraic theory of reactive systems},
volume = {209},
year = {2008}
}
@article{Atkey2012a,
abstract = {Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For example, the N-indexed type of vectors refines lists by their lengths. Other data types may be refined in similar ways, but programmers must produce purpose-specific refinements on an ad hoc basis, developers must anticipate which refinements to include in libraries, and implementations must often store redundant information about data and their refinements. In this paper we show how to generically derive inductive characterisations of refinements of inductive types, and argue that these characterisations can alleviate some of the aforementioned difficulties associated with ad hoc refinements. Our characterisations also ensure that standard techniques for programming with and reasoning about inductive types are applicable to refinements, and that refinements can themselves be further refined.},
archivePrefix = {arXiv},
arxivId = {1205.2492},
author = {Atkey, Robert and Johann, Patricia and Ghani, Neil},
doi = {10.2168/LMCS-8(2:09)2012},
eprint = {1205.2492},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {Category theory,Dependent types,Fibrations,Inductive types,Refinement types},
number = {2:09},
pages = {1--30},
title = {Refining inductive types},
volume = {8},
year = {2012}
}
@article{Klin2007,
author = {Klin, Bartek},
doi = {10.1016/j.entcs.2007.02.034},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {coalgebra,locally presentable category,modal logic},
month = apr,
pages = {177--201},
title = {Coalgebraic modal logic beyond sets},
volume = {173},
year = {2007}
}
@inproceedings{Brickell2008,
abstract = {Re-identification is a major privacy threat to public datasets containing individual records. Many privacy protection algorithms rely on generalization and suppression of "quasi-identifier" attributes such as ZIP code and birthdate. Their objective is usually syntactic sanitization: for example, k-anonymity requires that each "quasi-identifier" tuple appear in at least k records, while l-diversity requires that the distribution of sensitive attributes for each quasi-identifier have high entropy. The utility of sanitized data is also measured syntactically, by the number of generalization steps applied or the number of records with the same quasi-identifier. In this paper, we ask whether generalization and suppression of quasi-identifiers offer any benefits over trivial sanitization which simply separates quasi-identifiers from sensitive attributes. Previous work showed that k-anonymous databases can be useful for data mining, but k-anonymization does not guarantee any privacy. By contrast, we measure the tradeoff between privacy (how much can the adversary learn from the sanitized records?) and utility, measured as accuracy of data-mining algorithms executed on the same sanitized records. For our experimental evaluation, we use the same datasets from the UCI machine learning repository as were used in previous research on generalization and suppression. Our results demonstrate that even modest privacy gains require almost complete destruction of the data-mining utility. In most cases, trivial sanitization provides equivalent utility and better privacy than k-anonymity, l-diversity, and similar methods based on generalization and suppression.},
address = {New York, New York, USA},
author = {Brickell, Justin and Shmatikov, Vitaly},
booktitle = {Proceeding 14th ACM SIGKDD Int. Conf. Knowl. Discov. data Min. - KDD 08},
doi = {10.1145/1401890.1401904},
isbn = {9781605581934},
keywords = {anonymity,data mining,privacy,utility},
pages = {70},
publisher = {ACM Press},
title = {The Cost of Privacy: Destruction of Data-Mining Utility in Anonymized Data Publishing},
year = {2008}
}
@incollection{Palmigiano2007,
abstract = {This paper is a study into some properties and applications of Moss' coalgebraic or ‘cover' modality ∇ . First we present two axiomatizations of this operator, and we prove these axiomatizations to be sound and complete with respect to basic modal and positive modal logic, respectively. More precisely, we introduce the notions of a modal ∇ -algebra and of a positive modal ∇ -algebra. We establish a categorical isomorphism between the category of modal ∇ -algebra and that of modal algebras, and similarly for positive modal ∇ -algebras and positive modal algebras. We then turn to a presentation, in terms of relation lifting, of the Vietoris hyperspace in topology. The key ingredient is an F-lifting construction, for an arbitrary set functor F, on the category Chu of two-valued Chu spaces and Chu transforms, based on relation lifting. As a case study, we show how to realize the Vietoris construction on Stone spaces as a special instance of this Chu construction for the (finite) power set functor. Finally, we establish a tight connection with the axiomatization of the modal ∇ -algebras.},
address = {Bergen, Norway},
author = {Palmigiano, Alessandra and Venema, Yde},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-540-73859-6_27},
editor = {Mossakowski, Till and Montanari, Ugo and Haveraaen, Magne},
isbn = {978-3-540-73859-6},
keywords = {coalgebra,modal algebra,relation lifting,vietoris hyper-},
pages = {394--408},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Nabla algebras and Chu spaces},
year = {2007}
}
@article{YAGER1983,
author = {Yager, Ronald R.},
doi = {10.1080/03081078308960825},
issn = {0308-1079},
journal = {Int. J. Gen. Syst.},
month = jan,
number = {4},
pages = {249--260},
title = {ENTROPY AND SPECIFICITY IN A MATHEMATICAL THEORY OF EVIDENCE},
volume = {9},
year = {1983}
}
@book{Ben-Ari2012,
address = {London},
author = {Ben-Ari, Mordechai},
doi = {10.1007/978-1-4471-4129-7},
edition = {3},
isbn = {978-1-4471-4128-0},
publisher = {Springer London},
title = {Mathematical Logic for Computer Science},
year = {2012}
}
@book{Eilenberg1976,
address = {New York},
author = {Eilenberg, Samuel},
publisher = {Academic Press},
title = {Automata, Languages, and Machines},
volume = {2},
year = {1976}
}
@book{Milner1997,
abstract = {Standard ML is a general-purpose programming language designed for large projects. This book provides a formal definition of Standard ML for the benefit of all concerned with the language, including users and implementers. Because computer programs are increasingly required to withstand rigorous analysis, it is all the more important that the language in which they are written be defined with full rigor.The Definition of Standard ML is the essential point of reference for Standard ML. Since its publication in 1990, the implementation technology of the language has advanced enormously and the number of users has grown. The revised edition includes a number of new features, omits little-used features, and corrects mistakes of definition.},
author = {Milner, Robert and Tofte, Mads and Harper, Robert and MacQueen, David},
isbn = {9780262631815},
pages = {128},
title = {The Definition of Standard ML (Revised)},
year = {1997}
}
@incollection{Klima2014,
abstract = {Eilenberg correspondence, based on the concept of syntactic monoids, relates varieties of regular languages with pseudovarieties of finite monoids. Various modifications of this correspondence related more general classes of regular languages with classes of more complex algebraic objects. Such generalized varieties also have natural counterparts formed by classes of finite automata equipped with a certain additional algebraic structure. In this survey, we overview several variants of such varieties of enriched automata.},
archivePrefix = {arXiv},
arxivId = {1405.5595},
author = {Kl{\'{i}}ma, Ondřej},
booktitle = {Proc. 14th Int. Conf. Autom. Form. Lang.},
doi = {10.4204/EPTCS.151.3},
eprint = {1405.5595},
issn = {2075-2180},
month = may,
pages = {49--54},
series = {Electronic Proceedings in Theoretical Computer Science},
title = {On Varieties of Automata Enriched with an Algebraic Structure (Extended Abstract)},
year = {2014}
}
@article{Straubing1981,
author = {Straubing, Howard},
doi = {10.1016/0304-3975(81)90036-0},
issn = {03043975},
journal = {Theor. Comput. Sci.},
number = {2},
pages = {137--150},
title = {A generalization of the Sch{\"{u}}tzenberger product of finite monoids},
volume = {13},
year = {1981}
}
@article{Ghani2013,
author = {Ghani, Neil and Johann, Patricia and Fumex, Clement},
doi = {10.2168/LMCS-9(3:6)2013},
editor = {Klin, Bartek},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = aug,
number = {3},
pages = {1--31},
title = {Indexed induction and coinduction, fibrationally},
volume = {9},
year = {2013}
}
@book{Aczel1988a,
author = {Aczel, Peter},
publisher = {Center for the Study of Language and Information, Stanford},
title = {Non-well-founded sets},
type = {Book},
year = {1988}
}
@inproceedings{Milius2016,
author = {Milius, Stefan and Pattinson, Dirk and Wi{\ss}mann, Thorsten},
booktitle = {Proc. 19th Int. Conf. Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-662-49630-5_7},
editor = {Jacobs, Bart and L{\"{o}}ding, Christof},
isbn = {978-3-662-49629-9},
pages = {107--125},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A new foundation for finitary corecursion},
volume = {9634},
year = {2016}
}
@article{Dumas2013,
abstract = {Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, exception handling is an efficient way to implement the dynamic evaluation paradigm: for instance, in linear algebra, dynamic evaluation can be used for applying programs which have been written for matrices with coefficients in a field to matrices with coefficients in a ring. Thus, a proof system for computer algebra should include a treatement of exceptions, which must rely on a careful description of a semantics of exceptions. The categorical notion of monad can be used for formalizing the raising of exceptions: this has been proposed by Moggi and implemented in Haskell. In this paper, we provide a proof system for exceptions which involves both raising and handling, by extending Moggi's approach. Moreover, the core part of this proof system is dual to a proof system for side effects in imperative languages, which relies on the categorical notion of comonad. Both proof systems are implemented in the Coq proof assistant.},
archivePrefix = {arXiv},
arxivId = {1310.2338},
author = {Dumas, Jean-guillaume and Duval, Dominique and Ekici, Burak and Reynaud, Jean-Claude},
eprint = {1310.2338},
journal = {ArXiv e-prints},
month = oct,
pages = {1--17},
title = {Certified proofs in programs involving exceptions},
year = {2013}
}
@article{Dwork2011,
abstract = {In the information realm, loss of privacy is usually associated with failure to control access to information, to control the flow of information, or to control the purposes for which information is employed. Differential privacy arose in a context in which ensuring privacy is a challenge even if all these control problems are solved: privacy-preserving statistical analysis of data. The problem of statistical disclosure control— revealing accurate statistics about a set of respondents while preserving the privacy of individuals—has a venerable history, with an extensive literature spanning statistics, theoretical computer science, security, databases, and cryptography (see, for example, the excellent survey of Adam and Wortmann,1 the discussion of related work in Blum et al.,2 and the Journal of Official Statistics dedicated to confidentiality and disclosure control).},
author = {Dwork, Cynthia},
doi = {10.1145/1866739.1866758},
isbn = {0001-0782},
issn = {00010782},
journal = {Commun. ACM},
number = {1},
pages = {86},
title = {A firm foundation for private data analysis},
volume = {54},
year = {2011}
}
@phdthesis{Sokolova2005,
author = {Sokolova, Ana},
school = {Eindhoven University of Technology},
title = {Coalgebraic Analysis of Probabilistic Systems},
year = {2005}
}
@article{Hennessy2005,
abstract = {The security ??-calculus is a typed version of the asynchronous ??-calculus in which the types, in addition to constraining the input/output behaviour of processes, have security levels associated with them. This enables us to introduce a range of typing disciplines which allow input or output behaviour, or both, to be bounded above or below by a given security level. We define typed versions of may and must equivalences for the security ??-calculus, where the tests are parameterised relative to a security level. We provide alternative characterisations of these equivalences in terms of actions in context; these describe the actions a process may perform in a given typing environment, assuming the observer is constrained by a related, but possibly different, environment. The paper also contains non-interference results with respect to may and must testing. These show that certain form of non-interference can be enforced using our typing systems. ?? 2004 Elsevier Inc. All rights reserved.},
author = {Hennessy, Matthew},
doi = {10.1016/j.jlap.2004.01.003},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
keywords = {Distributed systems,Non-interference,Pi-calculus,Security types,Testing equivalences},
number = {1},
pages = {3--34},
title = {The security pi-calculus and non-interference},
volume = {63},
year = {2005}
}
@book{Jacobs2012,
author = {Jacobs, Bart},
isbn = {9781107177895},
month = dec,
pages = {494},
publisher = {Cambridge University Press},
series = {Cambridge Tracts in Theoretical Computer Science},
title = {Introduction to Coalgebra: Towards Mathematics of States and Observation},
volume = {59},
year = {2016}
}
@incollection{Hughes1995,
author = {Hughes, John},
booktitle = {Adv. Funct. Program.},
editor = {Meijer, J. Jeuring and E.},
pages = {53--96},
publisher = {Springer Verlag},
series = {Lecture Notes in Computer Science},
title = {The design of a pretty-printing library},
year = {1995}
}
@inproceedings{Jung2013,
author = {Jung, Achim and Rivieccio, Umberto},
booktitle = {2013 28th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2013.50},
isbn = {978-1-4799-0413-6},
issn = {10436871},
keywords = {Bilattice logic,Priestley duality,algebraic logic,modal logic},
month = jun,
pages = {438--447},
publisher = {IEEE},
title = {Kripke Semantics for Modal Bilattice Logic},
year = {2013}
}
@book{Bridges1994,
archivePrefix = {arXiv},
arxivId = {arXiv:1011.1669v3},
author = {Bridges, Douglas S.},
doi = {10.1007/978-1-4612-0863-1},
eprint = {arXiv:1011.1669v3},
isbn = {978-1-4612-6925-0},
issn = {1098-6596},
pmid = {25246403},
publisher = {Springer New York},
series = {Graduate Texts in Mathematics},
title = {Computability},
volume = {146},
year = {1994}
}
@article{Hasuo2015a,
abstract = {We devise a generic framework where a weakest precondition semantics, in the form of indexed posets, is derived from a monad whose Kleisli category is enriched by posets. It is inspired by Jacobs' recent identification of a categorical structure that is common in various predicate transformers, but adds generality in the following aspects: (1) different notions of modality (such as "may" vs. "must") are captured by Eilenberg-Moore algebras; (2) nested alternating branching-like in games and in probabilistic systems with nondeterministic environments-is modularly modeled by a monad on the Eilenberg-Moore category of another.},
author = {Hasuo, Ichiro},
doi = {10.1016/j.tcs.2015.03.047},
isbn = {9783662441237},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Algebra,Categorical model,Coalgebra,Effect,Game,Monad,Nondeterminism,Precondition calculus,Program logic,Program verification},
number = {April 2014},
pages = {2--29},
publisher = {Elsevier B.V.},
title = {Generic weakest precondition semantics from monads enriched with order},
volume = {604},
year = {2015}
}
@article{Calude2017,
abstract = {**medianamente t{\'{e}}cnico** La efectividad de las herramientas de analisis de datos es usada para apoyar la filosofia que va en contra del m{\'{e}}todo cient{\'{i}}fico. Siendo as{\'{i}}, los auotres, prueban que las bases de datos muy grandes contienen correlaciones arbitrarias. Los autores argumentan que demasiada informaci{\'{o}}n tiende a comportarse como muy poca informaci{\'{o}}n, por lo cual el paper afirma que el m{\'{e}}todo cientifico puede ser enriquecido por la computadora pero no reemplazado por ella.},
archivePrefix = {arXiv},
arxivId = {arXiv:1011.1669v3},
author = {Calude, Cristian S. and Longo, Giuseppe},
doi = {10.1007/s10699-016-9489-4},
eprint = {arXiv:1011.1669v3},
isbn = {9788578110796},
issn = {1233-1821},
journal = {Found. Sci.},
keywords = {Algorithmic information theory,Big data,Correlation,Ergodic theory,Ramsey theory},
month = sep,
number = {3},
pages = {595--612},
pmid = {25246403},
publisher = {Springer Netherlands},
title = {The Deluge of Spurious Correlations in Big Data},
volume = {22},
year = {2017}
}
@article{Antoniou1998,
abstract = {Default logic is one of the most prominent approaches to nonmonotonic reasoning, and allows one to make plausible conjectures when faced with incomplete information about the problem at hand. Default rules prevail in many application domains such as},
author = {ANTONIOU, GRIGORIS},
doi = {10.1017/S0269888998002136},
issn = {02698889},
journal = {Knowl. Eng. Rev.},
month = oct,
number = {3},
pages = {S0269888998002136},
title = {A tutorial on default reasoning},
volume = {13},
year = {1998}
}
@article{Tsuiki2002,
abstract = {We propose an embedding G of the unit open interval to the set {0, 1}⊥,$\omega$, 1 of infinite sequences of {0, 1} with at most one undefined element. This embedding is based on Gray code and it is a topological embedding with a natural topology on {0, 1}⊥,$\omega$, 1. We also define a machine called an indeterministic multihead Type 2 machine which input/output sequences in {0, 1}⊥$\omega$, 1, and show that the computability notion induced on real functions through the embedding G is equivalent to the one induced by the signed digit representation and Type 2 machines. We also show that basic algorithms can be expressed naturally with respect to this embedding. {\textcopyright} 2002 Elsevier Science B.V. All rights reserved.},
author = {Tsuiki, Hideki},
doi = {10.1016/S0304-3975(01)00104-9},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Gray code,IM2-machines,Indeterminism,Multihead,Real number computation},
month = jul,
number = {2},
pages = {467--485},
title = {Real number computation through Gray code embedding},
volume = {284},
year = {2002}
}
@book{Munkres1999,
author = {Munkres, James},
edition = {2},
isbn = {9780131816299},
pages = {537},
publisher = {Pearson},
title = {Topology},
year = {1999}
}
@inproceedings{Dwork2009,
abstract = {We consider private data analysis in the setting in which a trusted and trustworthy curator, having obtained a large data set containing private information, releases to the public a "sanitization" of the data set that simultaneously protects the privacy of the individual contributors of data and offers utility to the data analyst. The sanitization may be in the form of an arbitrary data structure, accompanied by a computational procedure for determining approximate answers to queries on the original data set, or it may be a "synthetic data set" consisting of data items drawn from the same universe as items in the original data set; queries are carried out as if the synthetic data set were the actual input. In either case the process is non-interactive; once the sanitization has been released the original data and the curator play no further role. For the task of sanitizing with a synthetic dataset output, we map the boundary between computational feasibility and infeasibility with respect to a variety of utility measures. For the (potentially easier) task of sanitizing with unrestricted output format, we show a tight qualitative and quantitative connection between hardness of sanitizing and the existence of traitor tracing schemes.},
address = {New York, New York, USA},
author = {Dwork, Cynthia and Naor, Moni and Reingold, Omer and Rothblum, Guy N and Vadhan, Salil},
booktitle = {Proc. 41st Annu. ACM Symp. Symp. theory Comput. - STOC '09},
doi = {10.1145/1536414.1536467},
isbn = {9781605585062},
issn = {07378017},
keywords = {cryptography,differential privacy,exponential mechanism,privacy,traitor tracing},
pages = {381},
publisher = {ACM Press},
title = {On the complexity of differentially private data release},
year = {2009}
}
@inproceedings{Bianco2009,
author = {Bianco, Alessandro and Mogavero, Fabio and Murano, Aniello},
booktitle = {2009 24th Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2009.28},
isbn = {978-0-7695-3746-7},
keywords = {-temporal logics,automata-theoretic approach,conservativeness,graded modalities,minimality,satisfiability},
month = aug,
pages = {342--351},
publisher = {IEEE},
title = {Graded computation tree Logic},
year = {2009}
}
@phdthesis{Vasilakopoulou2014,
archivePrefix = {arXiv},
arxivId = {1411.3038},
author = {Vasilakopoulou, Christina},
eprint = {1411.3038},
school = {University of Cambridge},
title = {Generalization of Algebraic Operations},
year = {2014}
}
@incollection{Linton1969,
author = {Linton, F. E. J.},
booktitle = {Semin. Triples Categ. Homol. Theory},
doi = {10.1007/BFb0083082},
editor = {Eckmann, B.},
pages = {75--90},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Coequalizers in categories of algebras},
year = {1969}
}
@article{Plotkin2013,
abstract = {TheBayesianapproachtomachinelearningamountstoinferringpos- terior distributions of random variables from a probabilistic model of how the variables are related (that is, a prior distribution) and a set of observations of variables. There is a trend in machine learning towards expressing Bayesian models as probabilistic programs. As a foundation for this kind of programming, we pro- pose a core functional calculus with primitives for sampling prior distributions and observing variables. We define combinators for measure transformers, based on theorems in measure theory, and use these to give a rigorous semantics to our core calculus. The original features of our semantics include its support for discrete, continuous, and hybrid measures, and, in particular, for observations of zero-probability events. We compile our core language to a small imperative lan- guage that has a straightforward semantics via factor graphs, data structures that enable many efficient inference algorithms. We use an existing inference engine for efficient approximate inference of posterior marginal distributions, treating thousands of observations per second for large instances of realistic models.},
archivePrefix = {arXiv},
arxivId = {1310.7417},
author = {Plotkin, Gordon D. and Pretnar, Matija},
doi = {10.2168/LMCS-9(4:23)2013},
editor = {Tarlecki, Andrzej},
eprint = {1310.7417},
isbn = {978-3-642-19717-8},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {()},
month = dec,
number = {4},
pages = {77--96},
title = {Handling algebraic effects},
volume = {9},
year = {2013}
}
@article{Milius2010,
author = {Milius, Stefan},
doi = {10.1109/LICS.2010.11},
isbn = {978-1-4244-7588-9},
journal = {25th Annu. IEEE Symp. Log. Comput. Sci.},
keywords = {-kleene algebra,coalgebra,regular ex-,streams},
month = jul,
pages = {421--430},
publisher = {Ieee},
title = {A Sound and Complete Calculus for Finite Stream Circuits},
year = {2010}
}
@article{Pattinson2010,
author = {Pattinson, Dirk and Schr{\"{o}}der, Lutz},
doi = {10.1016/j.ic.2009.11.008},
issn = {08905401},
journal = {Inf. Comput.},
month = dec,
number = {12},
pages = {1447--1468},
publisher = {Elsevier Inc.},
title = {Cut elimination in coalgebraic logics},
volume = {208},
year = {2010}
}
@incollection{Kupke2009,
author = {Kupke, Clemens and Leal, Raul Andres},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-03741-2_8},
editor = {Kurz, Alexander and Lenisa, Marina and Tarlecki, Andrzej},
isbn = {978-3-642-03740-5},
pages = {97--112},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Characterising Behavioural Equivalence: Three Sides of One Coin},
year = {2009}
}
@article{Boudes2012,
abstract = {We study the notion of stratification, as used in subsystems of linear logic with low complexity bounds on the cut-elimination procedure (the so-called light logics), from an abstract point of view, introducing a logical system in which stratification is handled by a separate modality. This modality, which is a generalization of the paragraph modality of Girard's light linear logic, arises from a general categorical construction applicable to all models of linear logic. We thus learn that stratification may be formulated independently of exponential modalities; when it is forced to be connected to exponential modalities, it yields interesting complexity properties. In particular, from our analysis stem three alternative reformulations of Baillot and Mazza's linear logic by levels: one geometric, one interactive, and one semantic.},
archivePrefix = {arXiv},
arxivId = {1206.6504},
author = {Boudes, Pierre and Mazza, Damiano and de Falco, Lorenzo Tortora},
eprint = {1206.6504},
journal = {ArXiv e-prints},
keywords = {categorical semantics,denotational semantics,implicit computational complexity,light linear logics},
month = jun,
title = {An abstract approach to stratification in linear logic},
year = {2012}
}
@article{Adamek2013a,
abstract = {Every ideal monad M on the category of sets is known to have a reflection M̂ in the category of all iterative monads of Elgot. Here we describe the iterative reflection M̂ as the monad of free iterative Eilenberg-Moore algebras for M. This yields numerous concrete examples: if M is the free-semigroup monad, then M̂ is obtained by adding a single absorbing element; if M is the monad of finite trees then M̂ is the monad of rational trees, etc. {\textcopyright} 2013 Elsevier Inc.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1016/j.ic.2013.02.003},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Equational laws,Iterative theory,Monad,Recursive equations},
pages = {83--118},
title = {How iterative reflections of monads are constructed},
volume = {225},
year = {2013}
}
@article{BREUGEL1996,
author = {van Breugel, Franck},
doi = {10.1111/j.1749-6632.1996.tb49160.x},
issn = {0077-8923},
journal = {Ann. N. Y. Acad. Sci.},
keywords = {and phrases,banach,compactly branching,complete metric space,finitely branching,labelled transition system,metric labelled,s theorem,transition system,unique},
month = dec,
pages = {69--87},
title = {A theory of metric labelled transition systems},
volume = {806},
year = {1996}
}
@article{Huet1997,
abstract = {Almost every programmer has faced the problem of representing a tree together with a subtree that is the focus of attention, where that focus may move left, right, up or down the tree. The Zipper is Huet's nifty name for a nifty data structure which fulfills this need. I wish I had known of it when I faced this task, because the solution I came up with was not quite so efficient or elegant as the Zipper.},
author = {HUET, G{\'{E}}RARD},
doi = {10.1017/S0956796897002864},
issn = {09567968},
journal = {J. Funct. Program.},
month = sep,
number = {5},
pages = {S0956796897002864},
title = {The Zipper},
volume = {7},
year = {1997}
}
@article{SCHULTZ2017,
abstract = {In this paper, we develop an algebraic approach to data integration by combining techniques from functional programming, category theory, and database theory. In our formalism, database schemas and instances are algebraic (multi-sorted equational) theories of a certain form. Schemas denote categories, and instances denote their initial (term) algebras. The instances on a schema S form a category, S – Inst , and a morphism of schemas F : S → T induces three adjoint data migration functors: $\Sigma$ F : S – Inst → T – Inst , defined by substitution along F , which has a right adjoint $\Delta$ F : T – Inst → S – Inst , which in turn has a right adjoint $\Pi$ F : S – Inst → T – Inst . We present a query language based on for/where/return syntax where each query denotes a sequence of data migration functors; a pushout-based design pattern for performing data integration using our formalism; and describe the implementation of our formalism in a tool we call AQL (Algebraic Query Language).},
author = {SCHULTZ, PATRICK and WISNESKY, RYAN},
doi = {10.1017/S0956796817000168},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = nov,
pages = {e24},
title = {Algebraic data integration},
volume = {27},
year = {2017}
}
@incollection{Bonsangue1995,
author = {Bonsangue, Marcello M. and Kwiatkowska, Marta Z.},
booktitle = {Modal Log. Process Algebr. A Bisimulation Perspect.},
editor = {Ponse, Alban and de Rijke, Maarten and Venema, Yde},
pages = {65--83},
publisher = {Stanford CLSI publications},
series = {CLSI Lecture Notes},
title = {Re-interpreting modal $\mu$-calculus},
year = {1995}
}
@article{Fritz2015,
abstract = {Resources and their use and consumption form a central part of our life. Many branches of science and engineering are concerned with the question of which given resource objects can be converted into which target resource objects. For example, information theory studies the conversion of a noisy communication channel instance into an exchange of information. Inspired by work in quantum information theory, we develop a general mathematical toolbox for this type of question. The convertibility of resources into other ones and the possibility of combining resources is accurately captured by the mathematics of ordered commutative monoids. As an intuitive example, we consider chemistry, where chemical reaction equations such as \mathrm{2H_2 + O_2} \lra \mathrm{2H_2O,} are concerned both with a convertibility relation ‘→' and a combination operation ‘+.' We study ordered commutative monoids from an algebraic and functional-analytic perspective and derive a wealth of results which should have applications to concrete resource theories, such as a formula for rates of conversion. As a running example showing that ordered commutative monoids are also of purely mathematical interest without the resource-theoretic interpretation, we exemplify our results with the ordered commutative monoid of graphs.},
archivePrefix = {arXiv},
arxivId = {1504.03661},
author = {Fritz, Tobias},
doi = {10.1017/S0960129515000444},
eprint = {1504.03661},
isbn = {0960129515000},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = sep,
number = {06},
pages = {850--938},
title = {Resource convertibility and ordered commutative monoids},
volume = {27},
year = {2017}
}
@article{Komendantskaya2013,
abstract = {Coinductive definitions, such as that of an infinite stream, may often be described by elegant logic programs, but ones for which SLD-refutation is of no value as SLD-derivations fall into infinite loops. Such definitions give rise to questions of lazy corecursive derivations and parallelism, as execution of such logic programs can have both recursive and corecursive features at once. Observational and coalgebraic semantics have been used to study them abstractly. The programming developments have often occurred separately and have usually been implementation-led. Here, we give a coherent semantics-led account of the issues, starting with abstract category theoretic semantics, developing coalgebra to characterise naturally arising trees, and proceeding towards implementation of a new dialect, CoALP, of logic programming, characterised by guarded lazy corecursion and parallelism.},
archivePrefix = {arXiv},
arxivId = {1312.6568},
author = {Komendantskaya, Ekaterina and Power, A. John and Schmidt, Martin},
eprint = {1312.6568},
journal = {ArXiv e-prints},
keywords = {coalgebra,coinduction,corecursion,logic programming,observational semantics,parallelism},
month = dec,
pages = {1--40},
title = {Coalgebraic Logic Programming: from Semantics to Implementation},
year = {2013}
}
@inproceedings{Gaboardi2016,
abstract = {Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful features include partiality, non-determinism, input-output, state, and exceptions. Coeffectful features include resource demands, variable access, notions of linearity, and data input requirements. The effectful or coeffectful behaviour of a program can be captured and described via type-based analyses, with fine grained information provided by monoidal effect annotations and semiring coeffects. Various recent work has proposed models for such typed calculi in terms of graded (strong) monads for effects and graded (monoidal) comonads for coeffects. Effects and coeffects have been studied separately so far, but in practice many computations are both effectful and coeffectful, e.g., possibly throwing exceptions but with resource requirements. To remedy this, we introduce a new general calculus with a combined effect-coeffect system. This can describe both the changes and requirements that a program has on its context, as well as interactions between these effectful and coeffectful features of computation. The effect-coeffect system has a denotational model in terms of effect-graded monads and coeffect-graded comonads where interaction is expressed via the novel concept of graded distributive laws. This graded semantics unifies the syntactic type theory with the denotational model. We show that our calculus can be instantiated to describe in a natural way various different kinds of interaction between a program and its evaluation context.},
address = {New York, New York, USA},
author = {Gaboardi, Marco and Katsumata, Shin-ya and Orchard, Dominic and Breuvart, Flavien and Uustalu, Tarmo},
booktitle = {Proc. 21st ACM SIGPLAN Int. Conf. Funct. Program. - ICFP 2016},
doi = {10.1145/2951913.2951939},
isbn = {9781450342193},
keywords = {categorical semantics,coeffects,comonads,distributive,effects,grading,laws,monads,types},
pages = {476--489},
publisher = {ACM Press},
title = {Combining effects and coeffects via grading},
year = {2016}
}
@article{Capriotti2014,
abstract = {Applicative functors are a generalisation of monads. Both allow the expression of effectful computations into an otherwise pure language, like Haskell. Applicative functors are to be preferred to monads when the structure of a computation is fixed a priori. That makes it possible to perform certain kinds of static analysis on applicative values. We define a notion of free applicative functor, prove that it satisfies the appropriate laws, and that the construction is left adjoint to a suitable forgetful functor. We show how free applicative functors can be used to implement embedded DSLs which can be statically analysed.},
archivePrefix = {arXiv},
arxivId = {1403.0749},
author = {Capriotti, Paolo and Kaposi, Ambrus},
doi = {10.4204/EPTCS.153.2},
eprint = {1403.0749},
issn = {2075-2180},
journal = {Electron. Proc. Theor. Comput. Sci.},
month = jun,
number = {section 10},
pages = {2--30},
title = {Free Applicative Functors},
volume = {153},
year = {2014}
}
@incollection{Osdol1971,
author = {Osdol, Donovan H. Van},
booktitle = {Exact Categ. Categ. Sheaves},
doi = {10.1007/BFb0058582},
isbn = {978-3-540-05678-2},
pages = {223--239},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Sheaves in regular categories},
year = {1971}
}
@book{Mostowskit1977,
author = {Keisler, H. J. and Mostowskit, A. and Robinsont, A. and Suppes, P. and Troelstra, A. S.},
editor = {Barwise, Jon},
isbn = {978-0-444-86388-1},
pages = {1165},
publisher = {North Holland},
series = {Studies in Logic and the Foundations of Mathematics},
title = {Handbook of Mathematical Logic},
volume = {90},
year = {1977}
}
@incollection{Sano2011a,
author = {Sano, Katsuhiko},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-22944-2_23},
editor = {Corradini, Andrea and Klin, Bartek and C{\^{i}}rstea, Corina},
pages = {329--343},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Generalized product of coalgebraic hybrid logics},
year = {2011}
}
@book{Rutten2005,
author = {Rutten, Jan J.M.M.},
booktitle = {Math. Struct. Comput. Sci.},
doi = {10.1017/S0960129504004517},
isbn = {0960129504004},
issn = {0960-1295},
month = feb,
number = {1},
pages = {93--147},
title = {A coinductive calculus of streams},
volume = {15},
year = {2005}
}
@incollection{Robinson1987,
author = {Robinson, Edmund P.},
booktitle = {Categ. Theory Comput. Sci.},
doi = {10.1007/3-540-18508-9_29},
editor = {Pitt, David H. and Poign{\'{e}}, Axel and Rydeheard, David E.},
isbn = {978-3-540-18508-6},
keywords = {Computer Science},
pages = {238--253},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Logical aspects of denotational semantics},
volume = {283},
year = {1987}
}
@article{Adamek2005,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
journal = {Theory Appl. Categ.},
number = {8},
pages = {157--199},
title = {Introduction to coalgebra},
volume = {14},
year = {2005}
}
@article{Karazeris2007,
author = {Karazeris, Panagis and Velebil, I},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {and phrases,definable operation,locally finitely presentable category,monad morphism},
number = {14},
pages = {372--399},
title = {Dense morphisms of monads},
volume = {18},
year = {2007}
}
@article{Lenisa2000,
author = {Lenisa, Marina and Power, A. John and Watanabe, Hiroshi},
doi = {10.1016/S1571-0661(05)80350-0},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jan,
pages = {230--260},
title = {Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads},
volume = {33},
year = {2000}
}
@incollection{Carton2008,
author = {Carton, Olivier and Perrin, Dominique and Pin, Jean-{\'{E}}ric},
booktitle = {Log. Autom. Hist. Perspect.},
editor = {Flum, Jörg and Grädel, Erich and Wilke, Thomas},
isbn = {978 90 5356 576 6},
pages = {133--167},
publisher = {Amsterdam University Press},
series = {Texts in Logic and Games},
title = {Automata and semigroups recognizing infinite words},
year = {2008}
}
@incollection{DArgenio2012,
abstract = {We present a format for the specification of probabilistic transition systems that guarantees that bisimulation equivalence is a congruence for any operator defined in this format. In this sense, the format is somehow comparable to the ntyft/ntyxt format in a non-probabilistic setting. We also study the modular construction of probabilistic transition systems specifications and prove that some standard conservative extension theorems also hold in our setting. Finally, we show that the trace congruence for image-finite processes induced by our format is precisely bisimulation on probabilistic systems.},
author = {D'Argenio, Pedro and Lee, Matias},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {452--466},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Probabilistic Transition System Specification: Congruence and Full Abstraction of Bisimulation},
volume = {7213},
year = {2012}
}
@incollection{Esik2002,
author = {{\'{E}}sik, Zolt{\'{a}}n and Lei$\beta$, Hans},
booktitle = {Comput. Sci. Logic. CSL 2002},
doi = {10.1007/3-540-45793-3_10},
editor = {Bradfield, Julian},
keywords = {al-,context-free languages,conway algebra,equational theory,gebraically complete semirings,greibach normal form,kleene algebra,point induction,pre-fixed-},
pages = {135--150},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Greibach Normal Form in Algebraically Complete Semirings},
volume = {2471},
year = {2002}
}
@article{Provan,
author = {Provan, Gregory M},
doi = {10.1016/0888-613X(90)90016-U},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {assumption-based truth maintenance system,dempster-shafer theory,ing,logic,reasoning system,theorem prov-,uncertainty},
month = sep,
number = {5-6},
pages = {451--495},
title = {A logic-based analysis of Dempster-Shafer theory},
volume = {4},
year = {1990}
}
@article{Fiore2011,
abstract = {We extend the basic concepts of Street's formal theory of monads from the setting of 2-categories to that of double categories. In particular, we introduce the double category Mnd(C) of monads in a double category C and define what it means for a double category to admit the construction of free monads. Our main theorem shows that, under some mild conditions, a double category that is a framed bicategory admits the construction of free monads if its horizontal 2-category does. We apply this result to obtain double adjunctions which extend the adjunction between graphs and categories and the adjunction between polynomial endofunctors and polynomial monads. ?? 2010 Elsevier B.V..},
archivePrefix = {arXiv},
arxivId = {1006.0797},
author = {Fiore, Thomas M. and Gambino, Nicola and Kock, Joachim},
doi = {10.1016/j.jpaa.2010.08.003},
eprint = {1006.0797},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jun,
number = {6},
pages = {1174--1197},
publisher = {Elsevier B.V.},
title = {Monads in double categories},
volume = {215},
year = {2011}
}
@article{Ghani2002,
abstract = {This paper introduces coalgebraic monads as a unified model of term algebras covering fundamental examples such as initial algebras, final coalgebras, rational terms and term graphs. We develop a general method for obtaining finitary coalgebraic monads which allows us to generalise the notion of rational term and term graph to categories other than Set. As an application we sketch part of the correctness of the the term graph implementation of functional programming languages. {\textcopyright} 2002 Published by Elsevier Science B.V.},
author = {Ghani, Neil and L{\"{u}}th, Christoph and {De Marchi}, Federico},
doi = {10.1016/S1571-0661(04)80360-8},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {71--91},
title = {Coalgebraic monads},
volume = {65},
year = {2002}
}
@incollection{Zhang2013,
abstract = {Publication of the private set-valued data will provide enormous opportunities for counting queries and various data mining tasks. Compared to those previous methods based on partition-based privacy models (e.g., k-anonymity), differential privacy provides strong privacy guarantees against adversaries with arbitrary background knowledge. However, the existing solutions based on differential privacy for data publication are currently limited to static datasets, and do not adequately address today's demand for up-to-date information. In this paper, we address the problem of differentially private set-valued data release on an incremental scenario in which the data need to be transformed are not static. Motivated by this, we propose an efficient algorithm, called IncTDPart, to incrementally generate a series of differentially private releases. The proposed algorithm is based on top-down partitioning model with the help of item-free taxonomy tree and update-bounded mechanism. Extensive experiments on real datasets confirm that our approach maintains high utility and scalability for counting query.},
author = {Zhang, Xiaojian and Meng, Xiaofeng and Chen, Rui},
booktitle = {Database Syst. Adv. Appl. DASFAA 2013},
doi = {10.1007/978-3-642-37487-6_30},
editor = {Meng, Weiyi and Feng, Ling and Bressan, St{\'{e}}phane and Winiwarter, Werner and Song, Wei},
isbn = {9783642374869},
issn = {03029743},
keywords = {Differential privacy,Incremental updates,Set-valued data},
pages = {392--406},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Differentially Private Set-Valued Data Release against Incremental Updates},
volume = {7825},
year = {2013}
}
@article{Mellies2015,
abstract = {Any refinement system (= functor) has a fully faithful representation in the refinement system of presheaves, by interpreting types as relative slice categories, and refinement types as presheaves over those categories. Motivated by an analogy between side effects in programming and *context effects* in linear logic, we study logical aspects of this "positive" (covariant) representation, as well as of an associated "negative" (contravariant) representation. We establish several preservation properties for these representations, including a generalization of Day's embedding theorem for monoidal closed categories. Then we establish that the positive and negative representations satisfy an Isbell-style duality. As corollaries, we derive two different formulas for the positive representation of a pushforward (inspired by the classical negative translations of proof theory), which express it either as the dual of a pullback of a dual, or as the double dual of a pushforward. Besides explaining how these constructions on refinement systems generalize familiar category-theoretic ones (by viewing categories as special refinement systems), our main running examples involve representations of Hoare Logic and linear sequent calculus.},
archivePrefix = {arXiv},
arxivId = {1501.05115},
author = {Melli{\`{e}}s, Paul-Andr{\'{e}} and Zeilberger, Noam},
eprint = {1501.05115},
journal = {ArXiv e-prints},
month = jan,
pages = {1--35},
title = {An Isbell Duality Theorem for Type Refinement Systems},
year = {2015}
}
@inproceedings{Cuff2016,
abstract = {Differential privacy is a precise mathematical constraint meant to ensure privacy of individual pieces of information in a database even while queries are being answered about the aggregate. Intuitively, one must come to terms with what differential privacy does and does not guarantee. For example, the definition prevents a strong adversary who knows all but one entry in the database from further inferring about the last one. This strong adversary assumption can be overlooked, resulting in misinterpretation of the privacy guarantee of differential privacy. Herein we give an equivalent definition of privacy using mutual information that makes plain some of the subtleties of differential privacy. The mutual-information differential privacy is in fact sandwiched between $\epsilon$-differential privacy and $(\epsilon,\delta)$-differential privacy in terms of its strength. In contrast to previous works using unconditional mutual information, differential privacy is fundamentally related to conditional mutual information, accompanied by a maximization over the database distribution. The conceptual advantage of using mutual information, aside from yielding a simpler and more intuitive definition of differential privacy, is that its properties are well understood. Several properties of differential privacy are easily verified for the mutual information alternative, such as composition theorems.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {1608.03677},
author = {Cuff, Paul and Yu, Lanqing},
booktitle = {Proc. 2016 ACM SIGSAC Conf. Comput. Commun. Secur. - CCS'16},
doi = {10.1145/2976749.2978308},
eprint = {1608.03677},
isbn = {9781450341394},
issn = {15437221},
keywords = {differential privacy,information theory},
pages = {43--54},
publisher = {ACM Press},
title = {Differential Privacy as a Mutual Information Constraint},
year = {2016}
}
@article{Teheux2007,
author = {Teheux, Bruno},
doi = {10.1007/s11225-007-9074-5},
issn = {0039-3215},
journal = {Stud. Log.},
keywords = {many-valued modal logics,mv-algebras,operator,rela-,topological duality},
month = oct,
number = {1},
pages = {13--36},
title = {A Duality for the Algebras of a {\L}ukasiewicz n + 1-valued Modal System},
volume = {87},
year = {2007}
}
@article{Isaksen2002,
abstract = {We present some constructions of limits and colimits in pro-categories. These are critical tools in several applications. In particular, certain technical arguments concerning strict pro-maps are essential for a theorem about \'etale homotopy types. Also, we show that cofiltered limits in pro-categories commute with finite colimits.},
archivePrefix = {arXiv},
arxivId = {math/0106094},
author = {Isaksen, Daniel C.},
doi = {10.4064/fm175-2-7},
eprint = {0106094},
issn = {00162736},
journal = {Fundam. Math.},
keywords = {Colimit,Essentially of type C,Limit,Pro-abelian category,Pro-category},
number = {2},
pages = {175--194},
primaryClass = {math},
title = {Calculating limits and colimits in pro-categories},
volume = {175},
year = {2002}
}
@article{Adamek2010a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Gumm, H. Peter and Trnkov{\'{a}}, V{\v{e}}ra},
doi = {10.1093/logcom/exn090},
issn = {0955-792X},
journal = {J. Log. Comput.},
month = feb,
number = {5},
pages = {991--1015},
publisher = {Oxford Univ Press},
title = {Presentation of Set Functors: A Coalgebraic Perspective},
type = {Journal article},
volume = {20},
year = {2009}
}
@incollection{Hulsbusch2012,
abstract = {We consider conditional reactive systems, a general abstract framework for rewriting, in which reactive systems {\`{a}} la Leifer and Milner are enriched with (nested) application conditions. We study the problem of deriving labelled transitions and bisimulation congruences from a reduction semantics. That is, we synthesize interactions with the environment in order to obtain a compositional semantics. Compared to earlier work we not only address the problem of deriving information about the (minimal) context needed to obtain a full left-hand side and thus be able to perform a reduction, but also generate conditions on the remaining context.},
author = {H{\"{u}}lsbusch, Mathias and K{\"{o}}nig, Barbara},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {361--375},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Deriving Bisimulation Congruences for Conditional Reactive Systems},
volume = {7213},
year = {2012}
}
@article{Desharnais2002,
author = {Desharnais, Jos{\'{e}}e and Edalat, Abbas and Panangaden, Prakash},
doi = {10.1006/inco.2001.2962},
issn = {08905401},
journal = {Inf. Comput.},
month = dec,
number = {2},
pages = {163--193},
title = {Bisimulation for Labelled Markov Processes},
volume = {179},
year = {2002}
}
@article{Reiterman1982,
author = {Reiterman, Jan},
doi = {10.1007/BF02483902},
issn = {0002-5240},
journal = {Algebr. Universalis},
month = dec,
number = {1},
pages = {1--10},
title = {The Birkhoff theorem for finite algebras},
volume = {14},
year = {1982}
}
@article{Eilenberg1976a,
author = {Eilenberg, Samuel and Sch{\"{u}}tzenb{\'{e}}rger, Marcel P.},
journal = {Adv. Math. (N. Y).},
number = {3},
pages = {413--418},
title = {On pseudovarieties},
volume = {19},
year = {1976}
}
@incollection{Rutten1995a,
author = {Rutten, Jan J.M.M.},
booktitle = {Modal Log. Process Algebr.},
editor = {Ponse, Alban and de Rijke, Maarten and Venema, Yde},
pages = {231--256},
publisher = {Center for the Study of Language and Information, Stanford},
title = {A calculus of transition systems (towards universal coalgebra)},
type = {Book chapter/section},
year = {1995}
}
@inproceedings{Kataoka2015b,
address = {Dagstuhl, Germany},
author = {Kataoka, Toshiki and Pavlovi{\'{c}}, Dusko},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.130},
editor = {Moss, Lawrence S and Sobocinski, Pawel},
isbn = {978-3-939897-84-2},
issn = {1868-8969},
keywords = {130,2015,4230,a,a sup- and inf-complete,algebra,and phrases concept analysis,calco,category,category a with a,completion,digital object identifier 10,it is an open,lipics,problem whether there exists,semantic indexing,sup- and inf-dense embedding},
pages = {130--155},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Towards Concept Analysis in Categories: Limit Inferior as Algebra, Limit Superior as Coalgebra},
volume = {35},
year = {2015}
}
@article{Mio2013,
author = {Mio, Matteo and Simpson, Alex},
doi = {10.4204/EPTCS.126.7},
issn = {2075-2180},
journal = {Electron. Proc. Theor. Comput. Sci.},
month = aug,
number = {Fics},
pages = {87--104},
title = {{\L}ukasiewicz mu-Calculus},
volume = {126},
year = {2013}
}
@article{Machanavajjhala2015,
author = {Machanavajjhala, Ashwin and Kifer, Daniel},
doi = {10.1145/2660766},
issn = {00010782},
journal = {Commun. ACM},
month = feb,
number = {3},
pages = {58--67},
title = {Designing statistical privacy for your data},
volume = {58},
year = {2015}
}
@article{Boja2015,
abstract = {The principle behind algebraic language theory for various kinds of structures, such as words or trees, is to use a compositional function from the structures into a finite set. To talk about compositionality, one needs some way of composing structures into bigger structures. It so happens that category theory has an abstract concept for this, namely a monad. The goal of this paper is to propose monads as a unifying framework for discussing existing algebras and designing new algebras.},
archivePrefix = {arXiv},
arxivId = {1502.04898},
author = {Boja{\'{n}}czyk, Miko{\l}aj},
doi = {10.1007/978-3-319-21500-6_1},
editor = {Potapov, Igor},
eprint = {1502.04898},
isbn = {978-3-319-21499-3},
journal = {19th Int. Conf. Dev. Lang. Theory},
pages = {1--13},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
title = {Recognisable languages over monads},
year = {2015}
}
@article{Tarizadeh2013,
author = {Tarizadeh, Abolfazl},
doi = {10.4995/agt.2013.1575},
issn = {1989-4147},
journal = {Appl. Gen. Topol.},
keywords = {coarser topology,connected components,flective subcategory,profinite spaces,re-},
number = {2},
pages = {147--157},
title = {On the category of profinite spaces as a reflective subcategory},
volume = {14},
year = {2013}
}
@article{Bacchus1996,
abstract = {An intelligent agent will often be uncertain about various properties of its environment, and when acting in that environment it will frequently need to quantify its uncertainty. For example, if the agent wishes to employ the expected-utility paradigm of decision theory to guide its actions, it will need to assign degrees of belief (subjective probabilities) to various assertions. Of course, these degrees of belief should not be arbitrary, but rather should be based on the information available to the agent. This paper describes one approach for inducing degrees of belief from very rich knowledge bases, that can include information about particular individuals, statistical correlations, physical laws, and default rules. We call our approach the random-worlds method. The method is based on the principle of indifference: it treats all of the worlds the agent considers possible as being equally likely. It is able to integrate qualitative default reasoning with quantitative probabilistic reasoning by providing a language in which both types of information can be easily expressed. Our results show that a number of desiderata that arise in direct inference (reasoning from statistical information to conclusions about individuals) and default reasoning follow directly from the semantics of random worlds. For example, random worlds captures important patterns of reasoning such as specificity, inheritance, indifference to irrelevant information, and default assumptions of independence. Furthermore, the expressive power of the language used and the intuitive semantics of random worlds allow the method to deal with problems that are beyond the scope of many other nondeductive reasoning systems.},
archivePrefix = {arXiv},
arxivId = {cs.AI/0307056},
author = {Bacchus, Fahiem and Grove, Adam J. and Halpern, Joseph Y. and Koller, Daphne},
doi = {10.1016/S0004-3702(96)00003-3},
eprint = {0307056},
isbn = {1595933182},
issn = {00043702},
journal = {Artif. Intell.},
month = nov,
number = {1-2},
pages = {75--143},
primaryClass = {cs.AI},
title = {From statistical knowledge bases to degrees of belief},
volume = {87},
year = {1996}
}
@article{Petkovic2005a,
abstract = {Pin's variety theorem for positive varieties of string languages and varieties of finite ordered semigroups is proved for trees, i.e., a bijective correspondence between positive varieties of tree languages and varieties of finite ordered algebras is established. This, in turn, is extended to generalized varieties of finite ordered algebras, which corresponds to Steinby's generalized variety theorem. Also, families of tree languages and classes of ordered algebras that are definable by ordered (syntactic or translation) monoids are characterized. {\textcopyright} 2005 Elsevier B.V. All rights reserved.},
author = {Petkovi{\'{c}}, Tatjana and Salehi, Saeed},
doi = {10.1016/j.tcs.2005.07.026},
isbn = {9521215763},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {ordered algebras,ordered monoids,tree automata,tree languages,variety theorem},
month = nov,
number = {1-2},
pages = {1--35},
title = {Positive varieties of tree languages},
volume = {347},
year = {2005}
}
@article{McLean1985,
author = {McLean, John},
doi = {10.1016/0020-0190(85)90065-1},
issn = {00200190},
journal = {Inf. Process. Lett.},
month = feb,
number = {2},
pages = {67--70},
title = {A comment on the ‘basic security theorem' of Bell and LaPadula},
volume = {20},
year = {1985}
}
@article{Kerstan2013a,
abstract = {We investigate some basic questions about the interaction of regular and\nrational relations on words. The primary motivation comes from the study of\nlogics for querying graph topology, which have recently found numerous\napplications. Such logics use conditions on paths expressed by regular\nlanguages and relations, but they often need to be extended by rational\nrelations such as subword or subsequence. Evaluating formulae in such extended\ngraph logics boils down to checking nonemptiness of the intersection of\nrational relations with regular or recognizable relations (or, more generally,\nto the generalized intersection problem, asking whether some projections of a\nregular relation have a nonempty intersection with a given rational relation).\n We prove that for several basic and commonly used rational relations, the\nintersection problem with regular relations is either undecidable (e.g., for\nsubword or su?x, and some generalizations), or decidable with\nnon-primitive-recursive complexity (e.g., for subsequence and its\ngeneralizations). These results are used to rule out many classes of graph\nlogics that freely combine regular and rational relations, as well as to\nprovide the simplest problem related to verifying lossy channel systems that\nhas non-primitive-recursive complexity. We then prove a dichotomy result for\nlogics combining regular conditions on individual paths and rational relations\non paths, by showing that the syntactic form of formulae classi?es them into\neither e?ciently checkable or undecidable cases. We also give examples of\nrational relations for which such logics are decidable even without syntactic\nrestrictions.},
archivePrefix = {arXiv},
arxivId = {1310.7417},
author = {Kerstan, Henning and K{\"{o}}nig, Barbara},
doi = {10.2168/LMCS-9(4:16)2013},
editor = {Koutny, Maciej},
eprint = {1310.7417},
isbn = {2009256492},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {Coalgebra,Markov processes,Probabilistic transition systems,Trace semantics},
month = dec,
number = {4},
pages = {1--44},
title = {Coalgebraic trace semantics for continuous probabilistic transition systems},
volume = {9},
year = {2013}
}
@article{Klin2011,
author = {Klin, Bartek},
doi = {10.1016/j.tcs.2011.03.023},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {structural operational semantics},
month = sep,
number = {38},
pages = {5043--5069},
publisher = {Elsevier B.V.},
title = {Bialgebras for structural operational semantics: An introduction},
volume = {412},
year = {2011}
}
@phdthesis{Kurz2000,
author = {Kurz, Alexander},
month = jul,
school = {University of Munich},
title = {Logics for Coalgebras and Applications to Computer Science},
year = {2000}
}
@article{Shulman2008,
abstract = {Questions of set-theoretic size play an essential role in category theory, especially the distinction between sets and proper classes (or small sets and large sets). There are many different ways to formalize this, and which choice is made can have noticeable effects on what categorical constructions are permissible. In this expository paper we summarize and compare a number of such "set-theoretic foundations for category theory," and describe their implications for the everyday use of category theory. We assume the reader has some basic knowledge of category theory, but little or no prior experience with formal logic or set theory.},
archivePrefix = {arXiv},
arxivId = {0810.1279},
author = {Shulman, Michael A.},
eprint = {0810.1279},
journal = {ArXiv e-prints},
month = oct,
pages = {1--39},
title = {Set theory for category theory},
year = {2008}
}
@article{Power2002,
author = {Power, A. John and Watanabe, Hiroshi},
doi = {10.1016/S0304-3975(01)00024-X},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {2-category,algebra,coalgebra,comonad,distributive,kleisli construction,monad},
month = may,
number = {1-2},
pages = {137--162},
title = {Combining a monad and a comonad},
volume = {280},
year = {2002}
}
@article{Kissig2011,
abstract = {We combine previous work on coalgebraic logic with the coalgebraic traces semantics of Hasuo, Jacobs, and Sokolova.},
archivePrefix = {arXiv},
arxivId = {1103.3239},
author = {Kissig, Christian and Kurz, Alexander},
eprint = {1103.3239},
journal = {ArXiv e-prints},
month = mar,
title = {Generic trace logics},
year = {2011}
}
@article{Bloom1983,
author = {Bloom, Stephen L. and Wright, Jesse B.},
doi = {10.1016/0022-4049(83)90080-4},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jul,
number = {1},
pages = {13--58},
title = {P-varieties - a signature independent characterization of varieties of ordered algebras},
volume = {29},
year = {1983}
}
@article{Kozen1983,
abstract = {In this paper we define and study a propositional ??-calculus L??, which consists essentially of propositional modal logic with a least fixpoint operator. L?? is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version we give an exponential-time decision procedure, small model property, and complete deductive system, theory subsuming the corresponding results for PDL. ?? 1983.},
author = {Kozen, Dexter},
doi = {10.1016/0304-3975(82)90125-6},
issn = {03043975},
journal = {Theor. Comput. Sci.},
number = {3},
pages = {333--354},
title = {Results on the propositional $\mu$-calculus},
volume = {27},
year = {1983}
}
@incollection{Yasuoka2010,
abstract = {Researchers have proposed formal definitions of quantitative information flow based on information theoretic notions such as the Shannon entropy, the min entropy, the guessing entropy, belief, and channel capacity. This paper investigates the hardness of precisely checking the quantitative information flow of a program according to such definitions. More precisely, we study the "bounding problem" of quantitative information flow, defined as follows: Given a program M and a positive real number q, decide if the quantitative information flow of M is less than or equal to q. We prove that the bounding problem is not a k-safety property for any k (even when q is fixed, for the Shannon-entropy-based definition with the uniform distribution), and therefore is not amenable to the self-composition technique that has been successfully applied to checking non-interference. We also prove complexity theoretic hardness results for the case when the program is restricted to loop-free boolean programs. Specifically, we show that the problem is PP-hard for all definitions, showing a gap with non-interference which is coNP-complete for the same class of programs. The paper also compares the results with the recently proved results on the comparison problems of quantitative information flow.},
archivePrefix = {arXiv},
arxivId = {1112.4237},
author = {Yasuoka, Hirotoshi and Terauchi, Tachio},
booktitle = {Comput. Secur. – ESORICS 2010},
doi = {10.1007/978-3-642-15497-3_22},
editor = {Gritzalis, Dimitris},
eprint = {1112.4237},
isbn = {3642154964},
issn = {18758924},
keywords = {Security,program verification,quantitative information flow},
pages = {357--372},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On Bounding Problems of Quantitative Information Flow},
volume = {6345},
year = {2010}
}
@article{Banaschewski1967,
author = {Banaschewski, Bernhard and Bruns, G.},
doi = {10.1007/BF01898828},
issn = {0003889X},
journal = {Arch. der Math.},
number = {4},
pages = {369--377},
title = {Categorical characterization of the MacNeille completion},
volume = {18},
year = {1967}
}
@incollection{Pattinson2001a,
author = {Pattinson, Dirk},
booktitle = {Proc. 18th Symp. Theor. Asp. Comput. Sci. (STACS 2001)},
doi = {10.1007/3-540-44693-1_45},
editor = {{H. Reichel and A. Ferreira}},
number = {Section 2},
pages = {514--526},
series = {Lecture Notes in Computer Science},
title = {Semantical Principles in the Modal Logic of Coalgebras},
year = {2001}
}
@article{Roßiger2000,
abstract = {Coalgebras are of growing importance in theoretical computer science. To develop languages for them is significant for the specification and verification of systems. Modallogic has proved to be suitable for this purpose. So far, most approaches have presented a language to describe only deterministic coalgebras. The present paper introduces a generalization that also covers non-deterministic systems. Models for our modal language are F-coalgebras where the functor F is inductively constructed from constant sets and the identity functor using product, coproduct, exponentiation, and the power set functor. Thus, Kripke-structures constitute a special case. First we introduce a language that is based on a multisorted modal setting: here the sorts are given by the subfunctors of F. Then we consider a restricted language that still has the same expressiveness. It turns out that, for the case of Kripke-structures, the obtained language is equivalent to the “usual” modallogic for these structures. Hence this approach actually constitutes a bridge between modal languages for coalgebras and the modallogic for Kripke-structures. A well-known result from modallogic can be transfered to our setting: for so-called image-finite coalgebras bisimilarity coincides with logical equivalence. Finally, we present a sound and complete deduction calculus in case the constants in F are finite.},
author = {R{\"{o}}{\ss}iger, Martin},
doi = {10.1016/S1571-0661(05)80353-6},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jan,
pages = {294--315},
title = {Coalgebras and Modal Logic},
volume = {33},
year = {2000}
}
@article{Bezhanishvili2000,
abstract = {This paper is the concluding part of [1] and [2], and it investigates the inner structure of the lattice $\Lambda$(MHA) of all varieties of monadic Heyting algebras. For every n ≤ $\omega$, we introduce and investigate varieties of depth n and cluster n, and present two partitions of $\Lambda$(MHA), into varieties of depth n, and into varieties of cluster n. We pay a special attention to the lower part of $\Lambda$(MHA) and investigate finite and critical varieties of monadic Heyting algebras in detail. In particular, we prove that there exist exactly thirteen critical varieties in $\Lambda$(MHA) and that it is decidable whether a given variety of monadic Heyting algebras is finite or not. The representation of $\Lambda$(MHA) is also given. All these provide us with a satisfactory insight into $\Lambda$(MHA). Since $\Lambda$(MHA) is dual to the lattice NExtMIPC of all normal extensions of the intuitionistic modal logic MIPC, we also obtain a clearer picture of the lattice structure of intuitionistic modal logics over MIPC.},
author = {Bezhanishvili, Guram},
doi = {10.1023/A:1005285631357},
journal = {Stud. Log.},
number = {2},
pages = {215--256},
title = {Varieties of Monadic Heyting Algebras. Part III},
volume = {64},
year = {2000}
}
@article{Klin2009a,
author = {Klin, Bartek},
doi = {10.1016/j.ic.2007.10.006},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {structural operational semantics},
month = feb,
number = {2},
pages = {237--257},
publisher = {Elsevier Inc.},
title = {Bialgebraic methods and modal logic in structural operational semantics},
volume = {207},
year = {2009}
}
@article{Adamek2008a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Bloom, Stephen L. and Milius, Stefan},
doi = {10.1093/logcom/exn035},
issn = {0955792X},
journal = {J. Log. Comput.},
number = {6},
pages = {1047--1085},
title = {On algebras with iteration},
volume = {18},
year = {2008}
}
@article{Abramsky1991,
abstract = {Some basic topics in the theory of concurrency are studied from the point of view of denotational semantics, and particularly the “domain theory in logical form” developed by the author. A domain of synchronization trees is defined by means of a recursive domain equation involving the Plotkin powerdomain. The logical counterpart of this domain is described, and shown to be related to it by Stone duality. The relationship of this domain logic to the standard Hennessy-Milner logic for transition systems is studied; the domain logic can be seen as a rational reconstruction of Hennessy-Milner logic from the standpoint of a very general and systematic theory. Finally, a denotational semantics for SCCS based on the domain of synchronization trees is given, and proved fully abstract with respect to bisimulation.},
author = {Abramsky, Samson},
doi = {10.1006/inco.1991.9999},
issn = {08905401},
journal = {Inf. Comput.},
month = jun,
number = {2},
pages = {161--218},
title = {A domain equation for bisimulation},
volume = {92},
year = {1991}
}
@article{Hughes2004,
author = {Hughes, Jesse and Jacobs, Bart},
doi = {10.1016/j.tcs.2004.07.022},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebra,relation lifting,simulation},
month = oct,
number = {1-2},
pages = {71--108},
title = {Simulations in coalgebra},
volume = {327},
year = {2004}
}
@book{Hutchison2010,
author = {Hutchison, David and Mitchell, John C},
doi = {10.1007/978-3-642-15838-4},
editor = {Domingo-Ferrer, Josep and Magkos, Emmanouil},
isbn = {9783642158377},
publisher = {Springer, Berlin, Heidelberg},
title = {UNESCO Chair in Data Privacy, International Conference, PSD 2010, Corfu, Greece, September 22-24, 2010. Proceedings},
year = {2010}
}
@book{Bloom1993,
author = {Bloom, Stephen L. and {\'{E}}sik, Zolt{\'{a}}n},
doi = {10.1007/978-3-642-78034-9},
isbn = {978-3-642-78036-3},
pages = {XV, 630},
publisher = {Springer-Verlag Berlin Heidelberg},
series = {Monographs in Theoretical Computer Science. An EATCS Series},
title = {Iteration Theories},
year = {1993}
}
@incollection{Pole1977,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
booktitle = {Comput. Sci. Log. 19th Int. Work. CSL 2005, 14th Annu. Conf. EACSL, Oxford, UK, August 22-25, 2005. Proc.},
doi = {10.1007/11538363_7},
editor = {Ong, Luke},
issn = {00224812},
month = sep,
number = {3},
pages = {70--86},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A Logic of Coequations},
year = {2005}
}
@article{Lawvere1973,
author = {Lawvere, F. William},
doi = {10.1007/BF02924844},
issn = {0370-7377},
journal = {Rend. del Semin. Mat. e Fis. di Milano},
month = dec,
number = {1},
pages = {135--166},
title = {Metric spaces, generalized logic, and closed categories},
volume = {43},
year = {1973}
}
@article{Power1999,
abstract = {We present a coalgebraic approach to trace equivalence semantics based on lifting behaviour endofunctors for deterministic action to Kleisli categories of monads for non-deterministic choice. In Set, this gives a category with ordinary transition systems as objects and with morphisms characterised in terms of a linear notion of bisimulation. The final object in this category is the canonical abstract model for trace equivalence and can be obtained by extending the final coalgebra of the deterministic action behaviour to the Kleisli category of the non-empty powerset monad. The corresponding final coalgebra semantics is fully abstract with respect to trace equivalence. Discussions with Julian Rathke and with Gordon Plotkin, Alex Simpson and Martin Wehr are gratefully acknowledged. {\textcopyright} 1999 Published by Elsevier Science B. V.},
author = {Power, John and Turi, Daniele},
doi = {10.1016/S1571-0661(05)80319-6},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
number = {1},
pages = {259--274},
publisher = {Elsevier B.V.},
title = {A coalgebraic foundation for linear time semantics},
volume = {29},
year = {1999}
}
@inproceedings{Pattinson2008,
author = {Pattinson, Dirk and Schr{\"{o}}der, Lutz},
booktitle = {Proc. Found. Softw. Sci. Comput. Struct.},
pages = {66--80},
publisher = {Springer},
title = {Beyond rank 1: Algebraic semantics and finite models for coalgebraic logics},
year = {2008}
}
@inproceedings{Goswami2017,
author = {Goswami, Puneet and Madan, Suman},
booktitle = {2017 Int. Conf. Comput. Commun. Autom.},
doi = {10.1109/CCAA.2017.8229787},
isbn = {978-1-5090-6471-7},
keywords = {data anonymization,down specialization,privacy preservation,top-},
month = may,
pages = {139--142},
publisher = {IEEE},
title = {Privacy preserving data publishing and data anonymization approaches: A review},
year = {2017}
}
@inproceedings{Kapulkin2012,
author = {Kapulkin, Krzysztof and Kurz, Alexander and Velebil, Jiř{\'{i}}},
booktitle = {Adv. Modal Log.},
keywords = {coalgebra,modal logic,poset},
pages = {368--385},
title = {Expressiveness of positive coalgebraic logic},
year = {2012}
}
@incollection{James2013,
abstract = {Domain modelling based on UML Class Diagrams is an established industrial practice. In the context of the Railway industry, we show how to utilize such diagrams for verification. This involves the translation of UML Class Diagrams into the algebraic specification language CASL. To this end, we define new Class Diagram institutions and provide suitable institution comorphisms.},
address = {Berlin, Heidelberg},
author = {James, Phillip and Knapp, Alexander and Mossakowski, Till and Roggenbach, Markus},
booktitle = {Recent Trends Algebr. Dev. Tech. 21st Int. Work. WADT 2012},
doi = {10.1007/978-3-642-37635-1_11},
editor = {Mart{\'{i}}-Oliet, Narciso and Palomino, Miguel},
isbn = {978-3-642-37635-1},
issn = {03029743},
pages = {178--194},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Designing domain specific languages -- A craftsman's approach for the railway domain using Casl},
volume = {7841},
year = {2013}
}
@inproceedings{Murray2010,
abstract = {We consider the problem of detecting covert channels within security-enforcing\nobject-capability patterns. Traditional formalisms for reasoning\nabout the security properties of object-capability patterns require\none to be aware, a priori , of all possible mechanisms for covert\ninformation flow that might be present within a pattern, in order\nto detect covert channels within it. We show how the CSP process\nalgebra, and its model-checker FDR, can be applied to overcome this\nlimitation.},
author = {Murray, Toby and Lowe, Gavin},
booktitle = {Form. Asp. Secur. Trust. FAST 2009},
doi = {10.1007/978-3-642-12459-4_7},
editor = {Degano, Pierpaolo and Guttman, Joshua D.},
isbn = {3642124585},
issn = {03029743},
pages = {81--95},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Analysing the information flow properties of object-capability patterns},
volume = {5983},
year = {2010}
}
@incollection{Abramsky2013,
abstract = {Our aim in this paper is to point out a surprising formal connection, between two topics which seem on face value to have nothing to do with each other: relational database theory, and the study of non-locality and contextuality in the foundations of quantum mechanics. We shall show that there is a remarkably direct correspondence between central results such as Bell's theorem in the foundations of quantum mechanics, and questions which arise naturally and have been well-studied in relational database theory.},
archivePrefix = {arXiv},
arxivId = {1208.6416},
author = {Abramsky, Samson},
booktitle = {Search Elegance Theory Pract. Comput.},
doi = {10.1007/978-3-642-41660-6_2},
editor = {Tannen, Val and Wong, Limsoon and Libkin, Leonid and Fan, Wenfei and Tan, Wang-Chiew and Fourman, Michael},
eprint = {1208.6416},
pages = {13--35},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Relational Databases and {B}ell's Theorem},
volume = {8000},
year = {2013}
}
@book{Adamek1990,
address = {New York},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Herrlich, Horst and Strecker, George E.},
keywords = {Category theory,category,theory},
mendeley-tags = {category,theory},
publisher = {Wiley-Interscience},
title = {Abstract and Concrete Categories},
type = {Book},
year = {1990}
}
@article{Isbell1966,
author = {Isbell, John R.},
issn = {1088-9485},
journal = {Bull. New. Ser. Am. Math. Soc.},
language = {EN},
month = jul,
number = {4},
pages = {619--655},
title = {Structure of categories},
volume = {72},
year = {1966}
}
@incollection{Paulson1991,
author = {Paulson, Lawrence C. and Smith, Andrew W.},
booktitle = {Proc. Extensions Log. Program.},
doi = {10.1007/BFb0038699},
editor = {Schroeder-Heister, Peter},
pages = {283--209},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Logic programming, functional programming, and inductive definitions},
year = {1991}
}
@phdthesis{Bernardy2011,
abstract = {This thesis revisits the well-known notion of parametric polymorphism in the light of modern developments in type-theory. Additionally, applica- tions of parametric polymorphism are also presented. The first part of the thesis presents a theoretical investigation of the se- mantics of parametric polymorphism of and within type-theories with de- pendent types. It is shown how the meaning of polymorphic, possibly dependent, types can be reflected within type-theory itself, via a simple syntactic transformation. This self-referential property opens the door to internalise the transformation in type-theory, and we study one possible way to do so. We also examine how the translation relates to various spe- cific features of type-theory, such as proof irrelevance and realizability. The second part is concerned an application of parametric polymorphism relevant to software engineers. We present a schema to reduce polymor- phic properties to equivalent monomorphic properties, for the purpose of testing. Our proof uses parametricity and properties of initial algebras.},
author = {Bernardy, Jean-Philippe},
isbn = {9789173855143},
keywords = {Dependent types,Haskell type-classes,Logical relations,Parametricity,Polymorphism,Realizability,Testing,Types},
school = {Chalmers University of Technology and G{\"{o}}teborg University},
title = {A Theory of Parametric Polymorphism and an Application},
year = {2011}
}
@article{Navarro-Arribas2012,
abstract = {In this paper, we review the role of information fusion in data privacy. To that end, we introduce data privacy, and describe how information and data fusion are used in some fields of data privacy. Our study is focused on the use of aggregation for privacy protections, and record linkage techniques. {\textcopyright} 2011 Elsevier B.V. All rights reserved.},
author = {Navarro-Arribas, Guillermo and Torra, Vicen{\c{c}}},
doi = {10.1016/j.inffus.2012.01.001},
isbn = {1566-2535},
issn = {15662535},
journal = {Inf. Fusion},
keywords = {Data privacy,Information fusion,Microaggregation,Record linkage},
month = oct,
number = {4},
pages = {235--244},
publisher = {Elsevier B.V.},
title = {Information fusion in data privacy: A survey},
volume = {13},
year = {2012}
}
@incollection{Kinoshita1989,
author = {Kinoshita, Y. and Power, A. John},
booktitle = {Proc. Int. Work. Extensions Log. Program.},
doi = {10.1007/3-540-60983-0_12},
isbn = {978-3-540-60983-4},
pages = {177--191},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A fibrational semantics for logic programs},
year = {1989}
}
@incollection{Pavlovic2006,
abstract = {We propose a methodology based on testing as a framework to capture the interactions of a machine represented in a denotational model and the data it manipulates. Using a connection that models machines on the one hand, and the data they manipulate on the other, testing is used to capture the interactions of each with the objects on the other side: just as the data that are input into a machine can be viewed as tests that the machine can be subjected to, the machine can be viewed as a test that can be used to distinguish data. This approach is based on generalizing from duality theories that now are common in semantics to logical connections, which are simply contravariant adjunctions. In the process, it accomplishes much more than simply moving from one side of a duality to the other; it faithfully represents the interactions that embody what is happening as the computation proceeds. Our basic philosophy is that tests can be used as a basis for modeling interactions, as well as processes and the data on which they operate. In more abstract terms, tests can be viewed as formulas of process logics, and testing semantics connects processes and process logics, and assigns computational meanings to both.},
address = {Berlin, Heidelberg},
author = {Pavlovi{\'{c}}, Dusko and Mislove, Michael W. and Worrell, James and Johnson, Michael and Vene, Varmo},
booktitle = {Algebr. Methodol. Softw. Technol.},
doi = {10.1007/11784180_24},
editor = {Johnson, Michael and Vene, Varmo},
isbn = {978-3-540-35633-2},
pages = {308--322},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Testing semantics: connecting processes and process logics},
volume = {4019},
year = {2006}
}
@incollection{Levy2011,
author = {Levy, Paul Blain},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-19805-2_3},
editor = {Hofmann, Martin},
pages = {27--41},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Similarity quotients as final coalgebras},
year = {2011}
}
@inproceedings{Chen2015,
archivePrefix = {arXiv},
arxivId = {1504.02692},
author = {Chen, Liang-Ting and Urbat, Henning},
booktitle = {Proc. 6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.50},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
eprint = {1504.02692},
keywords = {coalgebra,duality,eilenberg's variety theorem,grothendieck fibration},
pages = {50--65},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {A fibrational approach to automata theory},
year = {2015}
}
@article{Bloom1976,
author = {Bloom, Stephen L.},
doi = {10.1016/S0022-0000(76)80030-X},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
month = oct,
number = {2},
pages = {200--212},
title = {Varieties of ordered algebras},
volume = {13},
year = {1976}
}
@article{Jacobs2015,
abstract = {This paper takes a fresh look at the topic of trace semantics in the theory of coalgebras. In the last few years, two approaches, somewhat incomparable at first sight, captured successfully in a coalgebraic setting trace semantics for various types of transition systems. The first development of coalgebraic trace semantics used final coalgebras in Kleisli categories and required some non-trivial assumptions, which do not always hold, even in cases where one can reasonably speak of traces (like for weighted automata). The second development stemmed from the observation that trace semantics can also arise by performing a determinization construction and used final coalgebras in Eilenberg-Moore categories. In this paper, we develop a systematic study in which the two approaches can be studied and compared. Notably, we show that the two different views on trace semantics are equivalent, in the examples where both approaches are applicable.},
author = {Jacobs, Bart and Silva, Alexandra and Sokolova, Ana},
doi = {10.1016/j.jcss.2014.12.005},
isbn = {9783642327834},
issn = {10902724},
journal = {J. Comput. Syst. Sci.},
keywords = {Coalgebra,Eilenberg-Moore category,Kleisli category,Trace semantics},
number = {5},
pages = {859--879},
publisher = {Elsevier Inc.},
title = {Trace semantics via determinization},
volume = {81},
year = {2015}
}
@article{Power2000,
abstract = {Given a class F of weights, one can consider the construction that takes a small category to the free cocompletion of under weighted colimits, for which the weight lies in F. Provided these free F-cocompletions are small, this construction generates a 2-monad on Cat, or more generally on -Cat for monoidal biclosed complete and cocomplete . We develop the notion of a dense 2-monad on -Cat and characterise free F-cocompletions by dense KZ-monads on -Cat. We prove various corollaries about the structure of such 2-monads and their Kleisli 2-categories, as needed for the use of open maps in giving an axiomatic study of bisimulation in concurrency. This requires the introduction of the concept of a pseudo-commutativity for a strong 2-monad on a symmetric monoidal 2-category, and a characterisation of it in terms of structure on the Kleisli 2-category.},
author = {Power, A. John and Cattani, Gian Luca and Winskel, Glynn},
doi = {10.1016/S0022-4049(99)00063-8},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
pages = {273--286},
title = {A representation result for free cocompletions},
volume = {151},
year = {2000}
}
@article{Seely2008,
author = {Seely, Robert A. G.},
doi = {10.1017/S0305004100061284},
issn = {0305-0041},
journal = {Math. Proc. Cambridge Philos. Soc.},
month = oct,
number = {01},
pages = {33},
title = {Locally cartesian closed categories and type theory},
volume = {95},
year = {2008}
}
@book{Harper2016,
author = {Harper, Robert},
doi = {10.1017/CBO9781139342131},
edition = {2},
isbn = {9781139342131},
publisher = {Cambridge University Press},
title = {Practical Foundations for Programming Languages},
year = {2016}
}
@article{Loregian2015,
abstract = {The present note is a recollection of the most striking and useful applications of co/end calculus. We put a considerable effort in making arguments and constructions rather explicit: after having given a series of preliminary definitions, we characterize co/ends as particular co/limits; then we derive a number of results directly from this characterization. The last sections discuss the most interesting examples where co/end calculus serves as a powerful abstract way to do explicit computations in diverse fields like Algebra, Algebraic Topology and Category Theory. The appendices serve to sketch a number of results in theories heavily relying on co/end calculus; the reader who dares to arrive at this point, being completely introduced to the mysteries of co/end fu, can regard basically every statement as a guided exercise.},
archivePrefix = {arXiv},
arxivId = {1501.02503},
author = {Loregian, Fosco},
eprint = {1501.02503},
journal = {ArXiv e-prints},
month = jan,
title = {This is the (co)end, my only (co)friend},
year = {2015}
}
@incollection{Shenoy1990,
address = {Berlin, Heidelberg},
author = {Shenoy, Prakash P and Shafer, Glenn},
booktitle = {Class. Work. Dempster-Shafer Theory Belief Funct.},
doi = {10.1007/978-3-540-44792-4_20},
pages = {499--528},
publisher = {Springer Berlin Heidelberg},
title = {Axioms for Probability and Belief-Function Propagation},
year = {1990}
}
@incollection{Kurz2002,
author = {Kurz, Alexander and Pattinson, Dirk},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/S1571-0661(04)80363-3},
issn = {15710661},
month = oct,
number = {1},
pages = {135--155},
title = {Definability, canonical models, compactness for finitary coalgebraic modal logic},
volume = {65},
year = {2002}
}
@article{Plotkin2001a,
author = {Plotkin, Gordon D. and Power, A. John},
doi = {10.1016/S1571-0661(04)80970-8},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = nov,
pages = {332--345},
title = {Semantics for algebraic operations},
volume = {45},
year = {2001}
}
@article{Litak2016,
abstract = {Relational lattices are obtained by interpreting lattice connectives as natural join and inner union between database relations. Our study of their equational theory reveals that the variety generated by relational lattices has not been discussed in the existing literature. Furthermore, we show that addition of just the header constant to the lattice signature leads to undecidability of the quasiequational theory. Nevertheless, we also demonstrate that relational lattices are not as intangible as one may fear: for example, they do form a pseudoelementary class. We also apply the tools of Formal Concept Analysis and investigate the structure of relational lattices via their standard contexts. Furthermore, we show that the addition of typing rules and singleton constants allows a direct comparison with monotonic relational expressions of Sagiv and Yannakakis.},
author = {Litak, Tadeusz and Mikul{\'{a}}s, Szabolcs and Hidders, Jan},
doi = {10.1016/j.jlamp.2015.11.008},
issn = {23522208},
journal = {J. Log. Algebr. Methods Program.},
keywords = {1,34,38,39,algebraic logic,attention of algebraists,by vadim tropashko,connections,database theory,even those investigating the,introduction and motivation,it does not seem,lattice theory,natural database interpretation proposed,of lattices with a,relational algebra,relational lattices,to have attracted the,we study a class},
month = jun,
number = {4},
pages = {540--573},
publisher = {Elsevier Inc.},
title = {Relational lattices: From databases to universal algebra},
volume = {85},
year = {2016}
}
@article{Reiterman1978,
author = {Reiterman, Jan},
doi = {10.1017/S0004972700008923},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = dec,
number = {03},
pages = {371},
title = {Large algebraic theories with small algebras},
volume = {19},
year = {1978}
}
@article{Leymann1989,
abstract = {The theory of the universal relation model is discussed and different approaches for realizing universal relation systems are presented. Especially, various assumptions made in connection with this data model are discussed, revealing directives for designing semantically clear database schemes. {\textcopyright} 1989.},
author = {Leymann, Frank},
doi = {10.1016/0169-023X(89)90028-1},
issn = {0169023X},
journal = {Data Knowl. Eng.},
keywords = {Access path,Data manipulation,Data model,Database navigation,Database semantic,Object scheme,Query language,Relational database,Universal relation,Window},
month = dec,
number = {4},
pages = {305--320},
title = {A survey of the universal relation model},
volume = {4},
year = {1989}
}
@inproceedings{Wadler1993,
author = {Wadler, Philip},
booktitle = {Proc. 18th Int. Symp. Math. Found. Comput. Sci.},
isbn = {3-540-57182-5},
month = aug,
pages = {185--210},
title = {A Taste of Linear Logic},
year = {1993}
}
@article{Gumm2007,
abstract = {We define an out-degree for F-coalgebras and show that the coalgebras of outdegree at most $\kappa$ form a covariety. As a subcategory of all F-coalgebras, this class has a terminal object, which for many

repository: anqurvanillapy/Type-Theory

repo_name: anqurvanillapy/Type-Theory