text:
volume = {2566},
year = {2002}
}
@article{Power1995,
author = {Power, A. John},
doi = {10.1006/inco.1995.1112},
issn = {08905401},
journal = {Inf. Comput.},
month = aug,
number = {2},
pages = {251--262},
title = {Why Tricategories?},
volume = {120},
year = {1995}
}
@article{Selinger2011,
abstract = {This article is intended as a reference guide to various notions of monoidal categories and their associated string diagrams. It is hoped that this will be useful not just to mathematicians, but also to physicists, computer scientists, and others who use diagrammatic reasoning. We have opted for a somewhat informal treatment of topological notions, and have omitted most proofs. Nevertheless, the exposition is sufficiently detailed to make it clear what is presently known, and to serve as a starting place for more in-depth study. Where possible, we provide pointers to more rigorous treatments in the literature. Where we include results that have only been proved in special cases, we indicate this in the form of caveats.},
archivePrefix = {arXiv},
arxivId = {0908.3347},
author = {Selinger, P.},
doi = {10.1007/978-3-642-12821-9_4},
eprint = {0908.3347},
isbn = {9783642128202},
issn = {00758450},
journal = {Lect. Notes Phys.},
pages = {289--355},
title = {A survey of graphical languages for monoidal categories},
volume = {813},
year = {2011}
}
@article{Adamek1996,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
doi = {10.1006/jabr.1996.0345},
issn = {00218693},
journal = {J. Algebr.},
month = nov,
number = {3},
pages = {643--659},
title = {How to Sketch Quasivarieties},
volume = {185},
year = {1996}
}
@inproceedings{Adamek2015,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Myers, Robert Samuel Ralph and Urbat, Henning and Milius, Stefan},
booktitle = {30th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2015.46},
isbn = {978-1-4799-8875-4},
month = jul,
pages = {414--425},
publisher = {IEEE},
title = {Varieties of Languages in a Category},
year = {2015}
}
@article{Cirstea2007,
abstract = {We present a modular approach to defining logics for a wide variety of state-based systems. The systems are modelled as coalgebras, and we use modal logics to specify their observable properties. We show that the syntax, semantics and proof systems associated with such logics can all be derived in a modular fashion. Moreover, we show that the logics thus obtained inherit soundness, completeness and expressiveness properties from their building blocks. We apply these techniques to derive sound, complete and expressive logics for a wide variety of probabilistic systems, for which no complete axiomatisation has been obtained so far.},
author = {C{\^{i}}rstea, Corina and Pattinson, Dirk},
doi = {10.1016/j.tcs.2007.06.002},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebra,completeness,modal logic,probabilistic systems},
month = dec,
number = {1-3},
pages = {83--108},
title = {Modular construction of complete coalgebraic logics},
volume = {388},
year = {2007}
}
@article{Wisbauer2007,
author = {Wisbauer, Robert},
doi = {10.1007/s10485-007-9076-5},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
keywords = {16w30,18a40,18c15,18c20,2000,algebras,categories,coalgebras,hopf algebras,mathematics subject classifications},
month = may,
number = {1-2},
pages = {255--295},
title = {Algebras Versus Coalgebras},
volume = {16},
year = {2007}
}
@book{Power1998a,
abstract = {These notes constitute lecture notes to accompany a course on 2-categories at BRICS in the Computer Science Department of the University of Aarhus in March 1998. Each section corresponds to one lecture.},
author = {Power, A. John},
issn = {0909-3206},
month = aug,
number = {August},
series = {BRICS Notes Series},
title = {2-Categories},
year = {1998}
}
@article{Tholen2016a,
abstract = {For a quantaloid $\mathcal{Q}$, considered as a bicategory, Walters introduced categories enriched in $\mathcal{Q}$. Here we extend the study of monad-quantale-enriched categories of the past fifteen years by introducing monad-quantaloid-enriched categories. We do so by making lax distributive laws of a monad $\mathbb{T}$ over the discrete presheaf monad of the small quantaloid $\mathcal{Q}$ the primary data of the theory, rather than the lax monad extensions of $\mathbb{T}$ to the category of $\mathcal{Q}$-relations that they equivalently describe. The central piece of the paper establishes a Galois correspondence between such lax distributive laws and lax Eilenberg-Moore $\mathbb{T}$-algebra structures on the set of discrete presheaves over the object set of $\mathcal{Q}$. We give a precise comparison of these structures with the more restrictive notion introduced by Hofmann in the case of a commutative quantale, called natural topological theories here, and describe the lax monad extensions introduced by him as minimal. Throughout the paper, a variety of old and new examples of ordered, metric and topological structures illustrate the theory developed, which includes the consideration of algebraic functors and change-of-base functors in full generality.},
archivePrefix = {arXiv},
arxivId = {1603.06251},
author = {Tholen, Walter},
eprint = {1603.06251},
journal = {ArXiv e-prints},
keywords = {18 c15,18c20,18d99,2010 msc,algebraic functor,change-of-base functor,discrete presheaf monad,lax,lax distributive law,lax monad extension,monad,monad-quantaloid-enriched category,natural,quantale,quantaloid,topological theory,$\lambda$ -algebra},
month = mar,
pages = {1--32},
title = {Lax Distributive Laws for Topology, I},
year = {2016}
}
@article{Birkedal2010,
abstract = {It is well known that one can use an adaptation of the inverse-limit construction to solve recursive equations in the category of complete ultrametric spaces. We show that this construction generalizes to a large class of categories with metric-space structure on each set of morphisms: the exact nature of the objects is less important. In particular, the construction immediately applies to categories where the objects are ultrametric spaces with 'extra structure', and where the morphisms preserve this extra structure. The generalization is inspired by classical domain-theoretic work by Smyth and Plotkin. For many of the categories we consider, there is a natural subcategory in which each set of morphisms is required to be a compact metric space. Our setting allows for a proof that such a subcategory always inherits solutions of recursive equations from the full category. As another application, we present a construction that relates solutions of generalized domain equations in the sense of Smyth and Plotkin to solutions of equations in our class of categories. Our primary motivation for solving generalized recursive metric-space equations comes from recent and ongoing work on Kripke-style models in which the sets of worlds must be recursively defined. We show a series of examples motivated by this line of work. {\textcopyright} 2010 Elsevier B.V. All rights reserved.},
author = {Birkedal, Lars and St{\o}vring, Kristian and Thamsborg, Jacob},
doi = {10.1016/j.tcs.2010.07.010},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Fixed point,Metric space,Recursive equation},
number = {47},
pages = {4102--4122},
publisher = {Elsevier B.V.},
title = {The category-theoretic solution of recursive metric-space equations},
volume = {411},
year = {2010}
}
@article{Grandis2004,
author = {Grandis, Marco and Par{\'{e}}, Robert},
journal = {Cah. Topol. g{\'{e}}om{\'{e}}trie diff{\'{e}}rentielle cat{\'{e}}goriques},
number = {3},
pages = {193--240},
title = {Adjoint for double categories},
volume = {45},
year = {2004}
}
@article{Veldman1976,
author = {Veldman, Wim},
doi = {10.2307/2272955},
issn = {00224812},
journal = {J. Symb. Log.},
month = mar,
number = {1},
pages = {159},
title = {An Intuitionistic Completeness Theorem for Intuitionistic Predicate Logic},
volume = {41},
year = {1976}
}
@article{Abadi2002,
author = {Abadi, Martı́n and Fournet, C{\'{e}}dric and Gonthier, Georges},
doi = {10.1006/inco.2002.3086},
issn = {08905401},
journal = {Inf. Comput.},
month = apr,
number = {1},
pages = {37--83},
title = {Secure Implementation of Channel Abstractions},
volume = {174},
year = {2002}
}
@inproceedings{Lindley2016,
address = {New York, New York, USA},
author = {Lindley, Sam and Morris, J Garrett},
booktitle = {Proc. 9th Int. Symp. Haskell - Haskell 2016},
doi = {10.1145/2976002.2976018},
isbn = {9781450344340},
keywords = {embedded languages,linear types,session types},
pages = {133--145},
publisher = {ACM Press},
title = {Embedding session types in Haskell},
year = {2016}
}
@inproceedings{Scibior2015,
abstract = {The machine learning community has recently shown a lot of inter-est in practical probabilistic programming systems that target the problem of Bayesian inference. Such systems come in different forms, but they all express probabilistic models as computational processes using syntax resembling programming languages. In the functional programming community monads are known to offer a convenient and elegant abstraction for programming with probabil-ity distributions, but their use is often limited to very simple in-ference problems. We show that it is possible to use the monad abstraction to construct probabilistic models for machine learning, while still offering good performance of inference in challenging models. We use a GADT as an underlying representation of a prob-ability distribution and apply Sequential Monte Carlo-based meth-ods to achieve efficient inference. We define a formal semantics via measure theory. We demonstrate a clean and elegant implementa-tion that achieves performance comparable with Anglican, a state-of-the-art probabilistic programming system.},
address = {New York, New York, USA},
author = {{\'{S}}cibior, Adam and Ghahramani, Zoubin and Gordon, Andrew D.},
booktitle = {Proc. 8th ACM SIGPLAN Symp. Haskell - Haskell 2015},
doi = {10.1145/2804302.2804317},
isbn = {9781450338080},
issn = {03621340},
keywords = {and z is a,bayesian statis-,given particular values of,haskell,monads,monte carlo,normalising con-,parameters,posterior is a proper,probabilistic programming,probability distribution,stant that ensures the,tics},
pages = {165--176},
publisher = {ACM Press},
title = {Practical probabilistic programming with monads},
year = {2015}
}
@article{Beeri1984,
abstract = {Given a universal relation scheme, presented as a set of attributes and a set of dependencies, it may be advantageous to decompose it into a collection of schemes, each with its own sets of attributes and dependencies, that has some desired properties. A basic requirement for such a decomposition to be useful is that the corresponding decomposition map on universal relations be injective. A central problem in database theory is to find the reconstruction map, i.e., the inverse map of an injective decomposition map. It is proved here that when the decomposition, viewed as a hypergraph, is acyclic and the given dependencies are full implicational dependencies, then the reconstruction map is the natural join. Based on this, it is shown that there is a polynomial time algorithm to test for injectiveness of decompositions. {\textcopyright} 1984 Academic Press, Inc. All rights reserved.},
author = {Beeri, Catriel and Vardi, Moshe Y.},
doi = {10.1016/S0019-9958(84)80051-0},
issn = {00199958},
journal = {Inf. Control},
month = may,
number = {2},
pages = {75--84},
title = {On acyclic database decompositions},
volume = {61},
year = {1984}
}
@article{Adamek2006,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan},
doi = {10.1016/j.ic.2005.11.005},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {basic equation,iterative theory,rational tree,terminal coalgebra},
month = jul,
number = {7},
pages = {1139--1172},
title = {Terminal coalgebras and free iterative theories},
volume = {204},
year = {2006}
}
@article{Baez2011,
abstract = {There are numerous characterizations of Shannon entropy and Tsallis entropy as measures of information obeying certain properties. Using work by Faddeev and Furuichi, we derive a very simple characterization. Instead of focusing on the entropy of a probability measure on a finite set, this characterization focuses on the `information loss', or change in entropy, associated with a measure-preserving function. Information loss is a special case of conditional entropy: namely, it is the entropy of a random variable conditioned on some function of that variable. We show that Shannon entropy gives the only concept of information loss that is functorial, convex-linear and continuous. This characterization naturally generalizes to Tsallis entropy as well.},
archivePrefix = {arXiv},
arxivId = {1106.1791},
author = {Baez, John C. and Fritz, Tobias and Leinster, Tom},
doi = {10.3390/e13111945},
eprint = {1106.1791},
issn = {1099-4300},
journal = {Entropy},
keywords = {Information theory,Measure-preserving function,Shannon entropy,Tsallis entropy},
month = nov,
number = {12},
pages = {1945--1957},
title = {A Characterization of Entropy in Terms of Information Loss},
volume = {13},
year = {2011}
}
@article{Harding2013,
abstract = {We define a 2-category whose objects are fuzzy sets and whose maps are relations subject to certain natural conditions. We enrich this category with additional monoidal and involutive structure coming from t-norms and negations on the unit interval. We develop the basic properties of this category and consider its relation to other familiar categories. A discussion is made of extending these results to the setting of type-2 fuzzy sets. ?? 2013 Elsevier B.V. All rights reserved.},
author = {Harding, John and Walker, Carol and Walker, Elbert},
doi = {10.1016/j.fss.2013.04.004},
issn = {01650114},
journal = {Fuzzy Sets Syst.},
keywords = {2-Category,Biproducts,Category with involution,Fuzzy sets,Relations as morphisms,Symmetric monoidal tensor},
pages = {149--165},
publisher = {Elsevier},
title = {Categories with fuzzy sets and relations},
volume = {256},
year = {2013}
}
@article{Cignoli2004,
abstract = {Stone duality between boolean algebras and inverse limits of finite sets is extended to a duality between locally finite MV-algebras and a category of multisets naturally arising as inverse limits of finite multisets.},
author = {Cignoli, Roberto and Dubuc, Eduardo J. and Mundici, Daniele},
doi = {10.1016/j.jpaa.2003.10.021},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = may,
number = {1-3},
pages = {37--59},
title = {Extending Stone duality to multisets and locally finite MV-algebras},
volume = {189},
year = {2004}
}
@article{Tholen1987,
abstract = {For an abstract categoryC, several sufficient conditions for the intersection of two or of a larger collection of full reflective subcategories ofCto be reflective are presented. The given criteria are applicable particularly whenCis a concrete topological category.},
author = {Tholen, Walter},
doi = {10.1016/0166-8641(87)90105-2},
issn = {01668641},
journal = {Topol. Appl.},
month = nov,
number = {2},
pages = {201--212},
title = {Reflective subcategories},
volume = {27},
year = {1987}
}
@book{Johnstone2002a,
author = {Johnstone, Peter T.},
isbn = {978-0-19-851598-2},
pages = {716},
publisher = {Oxford University Press},
title = {Sketches of an Elephant: A Topos Theory Compendium},
volume = {2},
year = {2002}
}
@inproceedings{Calin2009,
author = {Calin, Georgel and Myers, Rob and Pattinson, Dirk and Schr{\"{o}}der, Lutz},
booktitle = {Proc. 5th Work. Methods Modalities (M4M5 2007)},
doi = {10.1016/j.entcs.2009.02.028},
issn = {15710661},
keywords = {automatic proving,coalgebra,modal logic},
pages = {41--54},
series = {ENTCS},
title = {CoLoSS: The Coalgebraic Logic Satisfiability Solver},
volume = {231},
year = {2009}
}
@article{Cirstea2009a,
author = {C{\^{i}}rstea, Corina and Kurz, Alexander and Pattinson, Dirk and Schr{\"{o}}der, Lutz and Venema, Yde},
doi = {10.1093/comjnl/bxp004},
issn = {0010-4620},
journal = {Comput. J.},
keywords = {coalgebra,compositionality,concurrency,knowledge representation,modal logic},
month = feb,
number = {1},
pages = {31--41},
title = {Modal Logics are Coalgebraic},
volume = {54},
year = {2009}
}
@incollection{Bun2016,
abstract = {“Concentrated differential privacy” was recently introduced by Dwork and Rothblum as a relaxation of differential privacy, which permits sharper analyses of many privacy-preserving computations. We present an alternative formulation of the concept of concentrated differential privacy in terms of the R{\'{e}}nyi divergence between the distributions obtained by running an algorithm on neighboring inputs. With this reformulation in hand, we prove sharper quantitative results, establish lower bounds, and raise a few new questions. We also unify this approach with approximate differential privacy by giving an appropriate definition of “approximate concentrated differential privacy”.},
author = {Bun, Mark and Steinke, Thomas},
booktitle = {Theory Cryptogr. TCC 2016},
doi = {10.1007/978-3-662-53641-4_24},
editor = {Hirt, Martin and Smith, Adam},
pages = {635--658},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds},
volume = {9985},
year = {2016}
}
@article{Pavlovic2014a,
abstract = {In Monoidal Computer I, we introduced a categorical model of computation where the formal reasoning about computability was supported by the simple and popular diagrammatic language of string diagrams. In the present paper, we refine and extend that model of computation to support a formal complexity theory as well. This formalization brings to the foreground the concept of normal complexity measures, which allow decompositions akin to Kleene's normal form. Such measures turn out to be just those where evaluating the complexity of a program does not require substantially more resources than evaluating the program itself. The usual time and space complexity are thus normal measures, whereas the average and the randomized complexity measures are not. While the measures that are not normal provide important design time information about algorithms, and for theoretical analyses, normal measures can also be used at run time, as practical tools of computation, e.g. to set the bounds for hypothesis testing, inductive inference and algorithmic learning.},
archivePrefix = {arXiv},
arxivId = {1402.5687},
author = {Pavlovi{\'{c}}, Dusko},
eprint = {1402.5687},
journal = {ArXiv e-prints},
title = {Monoidal computer II: Normal complexity by string diagrams},
year = {2014}
}
@article{Ponse2007,
abstract = {We study two alternative bases for Belnap's four-valued logic and provide complete equational axiomatizations for them. One is called conditional composition logic. It has a single, ternary if-then-else connective with a sequential, operational reading, and four constants for the truth values. The other logic is called guard logic. The main motivation for this logic lies in its technical properties. It admits a useful type of canonical form (term representation), and a relatively simple strategy for equational reasoning. ?? 2007 Elsevier Ltd. All rights reserved.},
author = {Ponse, Alban and van der Zwaag, Mark B.},
doi = {10.1016/j.tcs.2007.09.027},
isbn = {0304-3975},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Belnap's logic,Completeness,Conditional composition,Equational axiomatizations,Guard logic},
month = dec,
number = {1-3},
pages = {319--336},
title = {Belnap's logic and conditional composition},
volume = {388},
year = {2007}
}
@incollection{Kurz2015,
author = {Kurz, Alexander and Milius, Stefan and Pattinson, Dirk and Schr{\"{o}}der, Lutz},
booktitle = {Software, Serv. Syst.},
doi = {10.1007/978-3-319-15545-6},
editor = {{De Nicola}, Rocco and Hennicker, Rolf},
isbn = {978-3-319-15544-9},
pages = {75--90},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
title = {Simplified coalgebraic trace equivalence},
year = {2015}
}
@article{Narayanan2010,
author = {Narayanan, Arvind and Shmatikov, Vitaly},
doi = {10.1145/1743546.1743558},
isbn = {0001-0782},
issn = {00010782},
journal = {Commun. ACM},
number = {6},
pages = {24},
title = {Myths and fallacies of "personally identifiable information"},
volume = {53},
year = {2010}
}
@article{Street1987,
author = {Street, Ross},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {1},
pages = {53--56},
title = {Correction to “Fibrations in bicategories”},
volume = {28},
year = {1987}
}
@article{Pouillard2010,
author = {Pouillard, Nicolas and Pottier, Fran{\c{c}}ois},
doi = {10.1145/1932681.1863575},
isbn = {9781605587943},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {3,binders,cannot be mixed,equivalent,higher-order abstract syntax,in increasing,meta-programming,name abstraction,names,names with different scopes,these slogans are not,we have listed them},
month = sep,
number = {9},
pages = {217},
title = {A fresh look at programming with names and binders},
volume = {45},
year = {2010}
}
@phdthesis{Leal2011,
author = {Leal, Raul Andres},
isbn = {9789057762314},
school = {University of Amsterdan},
title = {Modalities Through the Looking Glass: A study on coalgebraic modal logic and their applications},
year = {2011}
}
@article{Reiter1980,
abstract = {The need to make default assumptions is frequently encountered in reasoning about incompletely specified worlds. Inferences sanctioned by default are best viewed as beliefs which may well be modified or rejected by subsequent observations. It is this property which leads to the non-monotonicity of any logic of defaults. In this paper we propose a logic for default reasoning. We then specialize our treatment to a very large class of commonly occuring defaults. For this class we develop a complete proof theory and show how to interface it with a top down resolution theorem prover. Finally, we provide criteria under which the revision of derived beliefs must be effected. {\textcopyright} 1980.},
author = {Reiter, R.},
doi = {10.1016/0004-3702(80)90014-4},
isbn = {0004-3702},
issn = {00043702},
journal = {Artif. Intell.},
month = apr,
number = {1-2},
pages = {81--132},
title = {A logic for default reasoning},
volume = {13},
year = {1980}
}
@article{Schubert2008,
author = {Schubert, Christoph and Seal, Gavin J.},
journal = {Theory Appl. Categ.},
keywords = {and phrases,initial extension,kleisli extension,lax algebra,strata extension,tower},
number = {7},
pages = {118--151},
title = {Extensions in the theory of lax algebras},
volume = {21},
year = {2008}
}
@article{Barr1990,
author = {Barr, Michael},
journal = {J. Pure Appl. Algebr.},
pages = {219--232},
title = {Accessible categories and models of linear logic},
volume = {69},
year = {1990}
}
@article{Tzevelekos2012,
author = {Tzevelekos, Nikos},
doi = {10.1016/j.cl.2012.02.002},
issn = {14778424},
journal = {Comput. Lang. Syst. Struct.},
keywords = {Environmental bisimulations,Game semantics,Higher-order computation and local state,Logical relations,Nominal computation,Program equivalence},
month = jul,
number = {2},
pages = {181--198},
publisher = {Elsevier},
title = {Program equivalence in a simple language with state},
volume = {38},
year = {2012}
}
@incollection{Klin2005,
author = {Klin, Bartek},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/11548133_16},
pages = {247--262},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {The least fibred lifting and the expressivity of coalgebraic modal logic},
year = {2005}
}
@inproceedings{Delaware2013a,
address = {New York, New York, USA},
author = {Delaware, Benjamin and {d. S. Oliveira}, Bruno C. and Schrijvers, Tom},
booktitle = {Proc. 40th Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '13},
doi = {10.1145/2429069.2429094},
isbn = {9781450318327},
keywords = {extensible church,modular mechanized meta-theory},
pages = {207},
publisher = {ACM Press},
title = {Meta-theory {\`{a}} la carte},
year = {2013}
}
@article{Kupke2012,
abstract = {We study the finitary version of the coalgebraic logic introduced by L.$\sim$Moss. The syntax of this logic, which is introduced uniformly with respect to a coalgebraic type functor, required to preserve weak pullbacks, extends that of classical propositional logic with a so-called coalgebraic cover modality depending on the type functor. Its semantics is defined in terms of a categorically defined relation lifting operation. As the main contributions of our paper we introduce a derivation system, and prove that it provides a sound and complete axiomatization for the collection of coalgebraically valid inequalities. Our soundness and completeness proof is algebraic, and we employ Pattinson's stratification method, showing that our derivation system can be stratified in countably many layers, corresponding to the modal depth of the formulas involved. In the proof of our main result we identify some new concepts and obtain some auxiliary results of independent interest. We survey properties of the notion of relation lifting, induced by an arbitrary but fixed set functor. We introduce a category of Boolean algebra presentations, and establish an adjunction between it and the category of Boolean algebras. Given the fact that our derivation system involves only formulas of depth one, it can be encoded as a endo-functor on Boolean algebras. We show that this functor is finitary and preserves embeddings, and we prove that the Lindenbaum-Tarski algebra of our logic can be identified with the initial algebra for this functor.},
author = {Kupke, Clemens and Kurz, Alexander and Venema, Yde},
doi = {10.2168/LMCS-8(3:2)2012},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,coalgebra,completeness,cover modality,modal logic,presenta-,relation lifting,relations,tions by generators and},
pages = {1--76},
title = {Completeness for the coalgebraic cover modality},
volume = {8},
year = {2012}
}
@article{Grandis1999,
author = {Grandis, Marco and Par{\'{e}}, Robert},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {3},
pages = {162--220},
title = {Limits in double categories},
volume = {40},
year = {1999}
}
@incollection{Focardi2001,
abstract = {In the recent years, many formalizations of security properties have been proposed, most of which are based on different underlying models and are consequently difficult to compare. A classification of security properties is thus of interest for understanding the relationships among different definitions and for evaluating the relative merits. In this paper, many non-interference-like properties proposed for computer security are classified and compared in a unifying framework. The resulting taxonomy is evaluated through some case studies of access control in computer systems. The approach has been mechanized, resulting in the tool CoSeC. Various extensions (e.g., the application to cryptographic protocol analysis) and open problems are discussed.},
author = {Focardi, Riccardo and Gorrieri, Roberto},
booktitle = {Found. Secur. Anal. Des. FOSAD 2000},
doi = {10.1007/3-540-45608-2_6},
editor = {Focardi, Riccardo and Gorrieri, Roberto},
isbn = {3540428968},
issn = {0302-9743},
pages = {331--396},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Classification of security properties (Part I: information flow)},
volume = {2171},
year = {2001}
}
@book{Johnstone1978a,
address = {Berlin, Heidelberg},
author = {Johnstone, Peter T. and Par{\'{e}}, Robert and Rosebrugh, R. D. and Schumacher, D. and Wood, R. J. and Wraith, G. C.},
doi = {10.1007/BFb0061360},
isbn = {978-3-540-08914-8},
issn = {0075-8434},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Indexed Categories and Their Applications},
volume = {661},
year = {1978}
}
@article{Terrovitis2008,
abstract = {In this paper we study the problem of protecting privacy in the publication of set-valued data. Consider a collection of transactional data that contains detailed information about items bought together by individuals. Even after removing all personal characteristics of the buyer, which can serve as links to his identity, the publication of such data is still subject to privacy attacks from adversaries who have partial knowledge about the set. Unlike most previous works, we do not distinguish data as sensitive and non-sensitive, but we consider them both as potential quasi-identifiers and potential sensitive data, depending on the point of view of the adversary. We define a new version of the k-anonymity guarantee, the k m-anonymity, to limit the effects of the data dimensionality and we propose efficient algorithms to transform the database. Our anonymization model relies on generalization instead of suppression, which is the most common practice in related works on such data. We develop an algorithm which finds the optimal solution, however, at a high cost which makes it inapplicable for large, realistic problems. Then, we propose two greedy heuristics, which scale much better and in most of the cases find a solution close to the optimal. The proposed algorithms are experimentally evaluated using real datasets.},
author = {Terrovitis, Manolis and Mamoulis, Nikos and Kalnis, Panos},
doi = {10.14778/1453856.1453874},
isbn = {0000000000000},
issn = {21508097},
journal = {Proc. VLDB Endow.},
month = aug,
number = {1},
pages = {115--125},
title = {Privacy-preserving anonymization of set-valued data},
volume = {1},
year = {2008}
}
@inproceedings{Hinze2012,
abstract = {Many program optimisations involve transforming a program in direct style to an equivalent program in continuation-passing style. This paper investigates the theoretical underpinnings of this transformation in the categorical setting of monads. We argue that so-called absolute Kan Extensions underlie this program optimisation. It is known that every Kan extension gives rise to a monad, the codensity monad, and furthermore that every monad is isomorphic to a codensity monad. The end formula for Kan extensions then induces an implementation of the monad, which can be seen as the categorical counterpart of continuationpassing style. We show that several optimisations are instances of this scheme: Church representations and implementation of backtracking using success and failure continuations, among others. Furthermore, we develop the calculational properties of Kan extensions, powers and ends. In particular, we propose a two-dimensional notation based on string diagrams that aims to support e ective reasoning with Kan extensions.},
author = {Hinze, Ralf},
booktitle = {Proc. 11th Int. Conf. Math. Progr. Constr.},
doi = {10.1007/978-3-642-31113-0_16},
isbn = {978-3-642-31112-3},
issn = {0302-9743},
keywords = {adjunction,backtracking,church representation,codensity monad,cps,end,haskell,kan extension,power,string diagram},
pages = {324--362},
publisher = {Springer-Verlag},
title = {Kan extensions for program optimisation or: art and dan explain an old trick},
year = {2012}
}
@article{Jones1996,
abstract = {The last decade has seen two methodological advances of particular direct import for the theory of finite monoids and indirect import for that of rational languages. The first has been the use of categories (considered as "algebras over graphs") as a framework in which to study monoids and their homomorphisms, the second has been the use of implicit operations to study pseudovarieties of monoids. Still more recent work has emphasized the role of profiniteness in finite monoid theory. This paper fuses these three topics by means of a general study of profinite categories, with applications to C-varieties (pseudovarieties of categories) in general, to those C-varieties arising from M-varieties (pseudovarieties of monoids) in particular, to implicit operations on categories and to recognizable languages over graphs.},
author = {Jones, Peter R.},
doi = {10.1016/0022-4049(95)00074-7},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {1},
pages = {61--95},
title = {Profinite categories, implicit operations and pseudovarieties of categories},
volume = {109},
year = {1996}
}
@inproceedings{Barthe2016,
abstract = {The aim of this paper is to provide a new method for learning the relationships between data that have been obtained independently. Unlike existing methods like matching, the proposed technique does not require any contextual information, provided that the dependency between the variables of interest is monotone. It can therefore be easily combined with matching in order to exploit the advantages of both methods. This technique can be described as a mix between quantile matching, and deconvolution. We provide for it a theoretical and an empirical validation.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {1601.0504},
author = {Barthe, Gilles and Gaboardi, Marco and Gr{\'{e}}goire, Benjamin and Hsu, Justin and Strub, Pierre-Yves},
booktitle = {Proc. 31st Annu. ACM/IEEE Symp. Log. Comput. Sci. - LICS '16},
doi = {10.1145/2933575.2934554},
eprint = {1601.0504},
isbn = {9781450343916},
issn = {10436871},
number = {212},
pages = {749--758},
publisher = {ACM Press},
title = {Proving differential privacy via probabilistic couplings},
volume = {1},
year = {2016}
}
@incollection{Kopotek1998,
abstract = {{\textcopyright} Springer-Verlag Berlin Heidelberg 1998. The paper presents a novel view of the Dempster-Shafer belief function as a measure of diversity in relational data bases. The Dempster rule of evidence combination corresponds to the join operator of the relational database theory. This rough-set based interpretation is qualitative in nature and can represent a number of belief function operators.},
author = {K{\l}opotek, Mieczys{\l}aw A. and Wierzcho{\'{n}}, S{\l}awomir T.},
booktitle = {Rough Sets Curr. Trends Comput.},
doi = {10.1007/3-540-69115-4_47},
editor = {Polkowski, Lech and Skowron, Andrzej},
pages = {346--354},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A New Qualitative Rough-Set Approach to Modeling Belief Functions},
volume = {1424},
year = {1998}
}
@article{Jakl2016,
author = {Jakl, Tom{\'{a}}{\v{s}} and Jung, Achim and Pultr, Ale{\v{s}}},
doi = {10.1016/j.entcs.2016.09.039},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {bilattices,bitopological spaces,d-frames,four-valued logic,nd-frames},
month = oct,
pages = {201--219},
title = {Bitopology and Four-valued Logic},
volume = {325},
year = {2016}
}
@phdthesis{Clarkson2010a,
abstract = {Computer security policies often are stated informally in terms of confidentiality, integrity, and availability of information and resources; these policies can be qualitative or quantitative. To formally quantify confidentiality and integrity, a new model of quantitative information flow is proposed in which information flow is quantified as the change in the accuracy of an observers beliefs. This new model resolves anomalies present in previous quantitative information-flow models, which are based on change in uncertainty. And the new model is sufficiently general that it can be instantiated to measure either accuracy or uncertainty. To formalize security policies in general, a generalization of the theory of trace properties (originally developed for program verification) is proposed. Security policies are modeled as hyperproperties, which are sets of trace properties. Although important security policies, such as secure information flow, cannot be expressed as trace properties, they can be expressed as hyperproperties. Safety and liveness are generalized from trace properties to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. Verification, refinement, and topology of hyperproperties are also addressed. Hyperproperties for system representations beyond trace sets are investigated.},
author = {Clarkson, Michael Ryan},
booktitle = {New York},
number = {February},
school = {Cornell University},
title = {Quantification and Formalization of Security},
year = {2010}
}
@incollection{Minkus2014,
abstract = {eBay is an online marketplace which allows people to easily engage in commerce with one another. Since the market's online nature precludes many physical cues of trust, eBay has instituted a reputation system through which users accumulate ratings based on their transactions. However, the eBay Feedback System as currently implemented has serious privacy flaws. When sellers leave feedback, buyers' purchase histories are exposed through no action of their own. In this paper, we describe and execute a series of attacks, leveraging the feedback system to reveal users' potentially sensitive purchases. As a demonstration, we collect and identify users who have bought gun-related items and sensitive medical tests. We contrast this information leakage with eBay users' privacy expectations as measured by an online survey. Finally, we make recommendations towards better privacy in the eBay feedback system.},
author = {Minkus, Tehila and Ross, Keith W.},
booktitle = {Priv. Enhancing Technol. PETS 2014},
doi = {10.1007/978-3-319-08506-7_9},
editor = {Cristofaro, Emiliano De and Murdoch, Steven J.},
isbn = {9783319085050},
issn = {16113349},
pages = {164--183},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {I Know What You're Buying: Privacy Breaches on eBay},
volume = {8555},
year = {2014}
}
@inproceedings{Bonsangue2009,
author = {Bonsangue, Marcello M. and Rutten, Jan J.M.M. and Silva, Alexandra},
booktitle = {24th Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2009.18},
isbn = {978-0-7695-3746-7},
month = aug,
pages = {49--58},
publisher = {IEEE},
title = {An Algebra for Kripke Polynomial Coalgebras},
year = {2009}
}
@article{Lack2009,
abstract = {Categorical universal algebra can be developed either using Lawvere theories (single-sorted finite product theories) or using monads, and the category of Lawvere theories is equivalent to the category of finitary monads on Set. We show how this equivalence, and the basic results of universal algebra, can be generalized in three ways: replacing Set by another category, working in an enriched setting, and by working with another class of limits than finite products. An important special case involves working with sifted-colimit-preserving monads rather than filtered-colimit-preserving ones.},
archivePrefix = {arXiv},
arxivId = {0810.2578},
author = {Lack, Stephen and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1007/s10485-009-9215-2},
eprint = {0810.2578},
issn = {0927-2852},
journal = {Appl. Categ. Struct.},
month = nov,
number = {1},
pages = {363--391},
title = {Notions of Lawvere Theory},
volume = {19},
year = {2009}
}
@article{Adamek2000,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Koubek, V{\'{a}}clav and Velebil, Jiř{\'{i}}},
issn = {0010-2628},
journal = {Comment. Math. Univ. Carolinae},
number = {3},
pages = {529--541},
title = {A duality between infinitary varieties and algebraic theories},
volume = {41},
year = {2000}
}
@article{Rutten2000,
author = {Rutten, Jan J.M.M.},
doi = {10.1016/S0304-3975(00)00056-6},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {3--80},
publisher = {Elsevier},
title = {Universal coalgebra: a theory of systems},
type = {Journal article},
volume = {249},
year = {2000}
}
@article{Nganou2015,
author = {Nganou, Jean B.},
doi = {10.1007/s11083-014-9345-5},
issn = {0167-8094},
journal = {Order},
keywords = {dually equivalent,finitely approximable,maximal ideal,multiset,mv-algebra,profinite,stone mv-algebra},
month = jan,
number = {April 2014},
title = {Profinite MV-algebras and multisets},
year = {2015}
}
@incollection{Fujii2016,
abstract = {In the mid-nineties, Turi and Plotkin gave an elegant categorical treatment of denotational and operational semantics for process algebra-like languages, proving compositionality and adequacy by defining operational semantics as a distributive law of syntax over behaviour. However, its applications to stateful or effectful languages, incorporating (co)models of a countable Lawvere theory, have been elusive so far. We make some progress towards a coalgebraic treatment of such languages, proposing a congruence format related to the evaluation-in-context paradigm. We formalise the denotational semantics in suitable Kleisli categories, and prove adequacy and compositionality of the semantic theory under this congruence format. {\textcopyright} 2013 Springer-Verlag.},
author = {Fujii, Soichiro and Katsumata, Shin-ya and Melli{\`{e}}s, Paul-Andr{\'{e}}},
booktitle = {Proc. 19th Int. Conf. Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-662-49630-5_30},
editor = {Jacobs, Bart and L{\"{o}}ding, Christof},
isbn = {978-3-662-49629-9},
issn = {0302-9743},
pages = {513--530},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Towards a Formal Theory of Graded Monads},
year = {2016}
}
@book{Brink2001,
author = {Brink, Chris and Rewitsky, Ingrid M.},
isbn = {1575863448},
publisher = {CSLI Publications Stanford, CA, USA},
series = {Studies in Logic, Language, and Information},
title = {A paradigm for program semantics: power structures and duality},
type = {Book},
year = {2001}
}
@article{Dang2011,
author = {Dang, H.-H. and H{\"{o}}fner, P. and M{\"{o}}ller, B.},
doi = {10.1016/j.jlap.2011.04.003},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
month = aug,
number = {6},
pages = {221--247},
publisher = {Elsevier Inc.},
title = {Algebraic separation logic},
volume = {80},
year = {2011}
}
@book{Lamport2002,
author = {Lamport, Leslie},
edition = {1},
isbn = {032114306X},
pages = {384},
publisher = {Addison-Wesley Professional},
title = {Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers},
year = {2002}
}
@incollection{Baltag2000,
abstract = {Building on the work of L. Moss on coalgebraic logic, we study in a general setting a class of infinitary modal logics for F-coalgebras, designed to capture simulation and bisimulation. We use work by A. Thijs on coalgebraic modelling of simulation, in terms of relators ?? as extensions of functors. We prove our logics can indeed capture simulation and bisimulation, i.e. the existence of a simulation (or bisimulation) is equivalent to the preservation of (or equivalence with respect to) certain classes of sentences. Moreover, we prove that one can characterize any given coalgebra up to simulation (and, in certain conditions, up to bisimulation) by a single sentence. We show that truth for this logic can be understood as a simulation relation itself, but with respect to a richer functor F moreover, it is the the largest simulation, i.e. the similarity relation between states of the coalgebra and elements of the language. This sheds a new perspective on the classical preservation and characterizability results, and also on logic games. The two kinds of games normally used in logic ("truth games" to define the semantics dynamically, and "similarity games" between two structures) are seen to be the same kind of game at the level of coalgebras: simulation games. This work has been carried out under the project SEN3.4 "PROMACS" . I thank Jan Rutten, Larry Moss, Martin Rossiger and Yde Venema for useful conversations and comments on the topics of this paper. ?? 2000 Published by Elsevier Science B.V.},
author = {Baltag, Alexandru},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/S1571-0661(05)80343-3},
issn = {15710661},
pages = {42--60},
title = {A logic for coalgebraic simulation},
volume = {33},
year = {2000}
}
@article{Dupre2009,
abstract = {By basing Bayesian probability theory on five axioms, we can give a trivial proof of Cox's Theorem on the product rule and sum rule for conditional plausibility without assuming continuity or differentiablity of plausibility. Instead, we extend the notion of plausibility to apply to unknowns, giving them plausi-ble values. Thus, we combine the best aspects of two approaches to Bayesian probability theory, namely the Cox-Jaynes theory and the de Finetti theory.},
author = {Dupr{\'{e}}, Maurice J. and Tipler, Frank J.},
doi = {10.1214/09-BA422},
isbn = {1936-0975},
issn = {1936-0975},
journal = {Bayesian Anal.},
keywords = {Axiomatic bayesian probability,Cox,De Finetti,Jaynes,Product rule,Sum rule},
month = sep,
number = {3},
pages = {599--606},
title = {New axioms for rigorous Bayesian probability},
volume = {4},
year = {2009}
}
@article{Adamek1977,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
doi = {10.1017/S0004972700010704},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
number = {03},
pages = {433},
title = {Colimits of algebras revisited},
volume = {17},
year = {1977}
}
@article{Terrovitis2011,
abstract = {In this paper, we study the problem of protecting privacy in the publication of set-valued data. Consider a collection of supermarket transactions that contains detailed information about items bought together by individuals. Even after removing all personal characteristics of the buyer, which can serve as links to his identity, the publication of such data is still subject to privacy attacks from adversaries who have partial knowledge about the set. Unlike most previous works, we do not distinguish data as sensitive and non-sensitive, but we consider them both as potential quasi-identifiers and potential sensitive data, depending on the knowledge of the adversary. We define a new version of the k-anonymity guarantee, the k (m) -anonymity, to limit the effects of the data dimensionality, and we propose efficient algorithms to transform the database. Our anonymization model relies on generalization instead of suppression, which is the most common practice in related works on such data. We develop an algorithm that finds the optimal solution, however, at a high cost that makes it inapplicable for large, realistic problems. Then, we propose a greedy heuristic, which performs generalizations in an Apriori, level-wise fashion. The heuristic scales much better and in most of the cases finds a solution close to the optimal. Finally, we investigate the application of techniques that partition the database and perform anonymization locally, aiming at the reduction of the memory consumption and further scalability. A thorough experimental evaluation with real datasets shows that a vertical partitioning approach achieves excellent results in practice.},
author = {Terrovitis, Manolis and Mamoulis, Nikos and Kalnis, Panos},
doi = {10.1007/s00778-010-0192-8},
issn = {1066-8888},
journal = {VLDB J.},
keywords = {Anonymity,Database privacy,Set-valued data},
month = feb,
number = {1},
pages = {83--106},
title = {Local and global recoding methods for anonymizing set-valued data},
volume = {20},
year = {2011}
}
@incollection{Matsubara2009,
author = {Czarnetzki, Silke and Krebs, Andreas},
booktitle = {Proc. 10th Int. Conf. Lang. Autom. Theory Appl.},
doi = {10.1007/978-3-319-30000-9_22},
editor = {Truthe, Adrian-Horia Dediu and Janou{\v{s}}ek, Jan and Mart{\'{i}}n-Vide, Carlos and Truthe, Bianca},
isbn = {978-3-642-00981-5},
pages = {283--294},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
title = {Using Duality in Circuit Complexity},
volume = {5457},
year = {2016}
}
@incollection{Benton2002,
abstract = {A tension in language design has been between simple semantics on the one hand, and rich possibilities for side-effects, exception handling and so on on the other. The introduction of monads has made a large step towards reconciling these alternatives. First proposed by Moggi as a way of structuring semantic descriptions, they were adopted by Wadler to structure Haskell programs. Monads have been used to solve long-standing problems such as adding pointers and assignment, inter-language working, and exception handling to Haskell, without compromising its purely functional semantics. The course introduces monads, effects, and exemplifies their applications in programming (Haskell) and in compilation (MLj). The course presents typed metalanguages for monads and related categorical notions, and then describes how they can be further refined by introducing effects.},
author = {Benton, Nick and Hughes, John and Moggi, Eugenio},
booktitle = {Appl. Semant.},
doi = {10.1007/3-540-45699-6_2},
editor = {Barthe, Gilles and Dybjer, Peter and Pinto, Lu{\'{i}}s and Saraiva, Jo{\~{a}}o},
isbn = {978-3-540-44044-4},
pages = {923--952},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Monads and Effects},
type = {Book part (with own title)},
volume = {2395},
year = {2002}
}
@article{Bezhanishvili2012,
abstract = {We introduce modal compact Hausdor spaces as generalizations of modal spaces, and show these are coalgebras for the Vietoris functor on compact Hausdor spaces. Modal compact regular frames and modal de Vries algebras are introduced as algebraic counterparts of modal compact Hausdor spaces, and dualities are given for the categories involved. These extend the familiar Isbell and de Vries dualities for compact Hausdor spaces, as well as the duality between modal spaces and modal algebras. As the first step in the logical treatment of modal compact Hausdor spaces, a version of Sahlqvist correspondence is given for the positive modal language.},
author = {Bezhanishvili, Guram and Bezhanishvili, Nick and Harding, John},
doi = {10.1093/logcom/exs030},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {compact hausdorff space,de vries duality,modal algebra,vietoris space},
month = jul,
title = {Modal compact Hausdorff spaces},
year = {2012}
}
@article{Adamek1989a,
abstract = {Monadic decomposition of adjoints, as introduced by H. Appelgate and M. Tierney, are investigated: sharper conditions under which the decomposition 'converges' are found, examples of non-convergent decompositions are presented, and the role that solid (semi-topological) functors play is made clear. {\textcopyright} 1989.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Herrlich, Horst and Tholen, Walter},
doi = {10.1016/0022-4049(89)90129-1},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {2},
pages = {111--123},
title = {Monadic decompositions},
volume = {59},
year = {1989}
}
@article{Schroder2007,
author = {Schr{\"{o}}der, Lutz},
doi = {10.1016/j.jlap.2006.11.004},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
keywords = {coalgebra,decidability,finite models,modal logic,weak completeness},
month = sep,
number = {1-2},
pages = {97--110},
title = {A finite model construction for coalgebraic modal logic},
volume = {73},
year = {2007}
}
@article{Barth-Jones2012,
author = {Barth-Jones, Daniel C.},
doi = {10.2139/ssrn.2076397},
issn = {1556-5068},
journal = {SSRN Electron. J.},
keywords = {de-identification,hipaa,population,privacy,statistical disclosure},
pages = {1--19},
title = {The 'Re-Identification' of Governor William Weld's Medical Information: A Critical Re-Examination of Health Data Identification Risks and Privacy Protections, Then and Now},
year = {2012}
}
@article{Carboni1987,
author = {Carboni, A. and Walters, R.F.C.},
doi = {10.1016/0022-4049(87)90121-6},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1-2},
pages = {11--32},
title = {Cartesian bicategories I},
volume = {49},
year = {1987}
}
@article{Power1990,
abstract = {Pasting is the fundamental operation within a 2-category. However, until recently, it had never been proved that the operation of pasting is well defined. In fact, a 2-categorical pasting theorem had not even been properly formulated. Herein, we state and prove such a result. This brings together two strands of the current work of the Sydney Category Theory school: taking the general theory of n-categories, and applying its ideas to the particular case of 2-categories, with heavy use of the techniques of Graph Theory. This provides a more solid foundation for the development of 2-categories.},
author = {Power, A. John},
doi = {10.1016/0021-8693(90)90229-H},
issn = {00218693},
journal = {J. Algebr.},
number = {2},
pages = {439--445},
title = {A 2-categorical pasting theorem},
volume = {129},
year = {1990}
}
@techreport{Chong2016,
abstract = {Report on the NSF Workshop on Formal Methods for Security, held 19-20 November 2015.},
archivePrefix = {arXiv},
arxivId = {1608.00678},
author = {Chong, Stephen and Guttman, Joshua and Datta, Anupam and Myers, Andrew and Pierce, Benjamin and Schaumont, Patrick and Sherwood, Tim and Zeldovich, Nickolai},
eprint = {1608.00678},
month = aug,
title = {Report on the NSF Workshop on Formal Methods for Security},
year = {2016}
}
@article{Cirstea2006,
abstract = {We propose a modular approachto defining notions of simulation, and modal logics whichcharacterise them. We use coalgebras to model state-based systems, relators to define notions of simulation for such systems, and inductive techniques to define the syntax and semantics of modal logics for coalgebras. We show that the expressiveness of an inductively defined logic for coalgebras w.r.t. a notion of simulation follows from an expressivity condition involving one stepin the definitionofthe logic, and the relator inducing that notion of simulation. Moreover, we show that notions of simulation and associated characterising logics for increasingly complex system types can be derived by lifting the operations used to combine system types, to a relational level as well as to a logical level. We use these results to obtain Baltag's logic for coalgebraic simulation, as well as notions of simulation and associated logics for a large class of non-deterministic and probabilistic systems. {\textcopyright} 2005 Elsevier Inc. All rights reserved.},
author = {C{\^{i}}rstea, Corina},
doi = {10.1016/j.ic.2005.04.005},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Coalgebra,Modal logic,Probabilistic system,Simulation},
month = apr,
number = {4},
pages = {469--502},
title = {A modular approach to defining and characterising notions of simulation},
volume = {204},
year = {2006}
}
@article{Williams1969,
author = {Williams, N. H.},
journal = {Compos. Math.},
pages = {1--3},
title = {On Grothendieck universes},
volume = {1},
year = {1969}
}
@article{Pattinson2003a,
author = {Pattinson, Dirk},
doi = {10.1016/S1571-0661(04)80642-X},
editor = {Gumm, H. Peter},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jul,
number = {1},
pages = {237--256},
publisher = {Elsevier B.V.},
title = {Computable Functions on Final Coalgebras},
volume = {82},
year = {2003}
}
@incollection{Aczel1989a,
author = {Aczel, Peter and Mendler, Nax Paul},
booktitle = {Categ. Theory Comput. Sci.},
doi = {10.1007/BFb0018361},
pages = {357--365},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A final coalgebra theorem},
type = {Book part (with own title)},
volume = {389},
year = {1989}
}
@incollection{Altenkirch2010,
address = {Berlin, Heidelberg},
author = {Altenkirch, Thorsten and Chapman, James and Uustalu, Tarmo},
booktitle = {Proc. 13th Int. Conf. Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-12032-9},
editor = {Ong, Luke},
isbn = {978-3-642-12031-2},
issn = {0302-9743},
pages = {297--311},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Monads need not be endofunctors},
year = {2010}
}
@inproceedings{Abel2013b,
address = {New York, New York, USA},
author = {Abel, Andreas M. and Pientka, Brigitte and Thibodeau, David and Setzer, Anton},
booktitle = {Proc. 40th Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '13},
doi = {10.1145/2429069.2429075},
isbn = {9781450318327},
keywords = {2008,by the graduiertenkol-,coinduction,elimination,functional programming,introduction,leg programm und modellanalyse,message passing,of the deutsche,pattern matching,puma,thibodeau acknowledges financial support,vs},
pages = {27},
publisher = {ACM Press},
title = {Copatterns},
year = {2013}
}
@article{Møgelberg2014,
address = {New York, New York, USA},
author = {M{\o}gelberg, Rasmus Ejlers},
doi = {10.1145/2603088.2603132},
isbn = {9781450328869},
journal = {Proc. Jt. Meet. Twenty-Third EACSL Annu. Conf. Comput. Sci. Log. Twenty-Ninth Annu. ACM/IEEE Symp. Log. Comput. Sci. - CSL-LICS '14},
keywords = {categorical semantics,corecursion,de-,dependent types,guarded recursion,notational semantics},
number = {1},
pages = {1--10},
publisher = {ACM Press},
title = {A type theory for productive coprogramming via guarded recursion},
year = {2014}
}
@article{Adamek1995a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Koubek, V{\'{a}}clav},
doi = {10.1016/0304-3975(95)00011-K},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {57--75},
title = {On the greatest fixed point of a set functor},
type = {Journal article},
volume = {150},
year = {1995}
}
@article{VanBreugel2012,
author = {van Breugel, Franck},
doi = {10.1016/j.ipl.2012.06.019},
issn = {00200190},
journal = {Inf. Process. Lett.},
month = oct,
number = {19},
pages = {715--718},
publisher = {Elsevier B.V.},
title = {On behavioural pseudometrics and closure ordinals},
volume = {112},
year = {2012}
}
@book{Mader1997,
abstract = {In this paper we show the equivalence of model checking infinite systems\nand solving infinite Boolean equation systems, andgive a method that\nsolves infinite Boolean equation systems. The method issound and\ncomplete, even if the problem itself is undecidable.},
address = {Berlin},
author = {Mader, Angelika},
isbn = {9783929470581},
issn = {1571-5078},
publisher = {Bertz Verlag},
series = {Edition versal 8},
title = {Verification of Modal Properties using Boolean Equation Systems},
year = {1997}
}
@book{MacKay2003,
abstract = {This book is aimed at senior undergraduates and graduate students in Engineering, Science, Mathematics, and Computing. It expects familiarity with calculus, probability theory, and linear algebra as taught in a rst- or secondyear undergraduate course on mathematics for scientists and engineers. Conventional courses on information theory cover not only the beautiful theoretical ideas of Shannon, but also practical solutions to communication problems. This book goes further, bringing in Bayesian data modelling, Monte Carlo methods, variational methods, clustering algorithms, and neural networks. Why unify information theory and machine learning? Because they are two sides of the same coin. In the 1960s, a single eld, cybernetics, was populated by information theorists, computer scientists, and neuroscientists, all studying common problems. Information theory and machine learning still belong together. Brains are the ultimate compression and communication systems. And the state-of-the-art algorithms for both data compression and error-correcting codes use the same tools as machine learning.},
archivePrefix = {arXiv},
arxivId = {arXiv:1011.1669v3},
author = {MacKay, David J. C.},
doi = {10.1198/jasa.2005.s54},
eprint = {arXiv:1011.1669v3},
isbn = {9780521642989},
issn = {01621459},
pages = {640},
pmid = {13217055},
publisher = {Cambridge University Press},
title = {Information Theory, Inference & Learning Algorithms},
year = {2003}
}
@article{Hasuo2007,
abstract = {Trace semantics has been defined for various kinds of state-based systems, notably with different forms of branching such as non-determinism vs. probability. In this paper we claim to identify one underlying mathematical structure behind these "trace semantics," namely coinduction in a Kleisli category. This claim is based on our technical result that, under a suitably order-enriched setting, a final coalgebra in a Kleisli category is given by an initial algebra in the category Sets. Formerly the theory of coalgebras has been employed mostly in Sets where coinduction yields a finer process semantics of bisimilarity. Therefore this paper extends the application field of coalgebras, providing a new instance of the principle "process semantics via coinduction."},
archivePrefix = {arXiv},
arxivId = {0710.2505},
author = {Hasuo, Ichiro and Jacobs, Bart and Sokolova, Ana},
doi = {10.2168/LMCS-3(4:11)2007},
editor = {Rutten, Jan},
eprint = {0710.2505},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = nov,
number = {4},
pages = {36},
title = {Generic trace semantics via coinduction},
volume = {3},
year = {2007}
}
@book{Codd1990,
abstract = {From the Preface (See Front Matter for full Preface) An important adjunct to precision is a sound theoretical foundation. The relational model is solidly based on two parts of mathematics: firstorder predicate logic and the theory of relations. This book, however, does not dwell on the theoretical foundations, but rather on all the features of the relational model that I now perceive as important for database users, and therefore for DBMS vendors. My perceptions result from 20 years of practical experience in computing and data processing (chiefly, but not exclusively, with large-scale customers of IBM), followed by another 20 years of research. I believe that this is the first book to deal exclusively with the relational approach. It does, however, include design principles in Chapters 21 and 22. It is also the first book on the relational model by the originator of that model. All the ideas in the relational model described in this book are mine, except in cases where I explicitly credit someone else. In developing the relational model, I have tried to follow Einstein's advice, "Make it as simple as possible, but no simpler." I believe that in the last clause he was discouraging the pursuit of simplicity to the extent of distorting reality. So why does the book contain 30 chapters and two appendixes? To answer this question, it is necessary to look at the history of research and development of the relational model.},
author = {Codd, E. F.},
isbn = {0201141922},
pages = {538},
pmid = {1917145},
publisher = {Pearson},
title = {The Relational Model for Database Management: Version 2},
year = {1990}
}
@article{Wilke1996,
abstract = {The class of frontier testable (i.e., reverse definite) tree languages is characterized by a finite set of pseudoidentities for tree algebras, which are introduced here for this characterization. An efficient algorithm is presented that decides whether a given tree automaton recognizes a frontier testable tree language. The algorithm runs in time O(mn3 +m2n2), where m is the cardinality of the alphabet and n is the number of states of the automaton.},
author = {Wilke, Thomas},
doi = {10.1016/0304-3975(95)00131-X},
issn = {03043975},
journal = {Theor. Comput. Sci.},
number = {1},
pages = {85--106},
title = {An algebraic characterization of frontier testable tree languages},
volume = {154},
year = {1996}
}
@article{Kelly1980,
abstract = {Many problems lead to the consideration of “algebras”, given by an object A of a category A together with “actions” TkA → A on A of one or more endofunctors of A, subjected to equational axioms. Such problems include those of free monads and free monoids, of cocompleteness in categories of monads and of monoids, of orthogonal subcategories (= generalized sheaf-categories), of categories of continuous functors, and so on; apart from problems involving the algebras for their own sake. Desirable properties of the category of algebras - existence of free ones, cocompleteness, existence of adjoints to algebraic functors - all follow if this category can be proved reflective in some well-behaved category: for which we choose a certain comma-category T/A We show that the reflexion exists and is given as the colimit of a simple transfinite sequence, if A is cocomplete and the Tk preserve either colimits or unions of suitably-long chains of subobjects. The article draws heavily on the work of earlier authors, unifies and simplifies this, and extends it to new problems. Moreover the reflectivity in T/A is stronger than any earlier result, and will be applied in forthcoming articles, in an enriched version, to the study of categories with structure.},
author = {Kelly, Gregory Maxwell},
doi = {10.1017/S0004972700006353},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = apr,
number = {01},
pages = {1},
title = {A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on},
volume = {22},
year = {1980}
}
@article{Blackwell1989a,
author = {Blackwell, Robert and Kelly, Gregory Maxwell and Power, A. John},
doi = {10.1016/0022-4049(89)90160-6},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jul,
number = {1},
pages = {1--41},
title = {Two-dimensional monad theory},
volume = {59},
year = {1989}
}
@inproceedings{Hansson1990,
author = {Hansson, H. and Jonsson, B.},
booktitle = {Real-Time Syst. RTSS 90},
doi = {10.1109/REAL.1990.128759},
isbn = {0-8186-2112-5},
pages = {278--287},
publisher = {IEEE},
title = {A calculus for communicating systems with time and probabilities},
year = {1990}
}
@incollection{Nordstrom2000,
author = {Nordstr{\"{o}}m, Bengt and Petersson, Kent and Smith, Jan M.},
booktitle = {Handb. Log. Comput. Sci.},
isbn = {978-0-19-853781-6},
number = {October},
publisher = {Oxford University Press},
title = {Martin-L{\"{o}}f Type Theory},
volume = {5},
year = {2000}
}
@article{Hyland2002,
author = {Hyland, Martin and Power, A. John},
doi = {10.1016/S0022-4049(02)00133-0},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1-3},
pages = {141--185},
title = {Pseudo-commutative monads and pseudo-closed 2-categories},
volume = {175},
year = {2002}
}
@book{Adamek1994,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.2277/0521422612},
isbn = {9780521422611},
pages = {332},
publisher = {Cambridge University Press},
series = {London Mathematical Society Lecture Note Series},
title = {Locally Presentable and Accessible Categories},
year = {1994}
}
@article{Jacobs2016,
abstract = {This paper establishes a link between Bayesian inference (learning) and predicate and state transformer operations from programming semantics and logic. Specifically, a very general definition of backward inference is given via first applying a predicate transformer and then conditioning. Analogously, forward inference involves first conditioning and then applying a state transformer. These definitions are illustrated in many examples in discrete and continuous probability theory and also in quantum theory.},
author = {Jacobs, Bart and Zanasi, Fabio},
doi = {10.1016/j.entcs.2016.09.038},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Bayes,Inference,Kleisli category,effectus,learning,predicate transformer,state transformer},
month = oct,
pages = {185--200},
publisher = {Elsevier B.V.},
title = {A predicate/state transformer semantics for Bayesian learning},
volume = {325},
year = {2016}
}
@article{Guitart1980,
author = {Guitart, Ren{\'{e}}},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {1},
pages = {5--62},
title = {Tenseurs et machines},
volume = {21},
year = {1980}
}
@article{Low2013,
archivePrefix = {arXiv},
arxivId = {1304.5227},
author = {Low, Zhen Lin},
eprint = {1304.5227},
journal = {ArXiv e-prints},
pages = {1--27},
title = {Universes for category theory},
year = {2013}
}
@article{Kingdom2015a,
abstract = {Writing formal specifications for distributed systems is difficult. Even simple consistency requirements often turn out to be unrealizable because of the complicated information flow in the distributed system: not all information is available in every component, and information transmitted from other components may arrive with a delay or not at all, especially in the presence of faults. The problem of checking the distributed realizability of a temporal specification is, in general, undecidable. Semi-algorithms for synthesis, such as bounded synthesis, are only useful in the positive case, where they construct an implementation for a realizable specification, but not in the negative case: if the specification is unrealizable, the search for the implementation never terminates. In this paper, we introduce counterexamples to distributed realizability and present a method for the detection of such counterexamples for specifications given in linear-time temporal logic (LTL). A counterexample consists of a set of paths, each representing a different sequence of inputs from the environment, such that, no matter how the components are implemented, the specification is violated on at least one of these paths. We present a method for finding such counterexamples both for the classic distributed realizability problem and for the fault-tolerant realizability problem. Our method considers, incrementally, larger and larger sets of paths until a counterexample is found. For safety specifications in weakly ordered architectures we obtain a decision procedure, while counterexamples for full LTL and arbitrary architectures may consist of infinitely many paths. Experimental results, obtained with a QBF-based prototype implementation, show that our method finds simple errors very quickly, and even problems with high combinatorial complexity, like the Byzantine Generals' Problem, are tractable.},
archivePrefix = {arXiv},
arxivId = {1505.06862},
author = {Bonchi, Filippo and Zanasi, Fabio},
doi = {10.2168/LMCS-11(1:14)2015},
editor = {Milius, Stefan},
eprint = {1505.06862},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {algebraic techniques in automata,and phrases,probabilistic automata,value 1 problem},
month = mar,
number = {1},
pages = {1--50},
title = {Bialgebraic Semantics for Logic Programming},
volume = {11},
year = {2015}
}
@book{Jones1999,
abstract = {Partial evaluation reconciles generality with efficiency by providing automated specialization and optimization of programs. This book covers the entire field of partial evaluation and takes the reader through a gentle introduction to state-of-the-art techniques. It is the first complete book on automatic partial evaluation to provide a practical and theoretically well-founded overview. Simple and complete algorithms are included and the book demonstrates by numerous examples that specialization can increase efficiency considerably.},
author = {Jones, Neil D. and Gomard, Carsten K. and Sestoft, Peter},
isbn = {0130202495},
month = jun,
pages = {xii + 415},
publisher = {Prentice Hall International},
title = {Partial Evaluation and Automatic Program Generation},
year = {1999}
}
@article{Abramsky2002,
author = {Abramsky, Samson and Haghverdi, Esfandiar and Scott, Philip},
doi = {10.1017/S0960129502003730},
isbn = {0960129502},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = oct,
number = {05},
pages = {625--665},
title = {Geometry of Interaction and linear combinatory algebras},
volume = {12},
year = {2002}
}
@article{ONeill2009,
abstract = {A much beloved and widely used example showing the elegance and simplicity of lazy functional programming represents itself as The Sieve of Eratosthenes. This paper shows that this example is not the sieve, and presents an implementation that actually is.},
author = {O'NEILL, MELISSA E.},
doi = {10.1017/S0956796808007004},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = jan,
number = {01},
pages = {95},
title = {The Genuine Sieve of Eratosthenes},
volume = {19},
year = {2009}
}
@article{Perkov2012,
author = {Perkov, Tin and Vukovi{\'{c}}, Mladen},
doi = {10.1016/j.apal.2012.07.001},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
month = jul,
pages = {1--12},
title = {Some characterization and preservation theorems in modal logic},
volume = {1},
year = {2012}
}
@article{Denniston2014,
author = {Denniston, Jeffrey T. and Melton, Austin C. and Rodabaugh, Stephen E.},
doi = {10.1016/j.fss.2014.05.008},
issn = {0165-0114},
journal = {Fuzzy Sets Syst.},
keywords = {1,Antisymmetry,Data-mining,Enriched categories,Enriched/preordered sets,Left- and right-residuations,Many-valued preorders,Order-reversing and order-preserving involutions,Partially ordered groupoids and ringoids,Pattern-matching,Skeletons,T0 separation axiom,Unital quantales,and spectra,and topological spaces,antisymmetry,data-mining,enriched,enriched categories,hemimetrics,introduction and motivations,left- and right-residuations,many-valued preorders,order-preserving involutions,order-reversing and,partially ordered groupoids and,pattern-matching,preordered sets,ringoids,skeletons,specialization orders,t 0 separation axiom,topological systems,unital quantales},
pages = {4--56},
publisher = {Elsevier},
title = {Enriched categories and many-valued preorders: Categorical, semantical, and topological perspectives},
volume = {256},
year = {2014}
}
@article{Ada,
abstract = {In the theory of accessible categories, pure subobjects, i.e. filtered colimits of split monomorphisms, play an important role. Here we investigate pure quotients, i.e., filtered colimits of split epimorphisms. For example, in abelian, finitely accessible categories, these are precisely the cokernels of pure subobjects, and pure subobjects are precisely the kernels of pure quotients.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Rosick{\'{y}}, Jiř{\'{i}}},
issn = {0011-4642},
journal = {Czechoslov. Math. J.},
keywords = {abelian category,locally presentable category,pure quotient,pure subobject,semi-abelian category},
language = {eng},
number = {3},
pages = {623--636},
title = {On pure quotients and pure subobjects},
volume = {54},
year = {2004}
}
@article{Kozen2014,
author = {Kozen, Dexter and Mardare, Radu and Panangaden, Prakash},
doi = {10.1016/j.entcs.2014.10.012},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {aumann algebras,isometry,markov processes,metrics,probabilistic reasoning,quantitative reasoning,stone duality},
month = oct,
pages = {211--227},
title = {A Metrized Duality Theorem for Markov Processes},
volume = {308},
year = {2014}
}
@article{Fine1975,
author = {Fine, Kit},
doi = {10.1305/ndjfl/1093891703},
issn = {0029-4527},
journal = {Notre Dame J. Form. Log.},
month = apr,
number = {2},
pages = {229--237},
title = {Normal forms in modal logic},
volume = {16},
year = {1975}
}
@article{Giunti2011,
author = {Giunti, Marco and Mazzola, Claudio},
doi = {10.1142/9789814383332},
isbn = {9789814383332},
journal = {{\ldots} Approaches Towar. a Gen. Theory {\ldots}},
keywords = {category theory,dynamical system,irreversibility,reversibility},
number = {iii},
pages = {1--13},
title = {Dynamical Systems on Monoids: Toward a General Theory of Deterministic Systems and Motion},
volume = {0},
year = {2011}
}
@incollection{Johnstone1985a,
address = {New York},
author = {Johnstone, Peter T.},
booktitle = {Contin. lattices their Appl.},
pages = {155--180},
publisher = {Marcel Dekker},
series = {Lecture Notes in Pure and Applied Mathematics},
title = {Vietoris locales and localic semilattices},
type = {Book part (with own title)},
year = {1985}
}
@article{GUMM2002,
author = {Gumm, H. Peter and Schr{\"{o}}der, Tobias},
issn = {1469-8072},
journal = {Math. Struct. Comput. Sci.},
language = {English},
month = oct,
number = {05},
pages = {565--578},
title = {Coalgebras of bounded type},
volume = {12},
year = {2002}
}
@incollection{Almeida2005,
address = {Dordrecht},
author = {Almeida, Jorge},
booktitle = {Struct. Theory Autom. Semigroups, Univers. Algebr.},
doi = {10.1007/1-4020-3817-8},
editor = {Kudryavtsev, Valery B. and Rosenberg, Ivo G. and Goldstein, Martin},
isbn = {1-4020-3815-1},
pages = {1--45},
publisher = {Springer-Verlag},
series = {NATO Science Series II: Mathematics, Physics and Chemistry},
title = {Profinite semigroups and applications},
volume = {207},
year = {2005}
}
@article{Leal2009,
author = {Leal, Raul Andres and Kupke, Clemens},
journal = {ILLC Prepublications/ILLC},
title = {Of the Hennessy-Milner property and Other Demons},
type = {Journal article},
year = {2009}
}
@phdthesis{Appelgate1965,
author = {Appelgate, Harry Wesley},
pages = {90},
school = {Columbia University},
title = {Acyclic models and resolvent functors},
year = {1965}
}
@book{Jones1997,
author = {Jones, Neil D.},
booktitle = {Electron. Notes Theor. Comput. Sci.},
isbn = {0-262-10064-9},
pages = {467},
publisher = {The MIT Press},
series = {Foundations of Computing},
title = {Computability and Complexity: From a Programming Perspective},
year = {1997}
}
@article{Kurz2013a,
abstract = {We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets. We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).},
author = {Kurz, Alexander and Velebil, Jiř{\'{i}}},
doi = {10.1017/S096012951500050X},
isbn = {0960129515000},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = jan,
number = {1983},
pages = {1--42},
title = {Quasivarieties and varieties of ordered algebras: regularity and exactness},
year = {2016}
}
@article{Homer2008,
abstract = {We use high-density single nucleotide polymorphism (SNP) genotyping microarrays to demonstrate the ability to accurately and robustly determine whether individuals are in a complex genomic DNA mixture. We first develop a theoretical framework for detecting an individual's presence within a mixture, then show, through simulations, the limits associated with our method, and finally demonstrate experimentally the identification of the presence of genomic DNA of specific individuals within a series of highly complex genomic mixtures, including mixtures where an individual contributes less than 0.1% of the total genomic DNA. These findings shift the perceived utility of SNPs for identifying individual trace contributors within a forensics mixture, and suggest future research efforts into assessing the viability of previously sub-optimal DNA sources due to sample contamination. These findings also suggest that composite statistics across cohorts, such as allele frequency or genotype counts, do not mask identity within genome-wide association studies. The implications of these findings are discussed.},
archivePrefix = {arXiv},
arxivId = {1310.3197},
author = {Homer, Nils and Szelinger, Szabolcs and Redman, Margot and Duggan, David and Tembe, Waibhav and Muehling, Jill and Pearson, John V. and Stephan, Dietrich A. and Nelson, Stanley F. and Craig, David W.},
doi = {10.1371/journal.pgen.1000167},
editor = {Visscher, Peter M.},
eprint = {1310.3197},
isbn = {1553-7404},
issn = {1553-7404},
journal = {PLoS Genet.},
month = aug,
number = {8},
pages = {e1000167},
pmid = {18769715},
title = {Resolving Individuals Contributing Trace Amounts of DNA to Highly Complex Mixtures Using High-Density SNP Genotyping Microarrays},
volume = {4},
year = {2008}
}
@article{Banaschewski1983,
author = {Banaschewski, Bernhard},
doi = {10.1007/BF01194543},
isbn = {0303604395},
journal = {Algebr. universalis},
number = {1},
pages = {360--368},
title = {The Birkhoff Theorem for varieties of finite algebras},
volume = {17},
year = {1983}
}
@incollection{Huang2016,
author = {Huang, Daniel and Morrisett, Greg},
booktitle = {Program. Lang. Syst. ESOP 2016},
doi = {10.1007/978-3-662-49498-1_14},
editor = {Thiemann, Peter},
isbn = {978-3-662-49497-4},
keywords = {probabilistic programs},
pages = {337--363},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages},
volume = {9632},
year = {2016}
}
@article{Kelly2016,
author = {Kelly, Kevin T. and Genin, Konstantin and Lin, Hanti},
doi = {10.1007/s11229-015-0993-9},
issn = {15730964},
journal = {Synthese},
keywords = {Epistemic justification,Learning,Ockham's Razor,Simplicity,Testability,Topology},
number = {4},
pages = {1191--1223},
publisher = {Springer Netherlands},
title = {Realism, rhetoric, and reliability},
volume = {193},
year = {2016}
}
@incollection{Simon1993,
author = {Simon, Imre},
booktitle = {Proc. 20th Conf. Math. Found. Program. Semant.},
doi = {10.1007/3-540-56939-1_92},
editor = {Lingas, Andrzej and Karlsson, Rolf and Carlsson, Svante},
pages = {430--444},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {The product of rational languages},
year = {1993}
}
@article{Shafer2016,
abstract = {The book that launched the Dempster–Shafer theory of belief functions appeared 40 years ago. This intellectual autobiography looks back on how I came to write the book and how its ideas played out in my later work.},
author = {Shafer, Glenn},
doi = {10.1016/j.ijar.2016.07.009},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Belief functions,Causality,Dempster–Shafer theory,Game-theoretic probability},
number = {November 1946},
pages = {7--25},
publisher = {Elsevier Inc.},
title = {A Mathematical Theory of Evidence turns 40},
volume = {79},
year = {2016}
}
@book{Schneider2010,
abstract = {The CSP approach has been widely used in the specification, analysis and verification of concurrent and real-time systems, and for understanding the particular issues that can arise when concurrency is present. It provides a language which enables specifications and designs to be clearly expressed and understood, together with a supporting theory which allows them to be analyzed and shown to be correct. This book supports advanced level courses on concurrency covering timed and untimed CSP. The first half introduces the language of CSP, the primary semantic models (traces, failures, divergences and infinite traces), and their use in the modelling, analysis and verification of concurrent systems. The second half of the book introduces time into the language, brings in the timed semantic model (timed failures) and finally presents the theory of timewise refinement which links the two halves together. Accompanying website: http://www.cs.rhbnc.ac.uk/books/concurrency Containing the following: -Exercises and solutions -Instructors resources - Example CSP programs to run on FDR and ProBe},
author = {Schneider, Steve},
pages = {526},
title = {Concurrent and Real-time Systems: The CSP Approach},
year = {2000}
}
@article{Isbell1963,
author = {Isbell, John R.},
journal = {Fund. Math.},
pages = {43--49},
title = {Two set-theoretical theorems in categories},
volume = {53},
year = {1963}
}
@incollection{Kuzu2011,
abstract = {For over fifty years, “record linkage” procedures have been refined to integrate data in the face of typographical and semantic errors. These procedures are traditionally performed over personal identifiers (e.g., names), but in modern decentralized environments, privacy concerns have led to regulations that require the obfuscation of such attributes. Various techniques have been proposed to resolve the tension, including secure multi-party computation protocols, however, such protocols are computationally intensive and do not scale for real world linkage scenarios. More recently, procedures based on Bloom filter encoding (BFE) have gained traction in various applications, such as healthcare, where they yield highly accurate record linkage results in a reasonable amount of time. Though promising, no formal security analysis has been designed or applied to this emerging model, which is of concern considering the sensitivity of the corresponding data. In this paper, we introduce a novel attack, based on constraint satisfaction, to provide a rigorous analysis for BFE and guidelines regarding how to mitigate risk against the attack. In addition, we conduct an empirical analysis with data derived from public voter records to illustrate the feasibility of the attack. Our investigations show that the parameters of the BFE protocol can be configured to make it relatively resilient to the proposed attack without significant reduction in record linkage performance.},
author = {Kuzu, Mehmet and Kantarcioglu, Murat and Durham, Elizabeth and Malin, Bradley},
booktitle = {Priv. Enhancing Technol. PETS 2011},
doi = {10.1007/978-3-642-22263-4_13},
editor = {Fischer-H{\"{u}}bner, Simone and Hopper, Nicholas},
pages = {226--245},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A constraint satisfaction cryptanalysis of bloom filters in private record linkage},
volume = {6794},
year = {2011}
}
@inproceedings{Altenkirch2009,
abstract = {We show that the syntactically rich notion of inductive families can be reduced to a core type theory with a fixed number of type constructors exploiting the novel notion of indexed containers. Indexed containers generalize simple containers, capturing strictly positive families instead of just strictly positive types, without having to extend the core type theory. Other applications of indexed containers include data type-generic programming and reasoning about polymorphic functions. The construction presented here has been formalized using the Agda system.},
author = {Altenkirch, Thorsten and Morris, Peter},
booktitle = {Log. Comput. Sci.},
doi = {10.1109/LICS.2009.33},
isbn = {9780769537467},
issn = {10436871},
keywords = {Functional programming,Type theory},
pages = {277--285},
title = {Indexed containers},
year = {2009}
}
@article{Hermida2011,
author = {Hermida, Claudio},
doi = {10.1016/j.ic.2010.09.009},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {bicategories of relations},
month = dec,
number = {12},
pages = {1505--1517},
publisher = {Elsevier Inc.},
title = {A categorical outlook on relational modalities and simulations},
volume = {209},
year = {2011}
}
@phdthesis{Bengtson2010,
abstract = {As the complexity of programs increase, so does the complexity of the models required to reason about them. Process calculi were introduced in the early 1980s and have since then been used to model communication protocols of varying size and scope. Whereas modeling sophisticated protocols in simple process algebras like CCS or the pi-calculus is doable, expressing the models required is often gruesome and error prone. To combat this, more advanced process calculi were introduced, which significantly reduce the complexity of the models. However, this simplicity comes at a price -- the theories of the calculi themselves instead become gruesome and error prone, and establishing their mathematical and logical properties has turned out to be difficult. Many of the proposed calculi have later turned out to be inconsistent.\n\nThe contribution of this thesis is twofold. Firstly we provide methodologies to formalise the meta-theory of process calculi in an interactive theorem prover. These are used to formalise significant parts of the meta-theory of CCS and the pi-calculus in the theorem prover Isabelle, using Nominal Logic to allow for a smooth treatment of the binders. Secondly we introduce and formalise psi-calculi, a framework for process calculi incorporating several existing ones, including those we already formalised, and which is significantly simpler and substantially more expressive. Our methods scale well as complexity of the calculi increases.\n\nThe formalised results include congruence results for both strong and weak bisimilarities, in the case of the pi-calculus for both the early and the late operational semantics. We also formalise the proof that the axiomatisation of strong late bisimilarity is sound and complete in the finite pi-calculus. We believe psi-calculi to be one of the most expressive frameworks for mobile process calculi, and our Isabelle formalisation to be the most extensive formalisation of process calculi ever done inside a theorem prover.},
author = {Bengtson, Jesper},
isbn = {9789155478018},
pages = {1--498},
school = {Uppsala Universitet},
title = {Formalising process calculi},
year = {2010}
}
@article{Banaschewski2006,
abstract = {In this paper we bring together results from a series of previous papers to prove the constructive version of the Gelfand duality theorem in any Grothendieck topos E, obtaining a dual equivalence between the category of commutative C∗-algebras and the category of compact, completely regular locales in the topos E.},
author = {Banaschewski, Bernhard and Mulvey, Christopher J.},
doi = {10.1016/j.apal.2005.05.018},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {18f99,46l99},
month = jan,
number = {1-3},
pages = {62--103},
title = {A globalisation of the Gelfand duality theorem},
volume = {137},
year = {2006}
}
@incollection{Johnstone1991,
abstract = {Preframes (directed complete posets with finite meets that distribute over the directed joins) are the algebras for an infinitary essentially algebraic theory, and can be presented by generators and relations. This result is combined with a general argument concerning categories of commutative monoids to give a very short proof of the localic Tychonoff Theorem. It is also shown how frames can be presented as preframes, a result analogous to Johnstone's construction of frames from sites, and an application is given.},
author = {Johnstone, Peter T. and Vickers, Steven},
booktitle = {Categ. Theory},
doi = {10.1007/BFb0084221},
editor = {Carboni, Aurelio and Pedicchio, Maria and Rosolini, Guiseppe},
pages = {193--212},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Preframe presentations present},
year = {1991}
}
@incollection{Bonsangue2013,
address = {Warsaw},
author = {Bonsangue, Marcello M. and Hansen, Helle Hvid and Kurz, Alexander and Rot, Jurriaan},
booktitle = {5th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-40206-7_9},
editor = {Heckel, Reiko and Milius, Stefan},
isbn = {978-3-642-40205-0},
number = {639},
pages = {95--109},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Presenting Distributive Laws},
year = {2013}
}
@misc{Wells2009,
author = {Wells, Charles},
month = sep,
title = {Sketches: Outline with References},
url = {http://www.cwru.edu/artsci/math/wells/pub/papers.html},
year = {2009}
}
@article{Goguen1977,
author = {Goguen, J. A. and Thatcher, J. W. and Wagner, E. G. and Wright, Jesse B.},
doi = {10.1145/321992.321997},
issn = {00045411},
journal = {J. ACM},
keywords = {algebras,and phrases algebraic semantics,continuous algebras,flow diagrams,free algebras,grammmg language semantics,posets,pro-,solutions of equations,syntax directed translation},
month = jan,
number = {1},
pages = {68--95},
title = {Initial Algebra Semantics and Continuous Algebras},
volume = {24},
year = {1977}
}
@article{Haghverdi2006,
abstract = {We consider the multiplicative and exponential fragment of linear logic (MELL) and give a geometry of interaction (GoI) semantics for it based on unique decomposition categories. We prove a soundness and finiteness theorem for this interpretation. We show that Girard's original approach to GoI 1 via operator algebras is exactly captured in this categorical framework. {\textcopyright} 2005 Elsevier B.V. All rights reserved.},
author = {Haghverdi, Esfandiar and Scott, Philip},
doi = {10.1016/j.tcs.2005.10.028},
isbn = {0304-3975},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Geometry of interaction,Linear logic,Partially additive categories,Traced monoidal categories,Unique decomposition categories},
month = feb,
number = {2-3},
pages = {252--274},
title = {A categorical model for the geometry of interaction},
volume = {350},
year = {2006}
}
@article{Manes2010,
abstract = {Let T be a submonad of the ultrafilter monad ?? and let G be a subfunctor of the filter functor. The T-algebras are topological spaces whose closed sets are the subalgebras and form thereby an equationally definable full subcategory of topological spaces. For appropriate T, countably generated free algebras provide ZFC examples of separable, Urysohn, countably compact, countably tight spaces which are neither compact nor sequential, and 2c non-homeomorphic such examples exist. For any space X, say that U ??? X is G-open if U belongs to every ultrafilter in GX which converges in U. The full subcategory TopG consists of all G-spaces, those spaces in which every G-open set is open. Each TopG has at least these stability properties: it contains all Alexandroff spaces, and is closed under coproducts, quotients and locally closed subspaces. Examples include sequential spaces, P-spaces and countably tight spaces. T-algebras are characterized as the T-compact, T-Hausdorff T-spaces. Malyhin's theorem on countable tightness generalizes verbatim to TopG for any G ??? ??. For r??? ??{star operator} = ?? ?? \ ??, let Gr be the subfunctor of ?? generated by r and let Tr be the generated submonad. If ???RK is the Rudin-Keisler preorder on ??{star operator}, r ???RK s ??? Gr ??? Gs. Let ???c be the Comfort preorder and define the monadic preorderr ???m s to mean Tr ??? Ts. Then r ???RK s ??? r ???m s ??? r ???c s. It follows that there exist 2c monadic types. For each such type Tr, the Tr-algebras form an equationally definable full subcategory of topological spaces with only one operation of countably infinite arity. No two of these varieties are term equivalent nor is any one a full subcategory of another inside topological spaces. Say that r ??? ??{star operator} is an m-point if Gr ??? Tr. Under CH, m-points exist. ?? 2009 Elsevier B.V. All rights reserved.},
author = {Manes, Ernie},
doi = {10.1016/j.topol.2009.12.013},
issn = {01668641},
journal = {Topol. Appl.},
keywords = {Rudin-Keisler and Comfort preorders,Ultrafilter monad,r-Compactness},
number = {5},
pages = {961--989},
publisher = {Elsevier B.V.},
title = {Monads in topology},
volume = {157},
year = {2010}
}
@inproceedings{Dankar2012,
address = {New York, New York, USA},
author = {Dankar, Fida Kamal and {El Emam}, Khaled},
booktitle = {Proc. 2012 Jt. EDBT/ICDT Work. - EDBT-ICDT '12},
doi = {10.1145/2320765.2320816},
isbn = {9781450311434},
keywords = {anonymity,de-identification,differential privacy,microdata},
pages = {158},
publisher = {ACM Press},
title = {The application of differential privacy to health data},
year = {2012}
}
@inproceedings{Levy2015,
author = {Levy, Paul Blain},
booktitle = {Proc. 6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.221},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
isbn = {978-3-939897-84-2},
keywords = {and phrases coalgebra,bisimulation,category theory,factorization sys-,modal logic},
pages = {221----237},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Final coalgebras from corecursive algebras},
year = {2015}
}
@inproceedings{Benton2010,
address = {Dagstuhl, Germany},
author = {Benton, Nick and Hur, Chung-Kil},
booktitle = {Model. Control. Reason. About State},
editor = {Ahmed, Amal and Benton, Nick and Birkedal, Lars and Hofmann, Martin},
issn = {1862-4405},
number = {10351},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
series = {Dagstuhl Seminar Proceedings},
title = {Step-Indexing: The Good, the Bad and the Ugly},
year = {2010}
}
@article{Society1988,
abstract = {A causal network is used in a number of areas as a depiction of patterns of `influence' among sets of variables. In expert systems it is common to perform `inference' by means of local computations on such large but sparse networks. In general, non-probabilistic methods are used to handle uncertainty when propagating the effects of evidence, and it has appeared that exact probabilistic methods are not computationally feasible. Motivated by an application in electromyography, we counter this claim by exploiting a range of local representations for the joint probability distribution, combined with topological changes to the original network termed `marrying' and `filling-in'. The resulting structure allows efficient algorithms for transfer between representations, providing rapid absorption and propagation of evidence. The scheme is first illustrated on a small, fictitious but challenging example, and the underlying theory and computational aspects are then discussed.},
author = {Lauritzen, S. L. and Spiegelhalter, D. J.},
doi = {10.2307/2345762},
isbn = {00359246},
issn = {0035-9246},
journal = {J. R. Stat. Soc.},
number = {2},
pages = {157--224},
title = {Local Computations with Probabilities on Graphical Structures and Their Application to Expert Systems},
volume = {50},
year = {1988}
}
@article{Bouyer2010,
author = {Bouyer, Patricia and Cassez, Franck and Laroussinie, Fran{\c{c}}ois},
doi = {10.1007/s10849-010-9127-4},
isbn = {1084901091274},
issn = {0925-8531},
journal = {J. Logic, Lang. Inf.},
keywords = {model checking,timed automata,timed modal logic},
month = apr,
number = {2},
pages = {169--203},
title = {Timed modal logics for real-time systems},
volume = {20},
year = {2011}
}
@misc{Lawvere1962,
author = {Lawvere, F William},
title = {The Category of Probabilistic Mappings},
url = {https://plus.google.com/+VenkataRayuduPosina/posts/KJ69q62PzQM},
year = {1962}
}
@book{Davey2002a,
author = {Davey, Brian A. and Priestley, Hilary A.},
edition = {2},
isbn = {0521784514},
month = apr,
publisher = {Cambridge University Press},
title = {Introduction to Lattices and Order},
type = {Book},
year = {2002}
}
@article{Adamek2008,
abstract = {For accessible set-valued functors it is well known that weak preservation of limits is equivalent to representability, and weak preservation of connected limits to familial representability. In contrast, preservation of weak wide pullbacks is equivalent to being a coproduct of quotients of hom-functors modulo groups of automorphisms. For ﬁnitary functors this was proved by Andr´e Joyal who called these functors analytic. We introduce a generalization of Joyal's concept from endofunctors of Set to endofunctors of a symmetric monoidal category.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Velebil, Jiř{\'{i}}},
journal = {Theory Appl. Categ.},
number = {11},
pages = {191--209},
title = {Analytic functors and weak pullbacks},
volume = {21},
year = {2008}
}
@book{Libkin2004,
address = {Berlin, Heidelberg},
author = {Libkin, Leonid},
doi = {10.1007/978-3-662-07003-1},
isbn = {978-3-642-05948-3},
pages = {318},
publisher = {Springer Berlin Heidelberg},
series = {Texts in Theoretical Computer Science},
title = {Elements of Finite Model Theory},
year = {2004}
}
@article{Kelly2000,
author = {Kelly, Gregory Maxwell and Lack, Stephen},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Categories with limits,Enriched categories,Monadicity,Weighted limits},
number = {7},
pages = {148--170},
title = {On the monadicity of categories with chosen colimits},
volume = {7},
year = {2000}
}
@article{Schroder2011,
author = {Schr{\"{o}}der, Lutz and Pattinson, Dirk},
doi = {10.1017/S0960129510000563},
isbn = {0960129510},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
number = {02},
pages = {235--266},
title = {Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra},
volume = {21},
year = {2011}
}
@inproceedings{Enqvist2016,
author = {Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
booktitle = {25th EACSL Annu. Conf. Comput. Sci. Log.},
doi = {10.4230/LIPIcs.CSL.2016.7},
editor = {Talbot, Jean-Marc and Regnier, Laurent},
isbn = {978-3-95977-022-4},
issn = {1868-8969},
keywords = {2016,4230,7,and phrases µ -calculus,automata,coalgebra,coalgebraic modal logic,completeness,csl,digital object identifier 10,lipics},
pages = {7:1--7:19},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Completeness for coalgebraic fixpoint logic},
volume = {62},
year = {2016}
}
@incollection{Plotkin2002,
abstract = {We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational effects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship.},
author = {Plotkin, Gordon D. and Power, John},
booktitle = {Proc. 5th Int. Conf. Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/3-540-45931-6_24},
editor = {Nielsen, Mogens and Engberg, Uffe},
isbn = {978-3-540-45931-6},
pages = {342--356},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Notions of Computation Determine Monads},
year = {2002}
}
@article{Bruse2014,
abstract = {Guarded normal form requires occurrences of fixpoint variables in a {\mu}-calculus-formula to occur under the scope of a modal operator. The literature contains guarded transformations that effectively bring a {\mu}-calculus-formula into guarded normal form. We show that the known guarded transformations can cause an exponential blowup in formula size, contrary to existing claims of polynomial behaviour. We also show that any polynomial guarded transformation for {\mu}-calculus-formulas in the more relaxed vectorial form gives rise to a polynomial solution algorithm for parity games, the existence of which is an open problem. We also investigate transformations between the {\mu}-calculus, vectorial form and hierarchical equation systems, which are an alternative syntax for alternating parity tree automata.},
archivePrefix = {arXiv},
arxivId = {1305.0648},
author = {Bruse, Florian and Friedmann, Oliver and Lange, Martin},
doi = {10.1093/jigpal/jzu030},
eprint = {1305.0648},
issn = {1367-0751},
journal = {Log. J. IGPL},
keywords = {Modal equation systems,Modal $\mu$-calculus,Parity games,guarded transformation},
month = apr,
number = {2},
pages = {194--216},
title = {On guarded transformation in the modal $\mu$-calculus},
volume = {23},
year = {2015}
}
@book{Howes1995,
author = {Howes, Norman R.},
doi = {10.1007/978-1-4612-0833-4},
isbn = {0387979867},
publisher = {Springer New York},
series = {Universitext},
title = {Modern Analysis and Topology},
year = {1995}
}
@article{Wang2012,
abstract = {We present a theoretical framework for the analysis of privacy and security tradeoffs in secure biometric authentication systems. We use this framework to conduct a comparative information-theoretic analysis of two biometric systems that are based on linear error correction codes, namely fuzzy commitment and secure sketches. We derive upper bounds for the probability of false rejection ($P_{FR}$) and false acceptance ($P_{FA}$) for these systems. We use mutual information to quantify the information leaked about a user's biometric identity, in the scenario where one or multiple biometric enrollments of the user are fully or partially compromised. We also quantify the probability of successful attack ($P_{SA}$) based on the compromised information. Our analysis reveals that fuzzy commitment and secure sketch systems have identical $P_{FR}, P_{FA}, P_{SA}$ and information leakage, but secure sketch systems have lower storage requirements. We analyze both single-factor (keyless) and two-factor (key-based) variants of secure biometrics, and consider the most general scenarios in which a single user may provide noisy biometric enrollments at several access control devices, some of which may be subsequently compromised by an attacker. Our analysis highlights the revocability and reusability properties of key-based systems and exposes a subtle design tradeoff between reducing information leakage from compromised systems and preventing successful attacks on systems whose data have not been compromised.},
archivePrefix = {arXiv},
arxivId = {1112.5630},
author = {Wang, Ye and Rane, Shantanu and Draper, Stark C. and Ishwar, Prakash},
doi = {10.1109/TIFS.2012.2210215},
eprint = {1112.5630},
issn = {1556-6013},
journal = {IEEE Trans. Inf. Forensics Secur.},
keywords = {Biometrics,fuzzy commitment,information leakage,privacy,reusability,revocability,secure sketch,security},
month = dec,
number = {6},
pages = {1825--1840},
title = {A Theoretical Analysis of Authentication, Privacy, and Reusability Across Secure Biometric Systems},
volume = {7},
year = {2012}
}
@article{Arieli1998,
author = {Arieli, Ofer and Avron, Arnon},
doi = {10.1016/S0004-3702(98)00032-0},
isbn = {9780977858231},
issn = {00043702},
journal = {Artif. Intell.},
keywords = {bilattices,multiple-valued systems,paraconsistency,preferential logics,reasoning},
month = jun,
number = {1},
pages = {97--141},
title = {The value of the four values},
volume = {102},
year = {1998}
}
@incollection{Boyd1994,
abstract = {In the past few years a lot of attention has been paid to the use of special logics to analyse cryptographic protocols, foremost among these being the logic of Burrows, Abadi and Needham (the BAN logic). These logics have been successful in finding weaknesses in various examples. In this paper a limitation of the BAN logic is illustrated with two examples. These show that it is easy for the BAN logic to approve protocols that are in practice unsound.},
address = {Berlin, Heidelberg},
author = {Boyd, Colin and Mao, Wenbo},
booktitle = {Adv. Cryptol. — EUROCRYPT '93},
doi = {10.1

license_type: permissive

branch_name: refs/heads/master

extension: bib