text:
= {Electron. Notes Theor. Comput. Sci.},
pages = {252--258},
title = {Relators and Metric Bisimulations},
volume = {11},
year = {1998}
}
@book{Oosten2008,
author = {Oosten, Jaap Van},
doi = {10.1016/S0049-237X(08)80001-8},
isbn = {978-0444515841},
pages = {328},
publisher = {Elsevier Science},
series = {Studies in Logic and the Foundations of Mathematics},
title = {Realizability: An Introduction to its Categorical Side},
year = {2008}
}
@article{Schurmann2008,
abstract = {Tait's method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed lambda-calculi. Historically, these proofs have been extremely difficult to formalize in proof assistants with weak meta-logics, such as Twelf, and yet they are often straightforward in proof assistants with stronger meta-logics. In this paper, we propose structural logical relations as a technique for conducting these proofs in systems with limited meta-logical strength by explicitly representing and reasoning about an auxiliary logic. In support of our claims, we give a Twelf-checked proof of the completeness of an algorithm for checking equality of simply typed lambda-terms.},
author = {Sch{\"{u}}rmann, Carsten and Sarnat, Jeffrey},
doi = {10.1109/LICS.2008.44},
isbn = {9780769531830},
issn = {10436871},
journal = {Proc. - Symp. Log. Comput. Sci.},
pages = {69--80},
title = {Structural logical relations},
year = {2008}
}
@article{Coleman2006,
abstract = {A nonexpansive algebra is a pseudometric algebra in which the operations are all nonexpansive. We study such algebras, particularly in the case of algebras in permutable and n -permutable varieties, leading to new characterizations of such varieties. Free nonexpansive algebras are also investigated.},
author = {Coleman, J. P.},
doi = {10.1007/s00012-006-1997-6},
issn = {0002-5240},
journal = {Algebr. universalis},
month = sep,
number = {4},
pages = {479--494},
publisher = {Birkh{\"{a}}user Basel},
title = {Nonexpansive algebras},
volume = {55},
year = {2006}
}
@article{Hennessy1985a,
author = {Hennessy, Matthew and Milner, Robin},
doi = {10.1145/2455.2460},
issn = {00045411},
journal = {J. ACM},
month = jan,
number = {1},
pages = {137--161},
title = {Algebraic laws for nondeterminism and concurrency},
type = {Journal article},
volume = {32},
year = {1985}
}
@article{Kupke2010,
author = {Kupke, Clemens and Rutten, Jan J.M.M.},
doi = {10.1016/j.ic.2009.10.009},
issn = {08905401},
journal = {Inf. Comput.},
month = dec,
number = {12},
pages = {1398--1420},
publisher = {Elsevier Inc.},
title = {Complete sets of cooperations},
volume = {208},
year = {2010}
}
@article{Kurz2001,
author = {Kurz, Alexander},
doi = {10.1016/S0304-3975(00)00125-0},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebras,modal logic,object-oriented programming,speci{\"{y}}cation,veri{\"{y}}cation},
month = jun,
number = {1-2},
pages = {119--138},
title = {Specifying coalgebras with modal logic},
volume = {260},
year = {2001}
}
@book{Pin2015,
author = {Pin, Jean-{\'{E}}ric},
title = {Mathematical Foundations of Automata Theory},
year = {2015}
}
@inproceedings{Plotkin1980a,
author = {Plotkin, Gordon D.},
booktitle = {Abstr. Softw. Specif.},
pages = {527--553},
publisher = {Springer},
title = {Dijkstra's predicate transformers and Smyth's powerdomains},
type = {Conference proceedings (article)},
year = {1980}
}
@article{Clementino2004,
author = {Clementino, Maria Manuel and Hofmann, Dirk},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Lax algebra,Lax monad,Relation},
number = {3},
pages = {41--60},
title = {On extensions of lax monads},
volume = {13},
year = {2004}
}
@article{Santocanale2008,
abstract = {A $\mu$-algebra is a model of a first-order theory that is an extension of the theory of bounded lattices, that comes with pairs of terms (f, $\mu$x . f) where $\mu$x . f is axiomatized as the least prefixed point of f, whose axioms are equations or equational implications. Standard $\mu$-algebras are complete meaning that their lattice reduct is a complete lattice. We prove that any nontrivial quasivariety of $\mu$-algebras contains a $\mu$-algebra that has no embedding into a complete $\mu$-algebra. We then focus on modal $\mu$-algebras, i.e. algebraic models of the propositional modal $\mu$-calculus. We prove that free modal $\mu$-algebras satisfy a condition-reminiscent of Whitman's condition for free lattices-which allows us to prove that (i) modal operators are adjoints on free modal $\mu$-algebras, (ii) least prefixed points of $\Sigma$1-operations satisfy the constructive relation $\mu$x . f = {n-ary logical or}n ≥ 0 fn (⊥). These properties imply the following statement: the MacNeille-Dedekind completion of a free modal$\mu$ -algebra is a complete modal$\mu$ -algebra and moreover the canonical embedding preserves all the operations in the classComp ($\Sigma$1, $\Pi$1) of the fixed point alternation hierarchy. {\textcopyright} 2007 Elsevier B.V. All rights reserved.},
author = {Santocanale, Luigi},
doi = {10.1016/j.apal.2007.11.001},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {Completions,Least fixed point,Modal $\mu$-calculus},
number = {1},
pages = {27--50},
title = {Completions of $\mu$-algebras},
volume = {154},
year = {2008}
}
@inproceedings{Darnas1982,
address = {New York, New York, USA},
author = {Damas, Luis and Milner, Robin},
booktitle = {Proc. 9th ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '82},
doi = {10.1145/582153.582176},
isbn = {0897910656},
pages = {207--212},
publisher = {ACM Press},
title = {Principal type-schemes for functional programs},
year = {1982}
}
@inproceedings{Patra2010,
abstract = {This work proposes an algebraic model for classical information theory. We first give an algebraic model of probability theory. Information theoretic constructs are based on this model. In addition to theoretical insights provided by our model one obtains new computational and analytical tools. Several important theorems of classical probability and information theory are presented in the algebraic framework.},
archivePrefix = {arXiv},
arxivId = {1006.0355},
author = {Patra, Manas K. and Braunstein, Samuel L.},
booktitle = {2010 IEEE Int. Symp. Inf. Theory},
doi = {10.1109/ISIT.2010.5513650},
eprint = {1006.0355},
isbn = {978-1-4244-7892-7},
month = jun,
pages = {2708--2712},
publisher = {IEEE},
title = {An algebraic approach to information theory},
year = {2010}
}
@incollection{Moshier2009,
abstract = {The full subcategory of proximity lattices equipped with some additional structure (a certain form of negation) is equivalent to the category of compact Hausdorff spaces. Using the Stone-Gelfand-Naimark duality, we know that the category of proximity lattices with negation is dually equivalent to the category of real C * algebras. The aim of this paper is to give a new proof for this duality, avoiding the construction of spaces. We prove that the category of C * algebras is equivalent to the category of skew frames with negation, which appears in the work of Moshier and Jung on the bitopological nature of Stone duality.},
author = {Moshier, M. Andrew and Petrişan, Daniela},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-03741-2_20},
editor = {Kurz, Alexander and Lenisa, Marina and Tarlecki, Andrzej},
isbn = {978-3-642-03740-5},
pages = {284--299},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A Duality Theorem for Real C^∗ Algebras},
volume = {5728},
year = {2009}
}
@incollection{Alfalayleh2016,
abstract = {In this paper, we consider the unordered pseudo-tree matching problem, which is a problem of, given two unordered labeled trees P and T , finding all occurrences of P in T via such many-one embeddings that preserve node labels and parent-child relationship. This problem is closely related to tree pattern matching problem for XPath queries with child axis only. If m > w , we present an efficient algorithm that solves the problem in time using O ( hm / w + m log( w )/ w ) space and O ( m log( w )) preprocessing on a unit-cost arithmetic RAM model with addition, where m is the number of nodes in P , n is the number of nodes in T , h is the height of T , and w is the word length. We also discuss a modification of our algorithm for the unordered tree homeomorphism problem, which corresponds to a tree pattern matching problem for XPath queries with descendant axis only.},
author = {Alfalayleh, Mousa and Brankovic, Ljiljana},
booktitle = {Comb. Algorithms. IWOCA 2014},
doi = {10.1007/978-3-319-19315-1_3},
editor = {Jan, Kratochv{\'{i}}l and Miller, Mirka and Froncek, Dalibor},
isbn = {978-3-319-44542-7},
issn = {0018-9219},
pages = {24--36},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {Quantifying Privacy: A Novel Entropy-Based Measure of Disclosure Risk},
volume = {8986},
year = {2015}
}
@book{Makkai1993,
author = {Makkai, Michael},
isbn = {0821825658},
pages = {106},
publisher = {American Mathematical Society},
series = {Memoirs of the American Mathematical Society},
title = {Duality and Definability in First Order Logic},
year = {1993}
}
@incollection{VanBreugel2005a,
abstract = {Metric labelled transition systems are labelled transition systems whose states and actions form (pseudo)metric spaces. These systems can capture a large class of timed transition systems, including systems with uncountably many states and uncountable nondeterminism. In this paper a behavioural pseudometric is introduced for metric labelled transition systems. The behavioural distance between states, a nonnegative real number, captures the similarity of the behaviour of those states. The smaller the distance, the more alike the states are. In particular, the distance between states is 0 iff they are bisimilar. Three different characterisations of this pseudometric are given: a fixed point, a logical and a coinductive characterisation. These generalise the fixed point, logical and coinductive characterisations of bisimilarity. {\textcopyright} Springer-Verlag Berlin Heidelberg 2005.},
author = {van Breugel, Franck},
booktitle = {Int. Conf. Concurr. Theory},
doi = {10.1007/11539452_14},
editor = {Abadi, Mart{\'{i}}n and de Alfaro, Luca},
isbn = {978-3-540-28309-6},
issn = {03029743},
pages = {141--155},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A behavioural pseudometric for metric labelled transition systems},
volume = {3653},
year = {2005}
}
@book{Admek2003a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Porst, Hans-E.},
booktitle = {Math. Struct. Comput. Sci.},
doi = {10.1017/S0960129502003882},
isbn = {0960129502},
issn = {09601295},
number = {2},
pages = {201--232},
title = {On varieties and covarieties in a category},
volume = {13},
year = {2003}
}
@article{Centazzo2004,
author = {Centazzo, C and Rosick{\'{y}}, Jiř{\'{i}} and Vitale, Enrico M.},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
keywords = {limit doctrine},
number = {2},
pages = {141--146},
title = {A characterization of locally D-presentable categories},
volume = {45},
year = {2004}
}
@article{PierangelaSamarati2001,
author = {Samarati, P.},
doi = {10.1109/69.971193},
issn = {10414347},
journal = {IEEE Trans. Knowl. Data Eng.},
number = {6},
pages = {1010--1027},
title = {Protecting respondents identities in microdata release},
volume = {13},
year = {2001}
}
@inproceedings{Agrawal2012,
author = {Agrawal, Manindra and Akshay, Sundararaman and Genest, Blaise and Thiagarajan, P. S.},
booktitle = {Log. Comput. Sci.},
title = {Approximate Verification of the Symbolic Dynamics of Markov Chains},
year = {2012}
}
@book{Gierz2003,
abstract = {Information content and programming semantics are just two of the applications of the mathematical concepts of order, continuity and domains. This authoritative and comprehensive account of the subject will be an essential handbook for all those working in the area. An extensive index and bibliography make this an ideal sourcebook for all those working in domain theory.},
address = {Cambridge},
author = {Gierz, Gerhard and Hofmann, Karl H. and Keimel, Klaus and Lawson, Jimmie D. and Mislove, Michael W. and Scott, Dana S.},
doi = {10.1017/CBO9780511542725},
isbn = {9780511542725},
month = apr,
publisher = {Cambridge University Press},
title = {Continuous Lattices and Domains},
type = {Book},
year = {2003}
}
@phdthesis{Tzevelekos2008,
author = {Tzevelekos, Nikos},
school = {University of Oxford},
title = {Nominal Game Semantics},
year = {2008}
}
@article{Jacobs2006,
author = {Jacobs, Bart},
doi = {10.1016/j.ic.2005.03.006},
issn = {08905401},
journal = {Inf. Comput.},
month = apr,
number = {4},
pages = {561--587},
title = {Distributive laws for the coinductive solution of recursive equations},
volume = {204},
year = {2006}
}
@inproceedings{Enqvist2015,
archivePrefix = {arXiv},
arxivId = {1501.07215},
author = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
booktitle = {Proc. 2015 30th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2015.41},
eprint = {1501.07215},
isbn = {978-1-4799-8875-4},
issn = {10436871},
keywords = {-coalgebra,Automata,Bisimulation invariance,Coalgebra,Modal mu-calculus,Monadic second-order logic,automata,bisimulation invariance,modal mu-calculus,monadic second-order logic},
month = jul,
pages = {353--365},
publisher = {IEEE},
title = {Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras},
volume = {2015-July},
year = {2015}
}
@article{Hohle2014,
author = {H{\"{o}}hle, Ulrich},
doi = {10.1016/j.fss.2013.03.010},
issn = {0165-0114},
journal = {Fuzzy Sets Syst.},
keywords = {-algebra,Categorical neighborhood axiom,Lower separation axiom,Many valued topology,Non-commutative topology,Ordered monad,Quantaloid enriched category,Quantaloid-enriched topology,Regularity,Smooth Borel probability measure,Spectrum of C*-algebra,categorical neighborhood axiom,lower separation axiom,many valued topology,non-commutative topology,ordered monad,quantaloid enriched category,quantaloid-enriched topology,regularity,smooth borel probability measure,spectrum of c},
pages = {166--210},
publisher = {Elsevier},
title = {Categorical foundations of topology with applications to quantaloid enriched topological spaces},
volume = {256},
year = {2014}
}
@article{Breiman2001,
abstract = {There are two cultures in the use of statistical modeling to reach conclusions from data. One assumes that the data are generated by a given stochastic data model. The other uses algorithmic models and treats the data mechanism as unknown. The statistical community has been committed to the almost exclusive use of data models. This commit-ment has led to irrelevant theory, questionable conclusions, and has kept statisticians from working on a large range of interesting current prob-lems. Algorithmic modeling, both in theory and practice, has developed rapidly in fields outside statistics. It can be used both on large complex data sets and as a more accurate and informative alternative to data modeling on smaller data sets. If our goal as a field is to use data to solve problems, then we need to move away from exclusive dependence on data models and adopt a more diverse set of tools.},
archivePrefix = {arXiv},
arxivId = {0010},
author = {Breiman, Leo},
doi = {10.2307/2676681},
eprint = {0010},
isbn = {08834237},
issn = {08834237},
journal = {Stat. Sci.},
number = {3},
pages = {199--231},
pmid = {10511666},
title = {Statistical Modeling: The Two Cultures},
volume = {16},
year = {2001}
}
@incollection{Cirstea2017a,
abstract = {{\textcopyright} Corina C{\^{i}}rstea, Shunsuke Shimizu, and Ichiro Hasuo; licensed under Creative Commons License CC-BY. We initiate a study of automata-based model checking for previously proposed quantitative linear time logics interpreted over coalgebras. Our results include: (i) an automata-theoretic characterisation of the semantics of these logics, based on a notion of extent of a quantitative parity automaton, (ii) a study of the expressive power of B{\"{u}}chi variants of such automata, with implications on the expressiveness of fragments of the logics considered, and (iii) a na{\"{i}}ve algorithm for computing extents, under additional assumptions on the domain of truth values.},
author = {C{\^{i}}rstea, C. and Shimizu, S. and Hasuo, I.},
booktitle = {7th Conf. Algebr. Coalgebra Comput. Sci. (CALCO 2017)},
doi = {10.4230/LIPIcs.CALCO.2017.7},
editor = {K{\"o}nig, Filippo Bonchi and Barbara},
isbn = {9783959770330},
issn = {18688969},
keywords = {Coalgebra,Linear time logic,Parity automaton,Quantitative logic},
pages = {7:1----7:18},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Parity automata for quantitative linear time logics},
volume = {72},
year = {2017}
}
@book{Levy2003,
abstract = {Call-by-push-value is a programming language paradigm that, surprisingly, breaks down the call-by-value and call-by-name paradigms into simple primitives. This monograph, written for graduate students and researchers, exposes the call-by-push-value structure underlying a remarkable range of semantics, including operational semantics, domains, possible worlds, continuations and games.},
author = {Levy, Paul Blain},
month = nov,
publisher = {Springer},
title = {Call-by-push-value: A Functional/imperative Synthesis},
type = {Book},
year = {2003}
}
@book{Aceto2007,
abstract = {Formal methods is the term used to describe the specification and verification of software and software systems using mathematical logic. Various methodologies have been developed and incorporated into software tools. An important subclass is distributed systems. There are many books that look at particular methodologies for such systems, e.g. CSP, process algebra. This book offers a more balanced introduction for graduate students that describes the various approaches, their strengths and weaknesses, and when they are best used. Milner's CCS and its operational semantics are introduced, together with notions of behavioural equivalence based on bisimulation techniques and with variants of Hennessy-Milner modal logics. Later in the book, the presented theories are extended to take timing issues into account. The book has arisen from various courses taught in Iceland and Denmark and is designed to give students a broad introduction to the area, with exercises throughout.},
author = {Aceto, Luca and Ing{\'{o}}lfsd{\'{o}}ttir, Anna and Larsen, Kim Guldstrand and Srba, Jiri},
isbn = {9780521875462},
pages = {302},
publisher = {Cambridge University Press},
title = {Reactive Systems: Modelling, Specification and Verification},
year = {2007}
}
@article{Dawid2001,
author = {Dawid, A.P.},
doi = {10.1023/A:1016734104787},
issn = {10122443},
journal = {Ann. Math. Artif. Intell.},
keywords = {Basic separoid,Belief function,Belief independence,Covariance independence,Directed Markov,Distributive,Graphoid,Hyper independence,Irrelevance,Join-orthogonal,Lattice,Linear independence,Markov,Meta independence,Modular,Natural independence},
number = {1/4},
pages = {335--372},
title = {Separoids: A mathematical framework for conditional independence and irrelevance},
volume = {32},
year = {2001}
}
@article{Wilkinson2012a,
author = {Wilkinson, Toby},
doi = {10.1016/j.entcs.2012.08.021},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {bisimulation,coalgebra,enriched logical connection,preordered set,simulation},
month = sep,
pages = {323--336},
publisher = {Elsevier B.V.},
title = {A characterisation of expressivity for coalgebraic bisimulation and simulation},
volume = {286},
year = {2012}
}
@book{Lambek1966,
author = {Lambek, Joachim},
doi = {10.1007/BFb0077265},
isbn = {978-3-540-03607-4},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Completions of Categories},
volume = {24},
year = {1966}
}
@inproceedings{Dwork2011a,
abstract = {Differential privacy describes a promise, made by a data curator to a data subject: you will not be affected, adversely or otherwise, by allowing your data to be used in any study, no matter what other studies, data sets, or information from other sources is available. At their best, differentially private database mechanisms can make confidential data widely available for accurate data analysis, without resorting to data clean rooms, institutional review boards, data usage agreements, restricted views, or data protection plans. To enjoy the fruits of the research described in this tutorial, the data analyst must accept that raw data can never be accessed directly and that eventually data utility is consumed: overly accurate answers to too many questions will destroy privacy. The goal of algorithmic research on differential privacy is to postpone this inevitability as long as possible.},
author = {Dwork, Cynthia},
booktitle = {2011 IEEE 52nd Annu. Symp. Found. Comput. Sci.},
doi = {10.1109/FOCS.2011.88},
isbn = {978-0-7695-4571-4},
issn = {02725428},
keywords = {differential privacy,privacy,private data analysis},
month = oct,
pages = {1--2},
publisher = {IEEE},
title = {The Promise of Differential Privacy: A Tutorial on Algorithmic Techniques},
year = {2011}
}
@article{Adamek2006a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1017/S0960129506005706},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = nov,
number = {06},
pages = {1085},
title = {Iterative algebras at work},
volume = {16},
year = {2006}
}
@article{Kupke2011,
abstract = {Coalgebras can be seen as a natural abstraction of Kripke frames. In the same sense, coalgebraic logics are generalised modal logics. In this paper, we give an overview of the basic tools, techniques and results that connect coalgebras and modal logic. We argue that coalgebras unify the semantics of a large range of different modal logics (such as probabilistic, graded, relational, conditional) and discuss unifying approaches to reasoning at this level of generality. We review languages defined in terms of the so-called cover modality, languages induced by predicate liftings as well as their common categorical abstraction, and present (abstract) results on completeness, expressiveness and complexity in these settings, both for basic languages as well as a number of extensions, such as hybrid languages and fixpoints.},
author = {Kupke, Clemens and Pattinson, Dirk},
doi = {10.1016/j.tcs.2011.04.023},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebra,modal logic},
month = sep,
number = {38},
pages = {5070--5094},
publisher = {Elsevier B.V.},
title = {Coalgebraic semantics of modal logics: An overview},
volume = {412},
year = {2011}
}
@book{Goldblatt1993a,
author = {Goldblatt, Robert},
isbn = {1-881526-23-2},
publisher = {Center for the Study of Language and Information, Stanford},
series = {CSLI Lecture Notes},
title = {Mathematics of modality},
type = {Book},
year = {1993}
}
@article{VanBreugel2005,
abstract = {Discrete notions of behavioural equivalence sit uneasily with semantic models featuring quantitative data, like probabilistic transition systems. In this paper, we present a pseudometric on a class of probabilistic transition systems yielding a quantitative notion of behavioural equivalence. The pseudometric is defined via the terminal coalgebra of a functor based on a metric on the space of Borel probability measures on a metric space. States of a probabilistic transition system have distance 0 if and only if they are probabilistic bisimilar. We also characterize our distance function in terms of a real-valued modal logic.},
author = {van Breugel, Franck and Worrell, James},
doi = {10.1016/j.tcs.2004.09.035},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {bisimilarity,probabilistic,probabilistic bisimilarity,probabilistic transition system,pseudometric,real-valued modal logic,terminal coalgebra},
month = feb,
number = {1},
pages = {115--142},
publisher = {Elsevier},
title = {A behavioural pseudometric for probabilistic transition systems},
volume = {331},
year = {2005}
}
@article{Adamek1974,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
journal = {Comment. Math. Univ. Carolinae},
number = {4},
pages = {589--602},
title = {Free algebras and automata realizations in the language of categories},
volume = {15},
year = {1974}
}
@article{Almeida1989,
author = {Almeida, Jorge},
journal = {Port. Math.},
number = {3},
pages = {313--328},
title = {Residually finite congruences and quasi-regular subsets in uniform algebras},
volume = {46},
year = {1989}
}
@incollection{Dahlqvist2011,
abstract = {Fusion is arguably the simplest way to combine modal logics. For normal modal logics with Kripke semantics, many properties such as completeness and decidability are known to transfer from the component logics to their fusion. In this paper we investigate to what extent these results can be generalised to the case of arbitrary coalgebraic logics. Our main result generalises a construction of Kracht and Wolter and confirms that completeness transfers to fusion for a large class of logics over coalgebraic semantics. This result is independent of the rank of the logics and relies on generalising the notions of distance and box operator to coalgebraic models.},
author = {Dahlqvist, Fredrik and Pattinson, Dirk},
booktitle = {Proc. 4th Int. Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-22944-2_12},
editor = {Corradini, Andrea and Klin, Bartek and C{\^{i}}rstea, Corina},
pages = {161--175},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On the fusion of coalgebraic logics},
year = {2011}
}
@incollection{Cohen2013,
abstract = {In intensional type theory, it is not always possible to form the quotient of a type by an equivalence relation. However, quotients are extremely useful when formalizing mathematics, especially in algebra. We provide a Coq library with a pragmatic approach in two complementary components. First, we provide a framework to work with quotient types in an axiomatic manner. Second, we program construction mechanisms for some specific cases where it is possible to build a quotient type. This library was helpful in implementing the types of rational fractions, multivariate polynomials, field extensions and real algebraic numbers.},
author = {Cohen, Cyril},
booktitle = {4th Int. Conf. Interact. Theorem Proving, 2013},
doi = {10.1007/978-3-642-39634-2_17},
editor = {Blazy, Sandrine and Paulin-Mohring, Christine and Pichardie, David},
isbn = {9783642396335},
issn = {03029743},
keywords = {Coq,Formalization of mathematics,Quotient types},
pages = {213--228},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Pragmatic quotient types in Coq},
year = {2013}
}
@article{Scott1976,
abstract = {The meaning of many kinds of expressions in programming languages can be taken as elements of certain spaces of “partial” objects. In this report these spaces are modeled in one universal domain ${\bf P} \omega $, the set of all subsets of the integers. This domain renders the connection of this semantic theory with the ordinary theory of number theoretic (especially general recursive) functions clear and straightforward.},
author = {Scott, Dana},
doi = {10.1137/0205037},
isbn = {0097-5397},
issn = {0097-5397},
journal = {SIAM J. Comput.},
month = sep,
number = {3},
pages = {522--587},
title = {Data Types as Lattices},
volume = {5},
year = {1976}
}
@inproceedings{Staton2013,
author = {Staton, Sam},
booktitle = {28th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2013.58},
isbn = {978-1-4799-0413-6},
month = jun,
number = {1},
pages = {519--519},
publisher = {IEEE},
title = {Instances of Computational Effects: An Algebraic Perspective},
year = {2013}
}
@article{Power2000a,
abstract = {We introduce the notion of discrete countable Lawvere V-theory and study constructions that may be made on it. The notion of discrete countable Lawvere V-theory extends that of ordinary countable Lawvere theory by allowing the homsets of an ordinary countable Lawvere theory to become homobjects of a well-behaved axiomatically defined category such as that of $\omega$-cpo's. Every discrete countable Lawvere V-theory induces a V-enriched monad, equivalently a strong monad, on V. We show that discrete countable Lawvere V-theories allow us to model all the leading examples of computational effects other than continuations, and that they are closed under constructions of sum, tensor and distributive tensor, which are the fundamental ways in which one combines such effects. We also show that discrete countable Lawvere V-theories are closed under taking an image, allowing one to treat observation as a mathematical primitive in modelling effects.},
author = {Power, John},
doi = {10.1007/11548133_22},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Lawvere theory,Monad},
pages = {83--93},
title = {Enriched Lawvere theories},
volume = {6},
year = {2000}
}
@article{Barr1993a,
author = {Barr, Michael},
doi = {2010.1016/0304-3975(93)90076-6},
issn = {0304-3975},
journal = {Theor. Comput. Sci.},
month = jun,
number = {2},
pages = {299--315},
title = {Terminal coalgebras in well-founded set theory},
type = {Journal article},
volume = {114},
year = {1993}
}
@inproceedings{Li2007,
author = {Li, Ninghui and Li, Tiancheng and Venkatasubramanian, Suresh},
booktitle = {2007 IEEE 23rd Int. Conf. Data Eng.},
doi = {10.1109/ICDE.2007.367856},
isbn = {1-4244-0802-4},
number = {3},
pages = {106--115},
publisher = {IEEE},
title = {$t$-Closeness: Privacy Beyond $k$-Anonymity and $l$-Diversity},
year = {2007}
}
@article{Goldblatt1985,
author = {Goldblatt, Robert},
doi = {10.2307/2274230},
issn = {0022-4812},
journal = {J. Symb. Log.},
month = jun,
number = {02},
pages = {412--422},
title = {On the role of the Baire Category Theorem and Dependent Choice in the foundations of logic},
volume = {50},
year = {1985}
}
@article{VanHorn2017,
abstract = {We consider the question of extending propositional logic to a logic of plausible reasoning, and posit four requirements that any such extension should satisfy. Each is a requirement that some property of classical propositional logic be preserved in the extended logic; as such, the requirements are simpler and less problematic than those used in Cox's Theorem and its variants. As with Cox's Theorem, our requirements imply that the extended logic must be isomorphic to (finite-set) probability theory. We also obtain specific numerical values for the probabilities, recovering the classical definition of probability as a theorem, with truth assignments that satisfy the premise playing the role of the “possible cases.”},
archivePrefix = {arXiv},
arxivId = {1706.05261},
author = {{Van Horn}, Kevin S.},
doi = {10.1016/j.ijar.2017.06.003},
eprint = {1706.05261},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Bayesian,Carnap,Cox,Jaynes,Logic,Probability},
pages = {309--332},
publisher = {Elsevier Inc.},
title = {From propositional logic to plausible reasoning: A uniqueness theorem},
volume = {88},
year = {2017}
}
@incollection{Balan2011a,
abstract = {We investigate how finitary functors on Set can be extended or lifted to finitary functors on Preord and Poset and discuss applications to coalgebra.},
author = {Balan, Adriana and Kurz, Alexander},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-22944-2_7},
pages = {85--99},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Finitary functors: From $\mathbf{Set}$ to $\mathbf{Preord}$ and $\mathbf{Poset}$},
type = {Book part (with own title)},
volume = {6859},
year = {2011}
}
@article{Erne1993,
author = {Ern{\'{e}}, Marcel and Koslowski, J{\"{u}}rgen and Melton, Austin C. and Strecker, George E.},
doi = {10.1111/j.1749-6632.1993.tb52513.x},
issn = {0077-8923},
journal = {Ann. N. Y. Acad. Sci.},
month = dec,
pages = {103--125},
title = {A Primer on Galois Connections},
volume = {704},
year = {1993}
}
@article{Trnkova1969,
author = {Trnkov{\'{a}}, V{\v{e}}ra},
journal = {Comment. Math. Univ. Carolinae},
number = {2},
pages = {323--352},
title = {Some properties of set functors},
volume = {10},
year = {1969}
}
@article{Fung2010,
abstract = {The collection of digital information by governments, corporations, and individuals has created tremendous opportunities for knowledge- and information-based decision making. Driven bymutual benefits, or by regu- lations that require certain data to be published, there is a demand for the exchange and publication of data among various parties. Data in its original form, however, typically contains sensitive information about in- dividuals, and publishing such data will violate individual privacy. The current practice in data publishing reliesmainly on policies and guidelines as to what types of data can be published and on agreements on the use of published data. This approach alone may lead to excessive data distortion or insufficient protection. Privacy-preserving data publishing (PPDP) provides methods and tools for publishing useful information while preserving data privacy. Recently, PPDP has received considerable attention in research communi- ties, and many approaches have been proposed for different data publishing scenarios. In this survey, we will systematically summarize and evaluate different approaches to PPDP, study the challenges in prac- tical data publishing, clarify the differences and requirements that distinguish PPDP from other related problems, and propose future research directions},
author = {Fung, Benjamin C. M. and Wang, Ke and Chen, Rui and Yu, Philip S.},
doi = {10.1145/1749603.1749605},
isbn = {ISSN$\sim$$\sim$26176633},
issn = {03600300},
journal = {ACM Comput. Surv.},
month = jun,
number = {4},
pages = {1--53},
pmid = {16914745},
title = {Privacy-preserving data publishing},
volume = {42},
year = {2010}
}
@article{Doberkat2012,
author = {Doberkat, Ernst-Erich},
doi = {10.2178/jsl/1333566646},
issn = {0022-4812},
journal = {J. Symb. Log.},
language = {EN},
month = jun,
number = {2},
pages = {687--716},
title = {A stochastic interpretation of propositional dynamic logic: expressivity},
volume = {77},
year = {2012}
}
@article{Rosicky1994,
abstract = {M. Richter has proved that whenever a class K of ?-structures has a finitary first-order axiomatization then the inclusion K ? Str ? preserves all existing directed colimits (see [7]). We will generalize this result to classes of ?-structures having an infinitary first-order axiomatization in a larger signature ?'. We will also show that, as categories, these classes have a natural characterization.},
author = {Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1007/BF00878503},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
keywords = {Mathematics and Statistics},
month = mar,
number = {1},
pages = {71--76},
publisher = {Springer Netherlands},
title = {More on directed colimits of models},
volume = {2},
year = {1994}
}
@incollection{Aydemir2007,
author = {Aydemir, Brian and Bohannon, Aaron and Weirich, Stephanie},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/j.entcs.2007.01.028},
issn = {15710661},
keywords = {coq,nominal reasoning techniques,variable binding},
month = jun,
number = {5},
pages = {69--77},
title = {Nominal Reasoning Techniques in Coq},
volume = {174},
year = {2007}
}
@article{Kurz2012a,
author = {Kurz, Alexander and Leal, Raul Andres},
doi = {10.1016/j.tcs.2012.03.027},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = apr,
pages = {88--116},
publisher = {Elsevier B.V.},
title = {Modalities in the stone age: A comparison of coalgebraic logics},
volume = {430},
year = {2012}
}
@article{Moss2008,
author = {Moss, Lawrence S.},
doi = {10.1093/logcom/exn095},
issn = {0955-792X},
journal = {J. Log. Comput.},
month = dec,
number = {5},
pages = {1101--1111},
title = {A note on expressive coalgebraic logics for finitary Set functors},
volume = {20},
year = {2008}
}
@article{Avery2014,
abstract = {The Giry monad on the category of measurable spaces sends a space to a space of all probability measures on it. There is also a finitely additive Giry monad in which probability measures are replaced by finitely additive probability measures. We give a characterisation of both finitely and countably additive probability measures in terms of integration operators that is a correction and extension of a result claimed by Sturtz. A counterexample to Sturtz's claim is given in the appendix. This correspondence gives a new description of the Giry monads, which is then used to show that the Giry monads arise as the codensity monads of forgetful functors from certain categories of convex sets and affine maps to the category of measurable spaces.},
archivePrefix = {arXiv},
arxivId = {1410.4432},
author = {Avery, Tom},
eprint = {1410.4432},
journal = {ArXiv e-prints},
pages = {1--27},
title = {Codensity and the Giry monad},
year = {2014}
}
@article{Brown1993,
abstract = {We define a relational quantale to be a quantale whose elements are relations on a set A, ordered by inclusion and forming a monoid under relational composition. Such quantales have been studied in several areas of theoretical computer science, and constitute a sound and complete class of models for non-commutative linear logic. We show that every quantale is isomorphic to a relational quantale, and investigate the classification of quantales according to properties of their representations as relational quantales. {\textcopyright} 1993.},
author = {Brown, Carolyn and Gurr, Doug},
doi = {10.1016/0022-4049(93)90169-T},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = mar,
number = {1},
pages = {27--42},
title = {A representation theorem for quantales},
volume = {85},
year = {1993}
}
@article{Garner2014a,
author = {Garner, Richard},
doi = {10.1016/j.jpaa.2014.02.018},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {11},
pages = {1973--1988},
publisher = {Elsevier B.V.},
title = {Lawvere theories, finitary monads and Cauchy-completion},
volume = {218},
year = {2014}
}
@incollection{Jacobs1996,
author = {Jacobs, Bart},
booktitle = {Object Orientat. with Parallelism Persistence},
doi = {10.1007/978-1-4613-1437-0_5},
editor = {Freitag, B. and Jones, C.B. and Lengauer, C. and Schek, HJ.},
pages = {83--103},
publisher = {Springer, Boston, MA},
series = {The Kluwer International Series in Engineering and Computer Science},
title = {Objects And Classes, Co-Algebraically},
volume = {370},
year = {1996}
}
@article{Alpern1987,
abstract = {A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi automaton that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjunction is the original. The characterizations also give insight into techniques required to prove a large class of safety and liveness properties.},
author = {Alpern, Bowen and Schneider, Fred B.},
doi = {10.1007/BF01782772},
issn = {0178-2770},
journal = {Distrib. Comput.},
month = sep,
number = {3},
pages = {117--126},
title = {Recognizing safety and liveness},
volume = {2},
year = {1987}
}
@article{Jacobs2010a,
abstract = {Abstract. This paper starts from the elementary observation that what is usually called a predicate lifting in coalgebraic modal logic is in fact an endomap of indexed categories. This leads to a systematic review of basic results in predicate logic for functors and monads , ...},
author = {Jacobs, Bart},
journal = {Preprint},
title = {Predicate logic for functors and monads},
year = {2010}
}
@article{Klin2009,
author = {Klin, Bartek},
doi = {10.1016/j.entcs.2006.11.018},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {algebra,bialgebra,category theory,coalgebra,structural operational semantics},
month = may,
number = {1},
pages = {33--43},
title = {Bialgebraic methods in structural operational semantics},
volume = {175},
year = {2007}
}
@article{Street2012,
abstract = {This is a report on aspects of the theory and use of monoidal categories. The first section introduces the main concepts through the example of the category of vector spaces. String notation is explained and shown to lead naturally to a link between knot theory and monoidal categories. The second section reviews the light thrown on aspects of representation theory by the machinery of monoidal category theory, such as braidings and convolution. The category theory of Mackey functors is reviewed in the third section. Some recent material and a conjecture concerning monoidal centres is included. The fourth and final section looks at ways in which monoidal categories are, and might, be used for new invariants of low-dimensional manifolds and for the field theory of theoretical physics.},
archivePrefix = {arXiv},
arxivId = {1201.2991},
author = {Street, Ross},
eprint = {1201.2991},
issn = {13701444},
journal = {Bull. Belgian Math. Soc.},
keywords = {and phrases,braiding,day convolution,duoidal category,enriched category,finite,functor,green functor,joyal species,mackey,manifold invariant,monoidal category,string diagram,topological quantum field theory},
month = jan,
number = {5},
pages = {769--820},
title = {Monoidal categories in, and linking, geometry and algebra},
volume = {19},
year = {2012}
}
@article{Schroder2015,
author = {Schr{\"{o}}der, Lutz and Pattinson, Dirk and Litak, Tadeusz},
doi = {10.1093/logcom/exv043},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {bisimulation invariance,coalgebra,correspondence theory,gaifman locality,modal logic},
month = jul,
pages = {exv043},
title = {A Van Benthem/Rosen theorem for coalgebraic predicate logic},
year = {2015}
}
@article{Hartonas1998,
author = {Hartonas, Chrysafis},
doi = {10.1016/S0304-3975(97)00233-8},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = jul,
number = {1-2},
pages = {193--222},
title = {Duality for modal $\mu$-logics},
type = {Journal article},
volume = {202},
year = {1998}
}
@inproceedings{Kammar2013,
address = {New York, New York, USA},
author = {Kammar, Ohad and Lindley, Sam and Oury, Nicolas},
booktitle = {Proc. 18th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '13},
doi = {10.1145/2500365.2500590},
isbn = {9781450323260},
keywords = {algebraic effects,continuations,effect handlers,effect typing,haskell,instance monad,modularity},
pages = {145},
publisher = {ACM Press},
title = {Handlers in action},
year = {2013}
}
@article{Kiefer2011,
abstract = {Checking two probabilistic automata for equivalence has been shown to be a key problem for efficiently establishing various behavioural and anonymity properties of probabilistic systems. In recent experiments a randomised equivalence test based on polynomial identity testing outperformed deterministic algorithms. In this paper we show that polynomial identity testing yields efficient algorithms for various generalisations of the equivalence problem. First, we provide a randomized NC procedure that also outputs a counterexample trace in case of inequivalence. Second, we show how to check for equivalence two probabilistic automata with (cumulative) rewards. Our algorithm runs in deterministic polynomial time, if the number of reward counters is fixed. Finally we show that the equivalence problem for probabilistic visibly pushdown automata is logspace equivalent to the Arithmetic Circuit Identity Testing problem, which is to decide whether a polynomial represented by an arithmetic circuit is identically zero.},
archivePrefix = {arXiv},
arxivId = {1112.4644},
author = {Kiefer, Stefan and Murawski, Andrzej S. and Ouaknine, Jo{\"{e}}l and Wachter, Bj{\"{o}}rn and Worrell, James},
eprint = {1112.4644},
journal = {ArXiv e-prints},
month = dec,
title = {On the Complexity of the Equivalence Problem for Probabilistic Automata},
year = {2011}
}
@article{Hashmi2018,
abstract = {Literature on business process compliance (BPC) has predominantly focused on the alignment of the regulatory rules with the design, verification and validation of business processes. Previously surveys on BPC have been conducted with specific context in mind; however, the literature on BPC management research is largely sparse and does not accumulate a detailed understanding on existing literature and related issues faced by the domain. This survey provides a holistic view of the literature on existing BPC management approaches, and categories them based on different compliance management strategies in the context of formulated research questions. A systematic literature approach is used where search terms pertaining keywords were used to identify literature related to the research questions from scholarly databases. From initially 183 papers, we selected 79 papers related to the themes of this survey published between 2000–2015. The survey results reveal that mostly compliance management approaches center around three distinct categories namely: design-time (28%), run-time (32%) and auditing (10%). Also, organisational and internal control based compliance management frameworks (21%) and hybrid approaches make (9%) of the surveyed approaches. Furthermore, open research challenges and gaps are identified and discussed with respect to the compliance problem.},
author = {Hashmi, Mustafa and Governatori, Guido and Lam, Ho-Pun and Wynn, Moe Thandar},
doi = {10.1007/s10115-017-1142-1},
issn = {0219-1377},
journal = {Knowl. Inf. Syst.},
keywords = {Business process compliance,Business processes,Compliance management frameworks,Normative requirements,Norms compliance,business process compliance,business processes,compliance management frameworks,normative requirements,norms compliance},
month = jan,
publisher = {Springer London},
title = {Are we done with business process compliance: state of the art and challenges ahead},
year = {2018}
}
@article{Dinur2003,
author = {Dinur, Irit and Nissim, Kobbi},
doi = {10.1145/773153.773173},
isbn = {1581136706},
journal = {Proc. twenty-second ACM SIGMOD-SIGACT-SIGART Symp. Princ. database Syst.},
keywords = {data reconstruction,integrity and security,subset-sums with noise},
pages = {202--210},
title = {Revealing information while preserving privacy},
year = {2003}
}
@article{Ki1984,
author = {Imieli{\'{n}}ski, Tomasz and Lipski, Witold},
doi = {10.1016/0022-0000(84)90077-1},
isbn = {9780080465210},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
month = feb,
number = {1},
pages = {80--102},
title = {The relational model of data and cylindric algebras},
volume = {28},
year = {1984}
}
@article{Lack2005,
author = {Lack, Stephen},
doi = {10.1007/s10485-005-2958-5},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
keywords = {2-monad,lax limit,lax morphism,monoidal functor},
month = jun,
number = {3},
pages = {189--203},
title = {Limits for Lax Morphisms},
volume = {13},
year = {2005}
}
@article{Kelly2009,
author = {Kelly, Gregory Maxwell},
doi = {10.1017/S0004972700005724},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = apr,
pages = {221--237},
title = {Two addenda to the author's ‘Transfinite constructions'},
volume = {26},
year = {1982}
}
@article{Gumm2009a,
author = {Gumm, H. Peter},
doi = {10.1016/j.tcs.2008.09.057},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = mar,
number = {12-13},
pages = {1129--1142},
publisher = {Elsevier B.V.},
title = {Copower functors},
volume = {410},
year = {2009}
}
@article{Bonchi2015,
abstract = {We propose an abstract framework for modelling state-based systems with internal behaviour as e.g. given by silent or $\epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator † to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems and non-deterministic transducers.},
archivePrefix = {arXiv},
arxivId = {1402.4062},
author = {Bonchi, Filippo and Milius, Stefan and Silva, Alexandra and Zanasi, Fabio},
doi = {10.1016/j.tcs.2015.03.024},
eprint = {1402.4062},
isbn = {9783662441237},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Coalgebras on kleisli categories,Epsilon transitions,Mazurkiewicz traces,Non-deterministic transducers,Parametrized fixpoint operator,Trace semantics},
pages = {102--126},
publisher = {Elsevier B.V.},
title = {Killing epsilons with a dagger: A coalgebraic study of systems with algebraic label structure},
volume = {604},
year = {2015}
}
@inproceedings{Gibbons2000,
abstract = {Remote procedure calls are computationally expensive, because network round-trips take several orders of magnitude longer than local interactions. One common technique for amortizing this cost is to batch together multiple independent requests into one com- pound request. Batching requests amounts to serializing the abstract syntax tree of a small program, in order to transmit it and run it remotely. The standard representation for abstract syntax is to use free monads; we show that free applicative functors are actually a better choice of representation for this scenario.},
address = {New York, New York, USA},
author = {Gibbons, Jeremy},
booktitle = {Proc. 9th Int. Symp. Haskell - Haskell 2016},
doi = {10.1145/2976002.2976005},
isbn = {9781450344340},
keywords = {batched request,free applicative functor,free monad,remote procedure call},
pages = {45--50},
publisher = {ACM Press},
title = {Free delivery (functional pearl)},
year = {2016}
}
@incollection{Gehrke2009,
abstract = {This is a theoretical paper giving the extended Stone duality perspective on the recently discovered connection between duality theory as studied in non-classical logic and theoretical computer science and the algebraic theory of finite state automata. As a bi-product we obtain a general result about profinite completion, namely, that it is the dual under extended Stone duality of the recognisable languages over the original algebra equipped with certain residuation operations.},
author = {Gehrke, Mai},
booktitle = {3rd Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-03741-2_17},
editor = {Kurz, Alexander and Lenisa, Marina and Tarlecki, Andrzej},
isbn = {3642037402},
issn = {03029743},
pages = {236--250},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Stone Duality and the Recognisable Languages over an Algebra},
year = {2009}
}
@article{Blumensath2011,
author = {Blumensath, Achim},
doi = {10.1016/j.tcs.2011.02.037},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = jul,
number = {29},
pages = {3463--3486},
publisher = {Elsevier B.V.},
title = {Recognisability for algebras of infinite trees},
volume = {412},
year = {2011}
}
@book{Martin-Lof1984,
address = {Napoli},
author = {Martin-Löf, Per},
isbn = {88-7088-105-9},
number = {June},
publisher = {Bibliopolis},
series = {Studies in Proof Theory},
title = {Intuitionistic Type Theory},
year = {1984}
}
@inproceedings{Hinze2000,
address = {New York, New York, USA},
author = {Hinze, Ralf},
booktitle = {Proc. fifth ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '00},
doi = {10.1145/351240.351258},
isbn = {1581132026},
pages = {186--197},
publisher = {ACM Press},
title = {Deriving backtracking monad transformers},
year = {2000}
}
@incollection{Bezhanishvili2007a,
abstract = {In this paper we discuss a uniform method for constructing free modal and distributive modal algebras. This method draws on works by (Abramsky 2005) and (Ghilardi 1995). We revisit the theory of normal forms for modal logic and derive a normal form representation for positive modal logic. We also show that every finitely generated free modal and distributive modal algebra axiomatised by equations of rank 1 is a reduct of a temporal algebra.},
author = {Bezhanishvili, Nick and Kurz, Alexander},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-540-73859-6_10},
editor = {Mossakowski, Till and Montanari, Ugo and Haveraaen, Magne},
pages = {143--157},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Free modal algebras: A coalgebraic perspective},
type = {Book part (with own title)},
volume = {4624},
year = {2007}
}
@article{Montanari2014,
author = {Montanari, Ugo and Sammartino, Matteo},
doi = {10.1016/j.tcs.2014.03.009},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = mar,
number = {2010},
pages = {1--37},
publisher = {Elsevier B.V.},
title = {A network-conscious $\pi$-calculus and its coalgebraic semantics},
volume = {1},
year = {2014}
}
@article{Mardare2012,
archivePrefix = {arXiv},
arxivId = {arXiv:1506.03843v1},
author = {Mio, Matteo},
doi = {10.2168/LMCS-8(4:18)2012},
editor = {Gr{\"{a}}del, Erich},
eprint = {arXiv:1506.03843v1},
isbn = {2111201200},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,axiomatization,logics,markov processes,probabilistic and stochastic modal},
month = nov,
number = {4},
pages = {1--39},
title = {Probabilistic modal $\mu$-calculus with independent product},
volume = {8},
year = {2012}
}
@article{Leinster1998,
archivePrefix = {arXiv},
arxivId = {math/9810017},
author = {Leinster, Tom},
eprint = {9810017},
journal = {ArXiv e-prints},
month = oct,
pages = {1--10},
primaryClass = {math},
title = {Basic Bicategories},
year = {1998}
}
@article{Coumans2012a,
abstract = {Canonical extension has proven to be a powerful tool in algebraic study of propositional logics. In this paper we describe a generalisation of the theory of canonical extension to the setting of first order logic. We define a notion of canonical extension for coherent categories. These are the categorical analogues of distributive lattices and they provide categorical semantics for coherent logic, the fragment of first order logic in the connectives ???, ???, 0, 1 and ???. We describe a universal property of our construction and show that it generalises the existing notion of canonical extension for distributive lattices. Our new construction for coherent categories has led us to an alternative description of the topos of types, introduced by Makkai (1981) in [22]. This allows us to give new and transparent proofs of some properties of the action of the topos of types construction on morphisms. Furthermore, we prove a new result relating, for a coherent category C, its topos of types to its category of models (in Set). ?? 2012 Elsevier B.V.},
author = {Coumans, Dion},
doi = {10.1016/j.apal.2012.07.002},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {Canonical extension,Coherent categories,Topos of types},
month = dec,
number = {12},
pages = {1940--1961},
publisher = {Elsevier B.V.},
title = {Generalising canonical extension to the categorical setting},
volume = {163},
year = {2012}
}
@book{Sorensen2006,
author = {S{\o}rensen, Morten Heine and Urzyczyn, Pawel},
editor = {Abramsky, Samson and Artemov, S. and Gabbay, D. M. and Kechris, A. and Pillay, A. and Shore, R. A.},
isbn = {978-0-444-52077-7},
pages = {456},
publisher = {Elsevier Inc.},
series = {Studies in Logic and the Foundations of Mathematics},
title = {Lectures on the Curry-Howard Isomorphisms},
year = {2006}
}
@article{Rosicky1995,
author = {Rosick{\'{y}}, Jiř{\'{i}} and Tholen, Walter},
doi = {10.1016/0022-4049(94)00035-H},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jan,
number = {2},
pages = {189--208},
title = {Accessibility and the solution set condition},
volume = {98},
year = {1995}
}
@incollection{Pattinson2015,
author = {Pattinson, Dirk and Schr{\"{o}}der, Lutz},
booktitle = {Proc. 31st Conf. Math. Found. Program. Semant.},
doi = {10.1016/j.entcs.2015.12.019},
issn = {15710661},
keywords = {bisimulation,comodels,completeness,equational logic},
month = dec,
pages = {315--331},
publisher = {Elsevier B.V.},
series = {Electronic Notes in Theoretical Computer Science},
title = {Sound and Complete Equational Reasoning over Comodels},
year = {2015}
}
@article{Manes2015,
author = {Manes, Ernie},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Burnside-Frobenius lemma,Conjugacy class of subgroups,Extensive category},
number = {17},
pages = {599--619},
title = {Extensive categories and the size of an orbit},
volume = {30},
year = {2015}
}
@inproceedings{Wu2014,
abstract = {Algebraic effect handlers are a powerful means for describing effectful computations. They provide a lightweight and orthogonal technique to define and compose the syntax and semantics of different effects. The semantics is captured by handlers, which are functions that transform syntax trees. Unfortunately, the approach does not support syntax for scoping constructs, which arise in a number of scenarios. While handlers can be used to provide a limited form of scope, we demonstrate that this approach constrains the possible interactions of effects and rules out some desired semantics. This paper presents two different ways to capture scoped constructs in syntax, and shows how to achieve different semantics by reordering handlers. The first approach expresses scopes using the existing algebraic handlers framework, but has some limitations. The problem is fully solved in the second approach where we introduce higher-order syntax.},
address = {New York, New York, USA},
author = {Wu, Nicolas and Schrijvers, Tom and Hinze, Ralf},
booktitle = {Proc. 2014 ACM SIGPLAN Symp. Haskell - Haskell '14},
doi = {10.1145/2633357.2633358},
isbn = {9781450330411},
issn = {03621340},
pages = {1--12},
publisher = {ACM Press},
title = {Effect handlers in scope},
year = {2014}
}
@article{Pavlovic1999,
author = {Pavlovi{\'{c}}, Dusko and Pratt, Vaughan},
doi = {10.1016/S1571-0661(05)80272-5},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jan,
pages = {103--117},
title = {On coalgebra of real numbers},
volume = {19},
year = {1999}
}
@article{Dupont2003,
abstract = {Starting from known examples of factorization systems in 2-categories, we discuss possible definitions of proper factorization system in a 2-category. We focus our attention on the construction of the free proper factorization system on a given 2-category. ?? 2003 Elsevier Science B.V. All rights reserved.},
author = {Dupont, M. and Vitale, E. M.},
doi = {10.1016/S0022-4049(02)00244-X},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {1-2},
pages = {65--86},
title = {Proper factorization systems in 2-categories},
volume = {179},
year = {2003}
}
@article{Eilenberg1967,
author = {Eilenberg, Samuel and Wright, Jesse B.},
doi = {10.1016/S0019-9958(67)90670-5},
issn = {00199958},
journal = {Inf. Control},
number = {4},
pages = {452--470},
title = {Automata in general algebras},
volume = {11},
year = {1967}
}
@article{Barr1970a,
author = {Barr, Michael},
doi = {10.1007/BF01111838},
issn = {0025-5874},
journal = {Math. Zeitschrift},
number = {4},
pages = {307--322},
title = {Coequalizers and free triples},
volume = {116},
year = {1970}
}
@article{Crans2003,
author = {Crans, Sjoerd E},
doi = {10.1023/A:1024186923002},
issn = {15730514},
journal = {K-Theory},
month = jan,
number = {1},
pages = {39--105},
title = {Localizations of Transfors},
volume = {28},
year = {2003}
}
@incollection{Capretta2009,
author = {Capretta, Venanzio and Uustalu, Tarmo and Vene, Varmo},
booktitle = {Form. Methods Found. Appl. SBMF 2009},
doi = {10.1007/978-3-642-10452-7_7},
editor = {Oliveira, Marcel Vin{\'{i}}cius Medeiros and Woodcock, Jim},
isbn = {3642104517},
issn = {03029743},
pages = {84--100},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Corecursive Algebras: A Study of General Structured Corecursion},
volume = {5902},
year = {2009}
}
@phdthesis{Fong2012,
abstract = {In this dissertation we develop a new formal graphical framework for causal reasoning. Starting with a review of monoidal categories and their associated graphical languages, we then revisit probability theory from a categorical perspective and introduce Bayesian networks, an existing structure for describing causal relationships. Motivated by these, we propose a new algebraic structure, which we term a causal theory. These take the form of a symmetric monoidal category, with the objects representing variables and morphisms ways of deducing information about one variable from another. A major advantage of reasoning with these structures is that the resulting graphical representations of morphisms match well with intuitions for flows of information between these variables. These categories can then be modelled in other categories, providing concrete interpretations for the variables and morphisms. In particular, we shall see that models in the category of measurable spaces and stochastic maps provide a slight generalisation of Bayesian networks, and naturally form a category themselves. We conclude with a discussion of this category, classifying the morphisms and discussing some basic universal constructions. ERRATA: (i) Pages 41-42: Objects of a causal theory are words, not collections, in $V$, and we include swaps as generating morphisms, subject to the identities defining a symmetric monoidal category. (ii) Page 46: A causal model is a strong symmetric monoidal functor.},
archivePrefix = {arXiv},
arxivId = {1301.6201},
author = {Fong, Brendan},
eprint = {1301.6201},
month = jan,
school = {University of Oxford},
title = {Causal Theories: A Categorical Perspective on Bayesian Networks},
type = {Master of Science in Mathematics and the Foundations of Computer Science},
year = {2012}
}
@article{Lack2012,
abstract = {We study limits in 2-categories whose objects are categories with extra structure and whose morphisms are functors preserving the structure only up to a coherent comparison map, which may or may not be required to be invertible. This is done using the framework of 2-monads. In order to characterize the limits which exist in this context, we need to consider also the functors which do strictly preserve the extra structure. We show how such a 2-category of weak morphisms which is "enhanced", by specifying which of these weak morphisms are actually strict, can be thought of as category enriched over a particular base cartesian closed category F. We give a complete characterization, in terms of F-enriched category theory, of the limits which exist in such 2-categories of categories with extra structure. ?? 2011 Elsevier Inc..},
archivePrefix = {arXiv},
arxivId = {1104.2111},
author = {Lack, Stephen and Shulman, Michael},
doi = {10.1016/j.aim.2011.08.014},
eprint = {1104.2111},
issn = {00018708},
journal = {Adv. Math. (N. Y).},
keywords = {2-Category,2-Monad,Category with structure,Enriched category,Lax morphism,Limit,Weak morphism},
month = jan,
number = {1},
pages = {294--356},
publisher = {Elsevier Inc.},
title = {Enhanced 2-categories and limits for lax morphisms},
volume = {229},
year = {2012}
}
@article{Evfimievski2010,
abstract = {We present a novel definition of privacy in the framework of offline (retroactive) database query auditing. Given information about the database, a description of sensitive data, and assumptions about users' prior knowledge, our goal is to determine if answering a past user's query could have led to a privacy breach. According to our definition, an audited property A is private, given the disclosure of property B, if no user can gain confidence in A by learning B, subject to prior knowledge constraints. Privacy is not violated if the disclosure of B causes a loss of confidence in A. The new notion of privacy is formalized using the well-known semantics for reasoning about knowledge, where logical properties correspond to sets of possible worlds (databases) that satisfy these properties. Database users are modelled as either possibilistic agents whose knowledge is a set of possible worlds, or as probabilistic agents whose knowledge is a probability distribution on possible worlds. We analyze the new privacy notion, show its relationship with the conventional approach, and derive criteria that allow the auditor to test privacy efficiently in some important cases. In particular, we prove characterization theorems for the possibilistic case, and study in depth the probabilistic case under the assumption that all database records are considered a-priori independent by the user, as well as under more relaxed (or absent) prior-knowledge assumptions. In the probabilistic case we show that for certain families of distributions there is no efficient algorithm to test whether an audited property A is private given the disclosure of a property B, assuming P NP. Nevertheless, for many interesting families, such as the family of product distributions, we obtain algorithms that are efficient both in theory and in practice.},
author = {Evfimievski, Alexandre and Fagin, Ronald and Woodruff, David},
doi = {10.1145/1870103.1870105},
isbn = {9781605581088},
issn = {00045411},
journal = {J. ACM},
month = dec,
number = {1},
pages = {1--45},
title = {Epistemic privacy},
volume = {58},
year = {2010}
}
@article{Cubitt2015,
abstract = {The spectral gap -- the difference in energy between the ground state and the first excited state -- is one of the most important properties of a quantum many-body system. Quantum phase transitions occur when the spectral gap vanishes and the system becomes critical. Much of physics is concerned with understanding the phase diagrams of quantum systems, and some of the most challenging and long-standing open problems in theoretical physics concern the spectral gap, such as the Haldane conjecture that the Heisenberg chain is gapped for integer spin, proving existence of a gapped topological spin liquid phase, or the Yang-Mills gap conjecture (one of the Millennium Prize problems). These problems are all particular cases of the general spectral gap problem: Given a quantum many-body Hamiltonian, is the system it describes gapped or gapless? Here we show that this problem is undecidable, in the same sense as the Halting Problem was proven to be undecidable by Turing. A consequence of this is that the spectral gap of certain quantum many-body Hamiltonians is not determined by the axioms of mathematics, much as Goedels incompleteness theorem implies that certain theorems are mathematically unprovable. We extend these results to prove undecidability of other low temperature properties, such as correlation functions. The proof hinges on simple quantum many-body models that exhibit highly unusual physics in the thermodynamic limit.},
archivePrefix = {arXiv},
arxivId = {arXiv:1502.04135v1},
author = {Cubitt, Toby S. and Perez-Garcia, David and Wolf, Michael M.},
doi = {10.1038/nature16059},
eprint = {arXiv:1502.04135v1},
isbn = {0028-0836},
issn = {0028-0836},
journal = {Nature},
month = dec,
number = {7581},
pages = {207--211},
pmid = {26659181},
publisher = {Nature Publishing Group},
title = {Undecidability of the spectral gap},
volume = {528},
year = {2015}
}
@article{Kuich1991,
abstract = {We generalize the following two language- and automata-theoretic results to ??-continuous semirings. • (i) The family of languages accepted by finite automata is the smallest class containing all finite languages and closed under union, product and star (Kleene's Theorem). • (ii) The family of languages accepted by pushdown automata is the family ofcontext-free languages. ?? 1991.},
author = {Kuich, Werner},
doi = {10.1016/0304-3975(91)90147-T},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = feb,
number = {1},
pages = {137--150},
title = {Automata and languages generalized to $\omega$-continuous semirings},
volume = {79},
year = {1991}
}
@article{Clairambault2014,
abstract = {Seely's paper Locally cartesian closed categories and type theory (Seely 1984) contains a well-known result in categorical type theory: that the category of locally cartesian closed categories is equivalent to the category of Martin-Lof type theories with $\Pi$, $\Sigma$ and extensional identity types. However, Seely's proof relies on the problematic assumption that substitution in types can be interpreted by pullbacks. Here we prove a corrected version of Seely's theorem: that the Be ́nabou–Hofmann interpretation of Martin-Lo ̈f type theory in locally cartesian closed categories yields a biequivalence of 2-categories. To facilitate the technical development, we employ categories with families as a substitute for syntactic Martin-Lo ̈f type theories. As a second result, we prove that if we remove $\Pi$-types, the resulting categories with families with only $\Sigma$ and extensional identity types are biequivalent to left exact categories.},
author = {Clairambault, Pierre and Dybjer, Peter},
doi = {10.1017/S0960129513000881},
journal = {Math. Struct. Comput. Sci.},
number = {6},
title = {The biequivalence of locally cartesian closed categories and Martin-l{\"{o}}f type theories},
volume = {24},
year = {2014}
}
@article{Garc??a2010,
author = {{Guti{\'{e}}rrez Garc{\'{i}}a}, Javier and Mardones-P{\'{e}}rez, Iraide and {de Prada Vicente}, Mar{\'{i}}a Angeles and Zhang, Dexue},
doi = {10.1002/malq.200810044},
issn = {09425616},
journal = {Math. Log. Q.},
keywords = {??-adjunction,??-relation,Category enriched over a unital quantale,Contravariant fuzzy galois connection,Covariant fuzzy galois connection,Girard quantale,Unital quantale},
month = mar,
number = {2},
pages = {131--147},
title = {Fuzzy Galois connections categorically},
volume = {56},
year = {2010}
}
@incollection{Gehrke2011a,
abstract = {We put forward a zero-knowledge based definition of privacy. Our\nnotion is strictly stronger than the notion of differential\nprivacy and is particularly attractive when modeling privacy in\nsocial networks. We furthermore demonstrate that it can be\nmeaningfully achieved for tasks such as computing averages,\nfractions, histograms, and a variety of graph parameters and\nproperties, such as average degree and distance to connectivity.\nOur results are obtained by establishing a connection between\nzero-knowledge privacy and sample complexity, and by leveraging\nrecent sublinear time algorithms.},
author = {Gehrke, Johannes and Lui, Edward and Pass, Rafael},
booktitle = {Theory Cryptogr. TCC 2011},
doi = {10.1007/978-3-642-19571-6_26},
editor = {Ishai, Yuval},
isbn = {9783642195709},
issn = {03029743},
pages = {432--449},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Towards Privacy for Social Networks: A Zero-Knowledge Based Definition of Privacy},
volume = {6597},
year = {2011}
}
@article{Esik1997,
author = {{\'{E}}sik, Zolt{\'{a}}n},
doi = {10.1016/S0304-3975(96)00240-X},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = apr,
number = {1},
pages = {217--283},
title = {Completeness of Park induction},
volume = {177},
year = {1997}
}
@article{Lai2017,
abstract = {For a small quantaloid $\mathcal{Q}$ we consider four fundamental 2-monads $\mathbb{T}$ on $\mathcal{Q}\text{-}{\bf Cat}$, given by the presheaf 2-monad $\mathbb{P}$ and the copresheaf 2-monad $\mathbb{P}^{\dag}$, as well as their two composite 2-monads, and establish that they all laxly distribute over $\mathbb{P}$. These four 2-monads therefore admit lax extensions to the category $\mathcal{Q}\text{-}{\bf Dist}$ of $\mathcal{Q}$-categories and their distributors. We characterize the corresponding $(\mathbb{T},\mathcal{Q})$-categories in each of the four cases, leading us to both known and novel categorical structures.},
archivePrefix = {arXiv},
arxivId = {1605.04489},
author = {Lai, Hongliang and Shen, Lili and Tholen, Walter},
eprint = {1605.04489},
journal = {Theory Appl. Categ.},
keywords = {2016,and phrases,c hongliang lai,copresheaf monad,double copresheaf monad,double presheaf,lax distributive law,lax monad extension,lax $\lambda$ -algebra,lili shen and walter,monad,permission to copy for,presheaf monad,private use granted,q -closure,q -interior space,quantaloid,space,tholen},
number = {21},
pages = {736--768},
title = {Lax distributive laws for topology, II},
volume = {32},
year = {2017}
}
@incollection{Barr1971,
author = {Barr, Michael},
booktitle = {Exact Categ. Categ. Sheaves},
doi = {10.1007/BFb0058580},
isbn = {978-3-540-05678-2},
pages = {1--120},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Exact Categories},
year = {1971}
}
@incollection{Pavlovic2012a,
abstract = {Formal Concept Analysis (FCA) begins froma context, given as a binary relation between some objects and some attributes, and derives a lattice of concepts, where each concept is given as a set of objects and a set of attributes, such that the first set consists of all objects that satisfy all attributes in the second, and vice versa. Many applications, though, provide contexts with quantitative information, telling not justwhether an object satisfies an attribute, but also quantifying this satisfaction. Contexts in this form arise as rating matrices in recommender systems, as occurrence matrices in text analysis, as pixel intensitymatrices in digital image processing, etc. Such applications have attracted a lot of attention, and several numeric extensions of FCA have been proposed. We propose the framework of proximity sets (proxets), which subsume partially ordered sets (posets) as well as metric spaces. One feature of this approach is that it extracts from quantified contexts quantified concepts, and thus allows full use of the available information. Another feature is that the categorical approach allows analyzing any universal properties that the classical FCA and the new versions may have, and thus provides structural guidance for aligning and combining the approaches.},
archivePrefix = {arXiv},
arxivId = {arXiv:1204.5802v1},
author = {Pavlovi{\'{c}}, Dusko},
booktitle = {Proc. 10th Int. Conf. Form. Concept Anal.},
doi = {10.1007/978-3-642-29892-9_24},
editor = {Domenach, Florent and Ignatov, Dmitry I. and Poelmans, Jonas},
eprint = {arXiv:1204.5802v1},
isbn = {9783642298912},
issn = {03029743},
keywords = {concept analysis,enriched category,semantic completion,universal property},
pages = {260--277},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Quantitative Concept Analysis},
year = {2012}
}
@inproceedings{Jung2008,
author = {Jung, Achim and Moshier, M. Andrew and Vickers, Steven},
booktitle = {Proc. 24th Conf. Math. Found. Program. Semant. (MFPS XXIV)},
doi = {10.1016/j.entcs.2008.10.013},
issn = {15710661},
month = oct,
pages = {209--229},
publisher = {Elsevier},
title = {Presenting dcpos and dcpo algebras},
volume = {218},
year = {2008}
}
@article{KLIN2004,
abstract = {An abstract coalgebraic approach to well-structured relations on processes is presented, based on notions of tests and test suites. Preorders and equivalences on processes are modelled as coalgebras for behaviour endofunctors lifted to a category of test suites. The general framework is specialized to the case of finitely branching labelled transition systems. It turns out that most equivalences from the so-called van Glabbeek spectrum can be described by well-structured test suites. As an immediate application, coinductive proof principles are described for these equivalences, in particular for trace equivalence.},
author = {Klin, Bartek},
doi = {10.1016/j.entcs.2004.02.029},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {coalgebra,coinduction,van glabbeek spectrum},
month = dec,
pages = {201--218},
title = {A Coalgebraic Approach to Process Equivalence and a Coinduction Principle for Traces},
volume = {106},
year = {2004}
}
@inproceedings{Kupke2008a,
abstract = {We give a sound and complete derivation system for the valid formulas in the ﬁnitary version of Moss' coalgebraic logic, for coalgebras of arbitrary type},
author = {Kupke, Clemens and Kurz, Alexander},
booktitle = {Adv. Modal Log.},
keywords = {coalgebra,coalgebraic logic,completeness,modal logic},
pages = {193--217},
publisher = {College Publications},
title = {Completeness of the finitary Moss logic},
volume = {7},
year = {2008}
}
@article{Urbat2016,
abstract = {Eilenberg-type correspondences, relating varieties of languages (e.g. of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. Numerous such correspondences are known in the literature. We demonstrate that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a generic variety theorem that covers e.g. Wilke's and Pin's work on $\infty$-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two previous categorical approaches of Boja\'nczyk and of Ad\'amek et al. In addition it gives a number of new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.},
archivePrefix = {arXiv},
arxivId = {1602.05831},
author = {Urbat, Henning and Ad{\'{a}}mek, Jiř{\'{i}} and Chen, Liang-Ting and Milius, Stefan},
eprint = {1602.05831},
journal = {ArXiv Prepr.},
title = {One Eilenberg theorem to rule them all},
year = {2016}
}
@article{Barr2008,
author = {Barr, Michael and Kennison, John F. and Raphael, Robert},
journal = {Theory Appl. Categ.},
keywords = {duality,fixed categories,sober objects},
number = {15},
pages = {504--542},
title = {Isbell duality},
volume = {20},
year = {2008}
}
@phdthesis{Tanaka2005,
author = {Tanaka, Miki},
pages = {167},
school = {University of Edinburgh},
title = {Pseudo-Distributive Laws and a Unified Framework for Variable Binding},
year = {2005}
}
@article{Hansen2009,
author = {Hansen, Helle Hvid and Kupke, Clemens and Pacuit, Eric},
doi = {10.2168/LMCS-5(2:2)2009},
editor = {Mossakowski, Till},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,behavioural,bisimulation,equivalence,invariance,neighbourhood semantics,non-normal modal logic},
month = apr,
number = {2},
pages = {1--38},
title = {Neighbourhood Structures: Bisimilarity and Basic Model Theory},
volume = {5},
year = {2009}
}
@article{Adamek2014,
abstract = {The category of all monads over many-sorted sets (and over other "set-like" categories) is proved to have coequalizers and strong cointersections. And a general diagram has a colimit whenever all the monads involved preserve monomorphisms and have arbitrarily large joint pre-fixpoints. In contrast, coequalizers fail to exist e.g. for monads over the (presheaf) category of graphs. For more general categories we extend the results on coproducts of monads from [2]. We call a monad separated if, when restricted to monomorphisms, its unit has a complement. We prove that every collection of separated monads with arbitrarily large joint pre-fixpoints has a coproduct. And a concrete formula for these coproducts is presented.},
archivePrefix = {arXiv},
arxivId = {1409.3805},
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
eprint = {1409.3805},
journal = {ArXiv e-prints},
month = sep,
pages = {1--26},
title = {Colimits of Monads},
year = {2014}
}
@inproceedings{Jacobs2013,
author = {Jacobs, Bart},
booktitle = {2013 28th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2013.13},
isbn = {978-1-4799-0413-6},
keywords = {-probabilistic system,duality,effect algebra,giry monad,measurable space},
month = jun,
pages = {83--92},
publisher = {IEEE},
title = {Measurable Spaces and Their Effect Logic},
year = {2013}
}
@book{Barendregt1984a,
author = {Barendregt, Henk},
isbn = {0444875085},
pages = {621},
publisher = {North Holland},
series = {Studies in Logic},
title = {The Lambda Calculus: Its Syntax and Semantics},
volume = {103},
year = {1984}
}
@article{Jacobs2012b,
author = {Jacobs, Bart and Mandemaker, Jorik},
doi = {10.1007/s10701-012-9654-8},
issn = {0015-9018},
journal = {Found. Phys.},
keywords = {Effect algebra,Limit and colimit,Partial commutative monoid,Tensor product},
month = jul,
number = {7},
pages = {932--958},
title = {Coreflections in Algebraic Quantum Logic},
volume = {42},
year = {2012}
}
@incollection{Hensel1997,
abstract = {Abstract. Data types like trees which are fmitdy branching and of (possibly) infinite depth are described by iterating initial algebras and terminal coalgebras. We study proof principles for such data types in the context of categorical logic, following and extending the approach ...},
author = {Hensel, U. and Jacobs, Bart},
booktitle = {Categ. Theory Comput. Sci.},
doi = {10.1007/BFb0026991},
editor = {Moggi, Eugenio and Rosolini, Giuseppe},
isbn = {978-3-540-63455-3},
pages = {220--241},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Proof principles for datatypes with iterated recursion},
year = {1997}
}
@article{Higgins1990,
author = {Higgins, Peter M.},
doi = {10.1007/BF01189004},
issn = {00025240},
journal = {Algebr. Universalis},
number = {4},
pages = {597--599},
title = {An algebraic proof that pseudovarieties are defined by pseudoidentities},
volume = {27},
year = {1990}
}
@article{Dubois2007,
abstract = {Deciding whether one probability distribution is more informative (in the sense of representing a less indeterminate situation) than another one is typically done using well-established information measures such as, e.g., the Shannon entropy or other dispersion indices. In contrast, the relative specificity of possibility distributions is evaluated by means of fuzzy set inclusion. In this paper, we propose a technique for comparing probability distributions from the point of view of their relative dispersion without resorting to a numerical index. A natural partial ordering in terms of relative "peakedness" of probability functions is proposed which is closely related to order-1 stochastic dominance. There is also a close connection between this ordering on probability distributions and the standard specificity ordering on possibility distributions that can be derived by means of a known probability-possibility transformation. The paper proposes a direct proof showing that the (total) preordering on probability measures defined by probabilistic entropy refines the (partial) ordering defined by possibilistic specificity. This result, also valid for other dispersion indices, is discussed against the background of related work in statistics, mathematics (inequalities on convex functions), and the social sciences. Finally, an application of the possibilistic specificity ordering in the field of machine learning or, more specifically, the induction of decision forests is proposed. {\textcopyright} 2006 Elsevier Inc. All rights reserved.},
author = {Dubois, Didier and H{\"{u}}llermeier, Eyke},
doi = {10.1016/j.ijar.2006.06.017},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Decision forest,Dispersion,Entropy,Machine learning,Possibility distributions,Probability distributions,Probability-possibility transformation,Recursive partitioning,Specificity,Stochastic dominance},
month = jul,
number = {2},
pages = {364--385},
title = {Comparing probability measures using possibility theory: A notion of relative peakedness},
volume = {45},
year = {2007}
}
@inproceedings{Ghani2013a,
abstract = {Data types are undergoing a major leap forward in their sophistication driven by a conjunction of i) theoretical advances in the foundations of data types; and ii) requirements of programmers for ever more control of the data structures they work with. In this paper we develop a theory of indexed data types where, crucially, the indices are generated inductively at the same time as the data. In order to avoid commitment to any specific notion of indexing we take an axiomatic approach to such data types using fibrations - thus giving us a theory of what we call fibred data types. The genesis of these fibred data types can be traced within the literature, most notably to Dybjer and Setzer's introduction of the concept of induction-recursion. This paper, while drawing heavily on their seminal work for inspiration, gives a categorical reformulation of Dybjer and Setzer's original work which leads to a large number of extensions of induction-recursion. Concretely, the paper provides i) conceptual clarity as to what inductionrecursion fundamentally is about; ii) greater expressiveness in allowing not just the inductive-recursive definition of families of sets, or even indexed families of sets, but rather the inductiverecursive definition of a whole host of other structures; iii) a semantics for induction-recursion based not on the specific model of families, but rather an axiomatic model based upon fibrations which therefore encompasses diverse structures (domain theoretic, realisability, games etc) arising in the semantics of programming languages; and iv) technical justification as to why these fibred data types exist using large cardinals from set theory.},
author = {Ghani, Neil and Malatesta, Lorenzo and Forsberg, Fredrik Nordvall and Setzer, Anton},
booktitle = {Proc. - Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2013.30},
isbn = {978-1-4799-0413-6},
issn = {10436871},
keywords = {data types,fibrations,initial algebras},
pages = {243--252},
title = {Fibred data types},
year = {2013}
}
@incollection{Chen2016,
abstract = {The Sch{\"{u}}tzenberger product of monoids is a key tool for the algebraic treatment of language concatenation. In this paper we gener-alize the Sch{\"{u}}tzenberger product to the level of monoids in an algebraic category D, leading to a uniform view of the corresponding construc-tions for monoids (Sch{\"{u}}tzenberger), ordered monoids (Pin), idempotent semirings (Kl{\'{i}}ma and Pol{\'{a}}k), and algebras over a field (Reutenauer). In addition, assuming that D is part of a Stone-type duality, we derive a characterization of the languages recognized by Sch{\"{u}}tzenberger products.},
author = {Chen, Liang-Ting and Urbat, Henning},
booktitle = {Proc. 20th Int. Conf. Dev. Lang. Theory},
doi = {10.1007/978-3-662-53132-7},
editor = {Brlek, Sre{\v{c}}ko and Reutenauer, Christophe},
isbn = {978-3-662-53131-0},
pages = {89--101},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Sch{\"{u}}tzenberger products in a category},
volume = {9840},
year = {2016}
}
@article{Domingo-Ferrer2008,
abstract = {k-Anonymity is a privacy property requiring that all combinations of key attributes in a database be repeated at least for k records. It has been shown that k-anonymity alone does not always ensure privacy. A number of sophistications of k-anonymity have been proposed, like p-sensitive k-anonymity, l-diversity and t-closeness. This paper explores the shortcomings of those properties, none of which turns out to be completely convincing.},
author = {Domingo-Ferrer, Josep and Torra, Vicen{\c{c}}},
doi = {10.1109/ARES.2008.97},
isbn = {0769531024},
journal = {ARES 2008 - 3rd Int. Conf. Availability, Secur. Reliab. Proc.},
pages = {990--993},
title = {A critique of $k$-anonymity and some of its enhancements},
year = {2008}
}
@phdthesis{Kick2003,
author = {Kick, Marco},
school = {University of Edinburgh},
title = {Coalgebraic Modelling of Timed Processes},
year = {2003}
}
@article{Crary2007,
author = {Crary, Karl and Harper, Robert},
doi = {10.1016/j.entcs.2007.02.010},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {data abstraction,lambda calculus and related,logics of programs,operational semantics,polymorphism,systems,type structure},
month = apr,
pages = {259--299},
title = {Syntactic logical relations for polymorphic and recursive types},
volume = {172},
year = {2007}
}
@inproceedings{Adamek2012,
abstract = {Coalgebra offers a unified theory of state based systems, including infinite streams, labelled transition systems and deterministic automata. In this paper, we use the coalgebraic view on systems to derive, in a uniform way, abstract procedures for checking behavioural equivalence in coalgebras, which perform (a combination of) minimization and determinization. First, we show that for coalgebras in categories equipped with factorization structures , there exists an abstract procedure for equivalence checking. Then, we consider coalgebras in categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with reflections . This transformation can be thought of as some kind of determinization. We will apply our theory to the following examples: conditional transition systems and (non-deterministic) automata.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Bonchi, Filippo and H{\"{u}}lsbusch, Mathias and K{\"{o}}nig, Barbara and Milius, Stefan and Silva, Alexandra},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-28729-9_4},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {58--73},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A coalgebraic perspective on minimization and determinization},
type = {Conference proceedings (article)},
volume = {7213},
year = {2012}
}
@article{Goldblatt2006a,
author = {Goldblatt, Robert},
doi = {doi:%20DOI:%2010.1016/j.apal.2005.06.006},
issn = {0168-0072},
journal = {Ann. Pure Appl. Log.},
month = mar,
number = {1-3},
pages = {77--93},
title = {Final coalgebras and the Hennessy-Milner property},
type = {Journal article},
volume = {138},
year = {2006}
}
@inproceedings{Coull2013,
author = {Coull, Scott E. and Kenneally, Erin},
booktitle = {2013 IEEE Int. Conf. Technol. Homel. Secur.},
doi = {10.1109/THS.2013.6698982},
isbn = {978-1-4799-1535-4},
month = nov,
pages = {93--98},
publisher = {IEEE},
title = {Toward a comprehensive disclosure control framework for shared data},
year = {2013}
}
@incollection{Golle2009,
abstract = {Abstract. Many applications benefit from user location data, but lo- cation data raises privacy concerns. Anonymization can protect privacy, but identities can sometimes be inferred from supposedly anonymous data. This paper studies a new attack on the anonymity of location data. We show that if the approximate locations of an individual's home and workplace can both be deduced from a location trace, then the median size of the individual's anonymity set in the U.S. working population is 1, 21 and 34,980, for locations known at the granularity of a census block, census track and county respectively. The location data of people who live and work in different regions can be re-identified even more easily. Our results show that the threat of re-identification for location data is much greater when the individual's home and work locations can both be deduced from the data. To preserve anonymity, we offer guidance for obfuscating location traces before they are disclosed.},
author = {Golle, Philippe and Partridge, Kurt},
booktitle = {Pervasive Comput.},
doi = {10.1007/978-3-642-01516-8_26},
pages = {390--397},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On the Anonymity of Home/Work Location Pairs},
volume = {5538},
year = {2009}
}
@inproceedings{Goncharov2015,
abstract = {We study a model of side-effecting processes obtained by starting from a monad modelling base effects and adjoining free operations using a cofree coalgebra construction; one thus arrives at what one may think of as types of non-wellfounded side-effecting trees, generalizing the infinite resumption monad. Types of this kind have received some attention in the recent literature; in particular, it has been shown that they admit guarded iteration. Here, we show that they also admit unguarded iteration, i.e. form complete Elgot monads, provided that the underlying base effect supports unguarded iteration.},
author = {Goncharov, Sergey and Rauch, Christoph and Schr{\"{o}}der, Lutz},
booktitle = {Proc. 31st Conf. Math. Found. Program. Semant.},
doi = {10.1016/j.entcs.2015.12.012},
issn = {15710661},
keywords = {Recursion,coalgebra,coinduction,complete Elgot monad,resumptions},
pages = {183--198},
publisher = {Elsevier B.V.},
title = {Unguarded Recursion on Coinductive Resumptions},
volume = {319},
year = {2015}
}
@article{Sullivan2015,
abstract = {We aim to highlight certain points and considerations for graduate students and young researchers, which should be avoided in submissions to good research journals. Observing these remarks could substantially decrease the probability of rejections of papers.},
archivePrefix = {arXiv},
arxivId = {1504.03789},
author = {Sullivan, Gail M.},
doi = {10.4300/JGME-D-14-00686.1},
eprint = {1504.03789},
issn = {1949-8349},
journal = {J. Grad. Med. Educ.},
month = mar,
number = {1},
pages = {1--3},
pmid = {26217410},
title = {What to Do When Your Paper Is Rejected},
volume = {7},
year = {2015}
}
@inproceedings{Getoor1999,
abstract = {A large portion of real-world data is stored in commercial relational database systems. In contrast, most statistical learning methods work only with "flat" data representations. Thus, to apply these methods, we are forced to convert our data into a flat form, thereby losing much of the relational structure present in our database. This paper builds on the recent work on probabilistic relational models (PRMs), and describes how to learn them from databases. PRMs allow the properties of an...},
address = {Stockholm, Sweden},
author = {Friedman, N. and Getoor, L. and Koller, D. and Pfeffer, A.},
booktitle = {Proc. Sixt. Int. Jt. Conf. Artif. Intell.},
pages = {1300----1309},
publisher = {Morgan Kaufman},
title = {Learning Probabilistic Relational Models},
year = {1999}
}
@inproceedings{Straubing2002,
abstract = {There are many examples in the research literature of fami- lies of regular languages defined by purely model-theoretic means (that is, in terms of the kinds of formulas of predicate logic used to define them) that can be characterized algebraically (that is, in terms of the syntactic monoids or syntactic morphisms of the languages). In fact the existence of such algebraic characterizations appears to be the rule. The present paper gives an explanation of the phenomenon: A generalization of Eilenberg's variety theorem is proved, and then applied to logic. We find that a very wide assortment of families of regular languages de- fined in model-theoretic terms form varieties in this new sense,and that consequently membership in the family depends only on the syntactic morphism of the language.},
author = {Straubing, Howard},
booktitle = {Lat. 2002 Theor. Informatics},
doi = {10.1007/3-540-45995-2_46},
editor = {Rajsbaum, Sergio},
pages = {528--538},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On logical descriptions of regular languages},
year = {2002}
}
@article{Spivak2012,
abstract = {In this paper we present a simple database definition language: that of categories and functors. A database schema is a small category and an instance is a set-valued functor on it. We show that morphisms of schemas induce three data migration functors, which translate instances from one schema to the other in canonical ways. These functors parameterize projections, unions, and joins over all tables simultaneously and can be used in place of conjunctive and disjunctive queries. We also show how to connect a database and a functional programming language by introducing a functorial connection between the schema and the category of types for that language. We begin the paper with a multitude of examples to motivate the definitions, and near the end we provide a dictionary whereby one can translate database concepts into category-theoretic concepts and vice versa. {\textcopyright} 2012 Elsevier Inc. All rights reserved.},
archivePrefix = {arXiv},
arxivId = {1009.1166},
author = {Spivak, David I.},
doi = {10.1016/j.ic.2012.05.001},
eprint = {1009.1166},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Adjoint functors,Category theory,Data migration,Databases,Queries},
month = aug,
pages = {31--51},
publisher = {Elsevier Inc.},
title = {Functorial data migration},
volume = {217},
year = {2012}
}
@incollection{Dinesh2008,
abstract = {We consider the problem of checking whether the operations of an organization conform to a body of regulation. The immediate motivation comes from the analysis of the U.S. Food and Drug Administration regulations that apply to bloodbanks - organizations that collect, process, store, and use donations of blood and blood components. Statements in such regulations convey constraints on operations or sequences of operations that are performed by an organization. It is natural to express these constraints in a temporal logic. There are two important features of regulatory texts that need to be accommodated by a representation in logic. First, the constraints conveyed by regulation can be obligatory (required) or permitted (optional). Second, statements in regulation refer to others for conditions or exceptions. An organization conforms to a body of regulation if and only if it satisfies all the obligations. However, permissions provide exceptions to obligations, indirectly affecting conformance. In this paper, we extend linear temporal logic to distinguish between obligations and permissions, and to allow statements to refer to others. While the resulting logic allows for a direct representation of regulation, evaluating references between statements has high complexity. We discuss an empirically motivated assumption that lets us replace references with tests of lower complexity, leading to efficient trace-checking algorithms in practice.},
author = {Dinesh, Nikhil and Joshi, Aravind and Lee, Insup and Sokolsky, Oleg},
booktitle = {Runtime Verif. RV 2008},
doi = {10.1007/978-3-540-89247-2_6},
editor = {Leucker, Martin},
isbn = {354089246X},
issn = {03029743},
pages = {86--103},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Checking Traces for Regulatory Conformance},
volume = {5289},
year = {2008}
}
@article{Tt2000,
archivePrefix = {arXiv},
arxivId = {math/0004117},
author = {Joyal, Andr{\'{e}} and Street, Ross},
doi = {10.1016/0001-8708(91)90003-P},
eprint = {0004117},
isbn = {9780521849425},
issn = {00018708},
journal = {Adv. Math. (N. Y).},
month = jul,
number = {1},
pages = {55--112},
primaryClass = {math},
title = {The geometry of tensor calculus, I},
volume = {88},
year = {1991}
}
@article{Dwork2014,
abstract = {The Algorithmic Foundations of Differential Privacy},
author = {Dwork, Cynthia and Roth, Aaron},
doi = {10.1561/0400000042},
isbn = {9781601988188},
issn = {1551-305X},
journal = {Found. Trends{\textregistered} Theor. Comput. Sci.},
number = {3-4},
pages = {211--407},
title = {The Algorithmic Foundations of Differential Privacy},
volume = {9},
year = {2014}
}
@article{Venema2012,
abstract = {This paper introduces an endofunctor $\VT$ on the category of frames, parametrized by an endofunctor $\T$ on the category $\Set$ that satisfies certain constraints. This generalizes Johnstone's construction of the Vietoris powerlocale, in the sense that his construction is obtained by taking for $\T$ the finite covariant power set functor. Our construction of the $\T$-powerlocale $\VT \bbL$ out of a frame $\bbL$ is based on ideas from coalgebraic logic and makes explicit the connection between the Vietoris construction and Moss's coalgebraic cover modality. We show how to extend certain natural transformations between set functors to natural transformations between $\T$-powerlocale functors. Finally, we prove that the operation $\VT$ preserves some properties of frames, such as regularity, zero-dimensionality, and the combination of zero-dimensionality and compactness.},
archivePrefix = {arXiv},
arxivId = {1202.3264},
author = {Venema, Yde and Vickers, Steven and Vosmaer, Jacob},
doi = {10.1017/S0960129512000229},
eprint = {1202.3264},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
keywords = {coalgebra,cover modality,frames,locales,modal logic,vietoris construction},
month = aug,
number = {01},
pages = {142--199},
title = {Generalised powerlocales via relation lifting},
volume = {23},
year = {2012}
}
@article{Doberkat2009,
abstract = {We generalize stochastic Kripke models and Markov transition systems to stochastic right coalgebras. These are coalgebras for a functor F⋅S with F as an endofunctor on the category of analytic spaces, and S is the subprobability functor. The modal operators are generalized through predicate liftings which are set-valued natural transformations involving the functor. Two states are equivalent iff they cannot be separated by a formula. This equivalence relation is used to construct a cospan for logical equivalent coalgebras under a separation condition for the set of predicate liftings. Consequently, behavioral and logical equivalence are really the same. From the cospan we construct a span. The central argument is a selection argument giving us the dynamics of a mediating coalgebra from the domains of the cospan. This construction is used to establish that behavioral equivalent coalgebras are bisimilar, yielding the equivalence of all three characterizations of a coalgebra's behavior as in the case of Kripke models or Markov transition systems.},
author = {Doberkat, Ernst-Erich and Schubert, Christoph},
doi = {10.1016/j.apal.2008.06.018},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
month = jun,
number = {3},
pages = {268--284},
title = {Coalgebraic logic for stochastic right coalgebras},
volume = {159},
year = {2009}
}
@article{Eklund2013,
abstract = {In this paper we will show how purely categorical constructions of terms are advantageous when investigating situations concerning uncertainty; more specifically where uncertainty comes from and how uncertainty is integrated when dealing with terms over selected signatures. There are basically two ways of invoking uncertainty for terms. On one hand, we may proceed by building composed monads where uncertainty is provided by some suitable monad composed with the traditional term monad. On the other hand, we can provide a strictly formal basis for term monads being created over categories themselves carrying uncertainty. This is the distinction between 'computing with fuzzy' and 'fuzzy computing' and the fundamental question raised by these constructions is where uncertainty resides in language constructions for logic. This paper also shows how the notion of signature often needs to be expanded to levels of signatures, in particular when dealing with type constructors. Such levels allow us to strictly delineate, e.g., primitive operations, type terms, and value level terms. Levels of signature will in this paper be exemplified by the construction of the signature of simply typed lambda calculus. {\textcopyright} 2013 Elsevier B.V. All rights reserved.},
author = {Eklund, Patrik and Gal{\'{a}}n, M. {\'{A}}ngeles and Helgesson, Robert and Kortelainen, Jari},
doi = {10.1016/j.fss.2013.02.012},
issn = {01650114},
journal = {Fuzzy Sets Syst.},
keywords = {Algebra,Category theory,Quantale,Term monads},
pages = {211--235},
publisher = {Elsevier},
title = {Fuzzy terms},
volume = {256},
year = {2013}
}
@article{Rothe2003,
author = {Rothe, Jan and Ma{\v{s}}ulovi{\'{c}}, Dragan},
doi = {10.1016/S1571-0661(04)80646-7},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jul,
number = {1},
pages = {303--320},
title = {Modal Logics for Observation Equivalences},
volume = {82},
year = {2003}
}
@article{Kelly1989,
author = {Kelly, Gregory Maxwell},
doi = {10.1017/S0004972700002781},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = apr,
number = {02},
pages = {301--317},
title = {Elementary observations on 2-categorical limits},
volume = {39},
year = {1989}
}
@article{Bonneau2015,
abstract = {Bitcoin has emerged as the most successful cryptographic currency in history. Within two years of its quiet launch in 2009, Bitcoin grew to comprise billions of dollars

repository: anqurvanillapy/Type-Theory

repo_name: anqurvanillapy/Type-Theory