text:
Phys.},
month = dec,
number = {1},
pages = {258--280},
title = {Bereiche zweiter Ordnung},
type = {Journal article},
volume = {32},
year = {1922}
}
@article{Dimov1993,
author = {Dimov, Georgi D. and Tholen, Walter},
journal = {Trans. Am. Math. Soc.},
number = {2},
pages = {901--913},
title = {Groups of dualities},
volume = {336},
year = {1993}
}
@article{DeVink1999,
author = {de Vink, Erik P. and Rutten, Jan J.M.M.},
doi = {10.1016/S0304-3975(99)00035-3},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {bisimulation,borel measures,coalgebras,final coalgebra,probabilistic transition systems,ultrametric spaces},
month = jun,
number = {1-2},
pages = {271--293},
title = {Bisimulation for probabilistic transition systems: a coalgebraic approach},
volume = {221},
year = {1999}
}
@article{Shulman2013,
abstract = {We develop a theory of categories which are simultaneously (1) indexed over a base category $S$ with finite products, and (2) enriched over an $S$-indexed monoidal category $V$. This includes classical enriched categories, indexed and fibered categories, and internal categories as special cases. We then describe the appropriate notion of ``limit'' for such enriched indexed categories, and show that they admit ``free cocompletions'' constructed as usual with a Yoneda embedding.},
author = {Shulman, Michael A.},
journal = {Theory Appl. Categ.},
keywords = {enriched category,fibered category,indexed category,monoidal category},
number = {21},
pages = {616--695},
title = {Enriched indexed categories},
volume = {28},
year = {2013}
}
@article{Domingo-Ferrer2018,
abstract = {We explore some novel connections between the main privacy models in use and we recall a few known ones. We show these models to be more related than commonly understood, around two main principles: deniability and permutation. In particular, randomized response turns out to be very modern in spite of it having been introduced over 50 years ago: it is a local anonymization method and it allows understanding the protection offered by $\epsilon$-differential privacy when $\epsilon$ is increased to improve utility. A similar understanding on the effect of large $\epsilon$ in terms of deniability is obtained from the connection between $\epsilon$-differential privacy and t-closeness. Finally, the post-randomization method (PRAM) is shown to be viewable as permutation and to be connected with randomized response and differential privacy. Since the latter is also connected with t-closeness, it follows that the permutation principle can explain the guarantees offered by all those models. Thus, calibrating permutation is very relevant in anonymization, and we conclude by sketching two ways of doing it.},
archivePrefix = {arXiv},
arxivId = {1803.02139},
author = {Domingo-Ferrer, Josep and Soria-Comas, Jordi},
eprint = {1803.02139},
keywords = {Differential privacy,PRAM,permutation paradigm,randomized response,risk and loss aversion,t-closeness},
month = mar,
title = {Connecting Randomized Response, Post-Randomization, Differential Privacy and t-Closeness via Deniability and Permutation},
year = {2018}
}
@article{Hofmann2012,
abstract = {In this paper we present methods of transition from one perspective on logic to others, and apply this in particular to obtain a coalgebraic presentation of logic. The central ingredient in this process is to view consequence relations as morphisms in a category.},
archivePrefix = {arXiv},
arxivId = {1202.0915},
author = {Hofmann, Dirk and Martins, Manuel A.},
eprint = {1202.0915},
month = feb,
title = {On a coalgebraic view on Logic},
year = {2012}
}
@article{Kamide2002a,
abstract = {We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, M{\'{e}}ndez's logics and relevant logics.},
author = {Kamide, Norihiro},
doi = {10.1023/A:1019915908844},
journal = {J. Logic, Lang. Inf.},
keywords = {completeness theorem,kripke semantics,linear logic,modal substructural logic,rele-},
pages = {453--470},
title = {Kripke Semantics for Modal Substructural Logics},
volume = {4},
year = {2002}
}
@incollection{Pavlovic2014,
author = {Pavlovi{\'{c}}, Dusko},
booktitle = {Categ. Types Logic, Lang. Phys.},
doi = {10.1007/978-3-642-54789-8_19},
editor = {Casadio, Claudia and Coecke, Bob and Moortgat, Michael and Scott, Philip},
pages = {353--367},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Chasing Diagrams in Cryptography},
year = {2014}
}
@article{Tschantz2011,
abstract = {Differential privacy is a promising approach to privacy preserving data analysis with a well-developed theory for functions. Despite recent work on implementing systems that aim to provide differential privacy, the problem of formally verifying that these systems have differential privacy has not been adequately addressed. We develop a formal probabilistic automaton model of differential privacy for systems by adapting prior work on differential privacy for functions. We present the first sound verification technique for proving differential privacy of interactive systems. The technique is based on a form of probabilistic bisimulation relation. The novelty lies in the way we track quantitative privacy leakage bounds using a relation family instead of a single relation. We illustrate the proof technique on a representative automaton motivated by PINQ, an implemented system that is intended to provide differential privacy. Surprisingly, our analysis yields a privacy leakage bound of (2t* ??) rather than (t* ??) when ??differentially private functions are called t times. The extra leakage arises from accounting for bounded memory constraints of real computers. ?? 2011 Elsevier B.V.All rights reserved.},
author = {Tschantz, Michael Carl and Kaynar, Dilsun and Datta, Anupam},
doi = {10.1016/j.entcs.2011.09.015},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Bisimulation,Differential Privacy,Formal Methods,Privacy,Verification},
number = {1},
pages = {61--79},
publisher = {Elsevier B.V.},
title = {Formal verification of differential privacy for interactive systems (extended abstract)},
volume = {276},
year = {2011}
}
@inproceedings{Gibbons2012,
author = {Gibbons, Jeremy},
booktitle = {UTP Symp.},
month = aug,
title = {Unifying Theories of Programming with Monads},
year = {2012}
}
@article{Kelly1982a,
author = {Kelly, Gregory Maxwell},
journal = {Cah. Topol. G{\'{e}}om. Diff{\'{e}}rentielle},
number = {1},
pages = {3--42},
title = {Structures defined by finite limits in the enriched context, I},
volume = {23},
year = {1982}
}
@book{Axler2006,
author = {Rautenberg, Wolfgang},
doi = {10.1007/0-387-34241-9},
isbn = {978-0-387-30294-2},
publisher = {Springer New York},
series = {Universitext},
title = {A Concise Introduction to Mathematical Logic},
year = {2006}
}
@incollection{Emerson1994,
abstract = {We give a comprehensive and unifying survey of the theoretical aspects of Temporal and Modal Logic.},
author = {Emerson, E. Allen},
booktitle = {Handb. Theor. Comput. Sci.},
editor = {van Leeuwen, J.},
isbn = {9780262220392},
pages = {995--1072},
publisher = {MIT Press},
title = {Temporal and modal logic},
volume = {B},
year = {1990}
}
@book{hottbook,
address = {Institute for Advanced Study},
author = {{Univalent Foundations Program}, The},
publisher = {\url{http://homotopytypetheory.org/book}},
title = {Homotopy Type Theory: Univalent Foundations of Mathematics},
year = {2013}
}
@article{Edwards2017,
abstract = {ABSTRACT This article reflects the kinds of situations and spaces where people and algorithms meet. In what situations do people become aware of algorithms? How do they experience and make sense of these algorithms, given their often hidden and invisible nature? To what extent does an awareness of algorithms affect people's use of these platforms, if at all? To help answer these questions, this article examines people's personal stories about the Facebook algorithm through tweets and interviews with 25 ordinary users. To understand the spaces where people and algorithms meet, this article develops the notion of the algorithmic imaginary. It is argued that the algorithmic imaginary – ways of thinking about what algorithms are, what they should be and how they function – is not just productive of different moods and sensations but plays a generative role in moulding the Facebook algorithm itself. Examining how algorithms make people feel, then, seems crucial if we want to understand their social power.},
author = {Edwards, Lilian and Veale, Michael},
doi = {10.2139/ssrn.2972855},
isbn = {3540445668},
issn = {1556-5068},
journal = {SSRN Electron. J.},
keywords = {International},
title = {Slave to the Algorithm? Why a Right to Explanationn is Probably Not the Remedy You are Looking for},
volume = {2017},
year = {2017}
}
@book{Doberkat2009a,
address = {Berlin, Heidelberg},
author = {Doberkat, Ernst-Erich},
doi = {10.1007/978-3-642-02995-0},
isbn = {978-3-642-02994-3},
publisher = {Springer Berlin Heidelberg},
series = {Monographs in Theoretical Computer Science},
title = {Stochastic Coalgebraic Logic},
year = {2009}
}
@inproceedings{Fiore1999,
address = {Trento},
author = {Fiore, Marcelo P. and Plotkin, Gordon D. and Turi, Daniele},
booktitle = {Proceedings. 14th Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.1999.782615},
isbn = {0-7695-0158-3},
pages = {193--202},
publisher = {IEEE Comput. Soc},
title = {Abstract syntax and variable binding},
year = {1999}
}
@article{Codd1970,
abstract = {Predicting the binding mode of flexible polypeptides to proteins is an important task that falls outside the domain of applicability of most small molecule and protein−protein docking tools. Here, we test the small molecule flexible ligand docking program Glide on a set of 19 non-$\alpha$-helical peptides and systematically improve pose prediction accuracy by enhancing Glide sampling for flexible polypeptides. In addition, scoring of the poses was improved by post-processing with physics-based implicit solvent MM- GBSA calculations. Using the best RMSD among the top 10 scoring poses as a metric, the success rate (RMSD ≤ 2.0 {\AA} for the interface backbone atoms) increased from 21% with default Glide SP settings to 58% with the enhanced peptide sampling and scoring protocol in the case of redocking to the native protein structure. This approaches the accuracy of the recently developed Rosetta FlexPepDock method (63% success for these 19 peptides) while being over 100 times faster. Cross-docking was performed for a subset of cases where an unbound receptor structure was available, and in that case, 40% of peptides were docked successfully. We analyze the results and find that the optimized polypeptide protocol is most accurate for extended peptides of limited size and number of formal charges, defining a domain of applicability for this approach.},
author = {Codd, E. F.},
doi = {10.1145/362384.362685},
journal = {Commun. ACM},
keywords = {icle},
number = {6},
pages = {377--387},
title = {A relational model of data for large shared data banks},
volume = {13},
year = {1970}
}
@incollection{Jay1991,
author = {Jay, C. Barry},
booktitle = {Proc. IV High. Order Work.},
doi = {10.1007/978-1-4471-3182-3_10},
editor = {Birtwistle, Graham},
pages = {151--161},
publisher = {Springer, London},
title = {Partial functions, ordered categories, limits and cartesian closure},
year = {1991}
}
@book{Hedman2004,
author = {Hedman, Shawn},
isbn = {978-0-19-852981-1},
month = jul,
pages = {452},
publisher = {Oxford University Press},
series = {Oxford Texts in Logic},
title = {A First Course in Logic: An Introduction to Model Theory, Proof Theory, Computability, and Complexity},
year = {2004}
}
@book{Jacobs1999,
abstract = {This book is an attempt to give a systematic presentation of both logic and type theory from a categorical perspective, using the unifying concept of fibred category. Its intended audience consists of logicians, type theorists, category theorists and (theoretical) computer scientists.},
address = {Amsterdam},
author = {Jacobs, Bart},
isbn = {0-444-50170-3},
pages = {784},
publisher = {North Holland},
series = {Studies in Logic and the Foundations of Mathematics},
title = {Categorical Logic and Type Theory},
year = {1999}
}
@article{Wyler1973,
author = {Wyler, Oswald},
doi = {10.1016/0016-660X(72)90014-1},
issn = {0016660X},
journal = {Gen. Topol. its Appl.},
month = sep,
number = {3},
pages = {225--242},
title = {Convenient categories for topology},
volume = {3},
year = {1973}
}
@article{Moss2006,
author = {Moss, Lawrence S. and Viglizzo, Ignacio Dario},
doi = {10.1016/j.ic.2005.04.006},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {coalgebra,final coalgebra,measurable space,modal logic,probability measure},
month = apr,
number = {4},
pages = {610--636},
title = {Final coalgebras for functors on measurable spaces},
volume = {204},
year = {2006}
}
@book{Approach2014,
address = {Cham},
author = {Nipkow, Tobias and Klein, Gerwin},
doi = {10.1007/978-3-319-10542-0},
isbn = {978-3-319-10541-3},
publisher = {Springer International Publishing},
title = {Concrete Semantics},
year = {2017}
}
@article{McSherry2010,
abstract = {We report on the design and implementation of the Privacy Integrated Queries (PINQ) platform for privacy-preserving data analysis. PINQ provides analysts with a programming interface to unscrubbed data through a SQL-like language. At the same time, the design of PINQ's analysis language and its careful implementation provide formal guarantees of differential privacy for any and all uses of the platform. PINQ's unconditional structural guarantees require no trust placed in the expertise or diligence of the analysts, substantially broadening the scope for design and deployment of privacy-preserving data analysis, especially by non-experts.},
author = {McSherry, Frank},
doi = {10.1145/1810891.1810916},
isbn = {9781605585512},
issn = {00010782},
journal = {Commun. ACM},
keywords = {anonymization,confidentiality,differential privacy,linq},
month = sep,
number = {9},
pages = {89},
title = {Privacy integrated queries},
volume = {53},
year = {2010}
}
@article{Salehi2007,
abstract = {We consider several aspects of Wilke's [T. Wilke, An algebraic characterization of frontier testable tree languages, Theoret. Comput. Sci. 154 (1996) 85-106] tree algebra formalism for representing binary labelled trees and compare it with approaches that represent trees as terms in the traditional way. A convergent term rewriting system yields normal form representations of binary trees and contexts, as well as a new completeness proof and a computational decision method for the axiomatization of tree algebras. Varieties of binary tree languages are compared with varieties of tree languages studied earlier in the literature. We also prove a variety theorem thus solving a problem noted by several authors. Syntactic tree algebras are studied and compared with ordinary syntactic algebras. The expressive power of the language of tree algebras is demonstrated by giving equational definitions for some well-known varieties of binary tree languages. ?? 2007 Elsevier Ltd. All rights reserved.},
author = {Salehi, Saeed and Steinby, Magnus},
doi = {10.1016/j.tcs.2007.02.006},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Binary trees,Syntactic tree algebras,Tree algebras,Tree automata,Tree languages,Varieties of tree languages},
month = may,
number = {1-3},
pages = {1--24},
title = {Tree algebras and varieties of tree languages},
volume = {377},
year = {2007}
}
@article{Kifer2012,
abstract = {" Privacy " and " utility " are words that frequently appear in the lit-erature on statistical privacy. But what do these words really mean? In recent years, many problems with intuitive notions of privacy and utility have been un-covered. Thus more formal notions of privacy and utility, which are amenable to mathematical analysis, are needed. In this paper we present our initial work on an axiomatization of privacy and utility. We present two privacy axioms which describe how privacy is affected by both post-processing data and by randomly se-lecting a privacy mechanism. We present three axioms for utility measures which also describe how measured utility is affected by post-processing. Our analysis of these axioms yields new insights into the construction of privacy definitions and utility measures. In particular, we characterize the class of relaxations of differ-ential privacy that can be obtained by changing constraints on probabilities; we show that the resulting constraints must be formed from concave functions. We also present several classes of utility metrics satisfying our axioms and explicitly show that measures of utility borrowed from statistics can lead to utility paradoxes when applied to statistical privacy. Finally, we show that the outputs of differ-entially private algorithms are best interpreted in terms of graphs or likelihood functions rather than query answers or synthetic data.},
author = {Kifer, Daniel and Lin, Bing-Rong},
journal = {J. Priv. Confidentiality},
number = {1},
pages = {5--49},
title = {An Axiomatic View of Statistical Privacy and Utility},
volume = {4},
year = {2012}
}
@book{James1999,
author = {James, Ioan},
booktitle = {Numer. Methods Partial Differ. Equ.},
doi = {10.1007/978-1-4471-3994-2},
isbn = {9781846280405},
publisher = {Springer London},
series = {Springer Undergraduate Mathematics Series},
title = {Topologies and Uniformities},
volume = {79},
year = {1999}
}
@article{Maurice2006,
author = {Maurice, K. and {Celestin Nkuimi}, J.},
doi = {10.1155/IJMMS/2006/56786},
journal = {Int. J. Math. Math. Sci.},
pages = {9},
publisher = {Hindawi Publishing Corporation},
title = {A simplification functor for coalgebras},
type = {Journal article},
volume = {2006},
year = {2006}
}
@misc{Riehl2008,
address = {Chicago},
author = {Riehl, Emily},
title = {Factorization systems},
year = {2008}
}
@incollection{Pfenning2002,
author = {Pfenning, Frank},
booktitle = {Proof Syst.},
doi = {10.1007/978-94-010-0413-8_5},
editor = {Schwichtenberg, Helmut and Steinbr{\"{u}}ggen, Ralf},
keywords = {logical frameworks,type theory},
pages = {137--166},
publisher = {Springer Netherlands},
series = {NATO Science Series},
title = {Logical Frameworks—A Brief Introduction},
year = {2002}
}
@article{Hughes1989,
author = {Hughes, J.},
doi = {10.1093/comjnl/32.2.98},
issn = {0010-4620},
journal = {Comput. J.},
month = feb,
number = {2},
pages = {98--107},
title = {Why Functional Programming Matters},
volume = {32},
year = {1989}
}
@article{Descotte2014,
archivePrefix = {arXiv},
arxivId = {1406.5762},
author = {Descotte, M. Emilia and Dubuc, Eduardo J.},
eprint = {1406.5762},
journal = {ArXiv e-prints},
month = jun,
pages = {1--33},
title = {A theory of 2-pro-objects (with expanded proofs)},
year = {2014}
}
@book{Comon2007,
author = {Comon, Hubert and Dauchet, Max and Gilleron, R{\'{e}}mi and Jacquemard, Florent and Lugiez, Denis and L{\"{o}}ding, Christof and Tison, Sophie and Tommasi, Marc},
pages = {262},
publisher = {Available on: \url{http://www.grappa.univ-lille3.fr/tata}},
title = {Tree Automata Techniques and Applications},
year = {2007}
}
@article{Kurz2010a,
author = {Kurz, Alexander and Palmigiano, Alessandra and Venema, Yde},
doi = {10.1093/logcom/exn094},
issn = {0955-792X},
journal = {J. Log. Comput.},
month = sep,
number = {5},
pages = {985--990},
title = {Coalgebra and Logic: A Brief Overview},
volume = {20},
year = {2010}
}
@article{Santocanale2003,
author = {Santocanale, Luigi},
doi = {10.1016/S0304-3975(02)00412-7},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {fixed point calculi,least {\"{y}}xed point,programs,semantics and logics of,temporal logic},
month = feb,
number = {1-3},
pages = {341--370},
title = {On the equational definition of the least prefixed point},
volume = {295},
year = {2003}
}
@book{Pouly2011,
address = {Hoboken, NJ, USA},
author = {Pouly, Marc and Kohlas, J{\"{u}}rg},
doi = {10.1002/9781118010877},
isbn = {9781118010877},
month = may,
pages = {484},
publisher = {John Wiley \& Sons, Inc.},
title = {Generic Inference},
year = {2011}
}
@incollection{Jacobs2010,
author = {Jacobs, Bart},
booktitle = {Proc. 6th IFIP TC 1/WG 2.2 Int. Conf.},
doi = {10.1007/978-3-642-15240-5_1},
editor = {Calude, Cristian S. and Sassone, Vladimiro},
number = {1},
pages = {1--19},
publisher = {Springer Berlin Heidelberg},
series = {IFIP Advances in Information and Communication Technology},
title = {Convexity, Duality and Effects},
year = {2010}
}
@article{Pastro2009,
abstract = {This paper determines what structure is needed for internal homs in a monoidal category C to be liftable to the category CG of Eilenberg-Moore coalgebras for a monoidal comonad G on C. We apply this to lift *-autonomy with the view to recasting the definition of quantum groupoid. ?? 2008 Elsevier Inc. All rights reserved.},
author = {Pastro, Craig and Street, Ross},
doi = {10.1016/j.jalgebra.2008.05.004},
isbn = {0021-8693},
issn = {00218693},
journal = {J. Algebr.},
keywords = {*-autonomy,Antipode,Bialgebroid,Closed category,Internal hom,Monad,Quantum groupoid},
month = jun,
number = {11},
pages = {3494--3520},
publisher = {Elsevier Inc.},
title = {Closed categories, star-autonomy, and monoidal comonads},
volume = {321},
year = {2009}
}
@incollection{Riba2015a,
author = {Riba, Colin},
booktitle = {13th Int. Conf. Typed Lambda Calc. Appl.},
doi = {10.4230/LIPIcs.TLCA.2015.302},
editor = {Altenkirch, Thorsten},
isbn = {978-3-939897-87-3},
keywords = {2015,302,4230,Categorical logic,Game semantics,Tree automata,and phrases tree automata,categorical logic,digital object identifier 10,game semantics,lipics,tlca},
pages = {302--316},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Fibrations of Tree Automata},
year = {2015}
}
@article{Doberkat2008,
author = {Doberkat, Ernst-Erich},
doi = {10.1016/j.apal.2008.01.010},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {1,behavioral equivalence,close cousins like the,coalgebraic and modal logic,coalgebras,hennessy,introduction and motivation,investigating equivalent behavior of,milner theorem,modal logics or their,model checking usually follows,partitioned into states that,predicate liftings,satisfy,stochastic kripke models for,stochastic relations,the state space is,this pattern,tree logics used for},
month = aug,
number = {1},
pages = {46--68},
title = {Stochastic coalgebraic logic: Bisimilarity and behavioral equivalence},
volume = {155},
year = {2008}
}
@incollection{Mir2013,
author = {Mir, Darakhshan J},
booktitle = {Found. Pract. Secur. FPS 2012},
doi = {10.1007/978-3-642-37119-6_25},
editor = {Tawbi, Joaquin Garcia-Alfaro and Cuppens, Fr{\'{e}}d{\'{e}}ric and Cuppens-Boulahia, Nora and MiriNadia, Ali},
pages = {374--381},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Information-Theoretic Foundations of Differential Privacy},
volume = {7743},
year = {2013}
}
@article{Morales1996,
author = {Morales, Domingo and Pardo, Leandro and Vajda, Igor},
doi = {10.1109/3468.541329},
issn = {10834427},
journal = {IEEE Trans. Syst. Man, Cybern. - Part A Syst. Humans},
number = {6},
pages = {681--697},
title = {Uncertainty of discrete stochastic systems: general theory and statistical inference},
volume = {26},
year = {1996}
}
@article{Bezhanishvili2010,
abstract = {Building on the fact that descriptive frames are coalgebras for the Vietoris functor on the category of Stone spaces, we introduce and study the concept of a Vietoris bisimulation between two descriptive modal models, together with the associated notion of bisimilarity. We prove that our notion of bisimilarity, which is defined in terms of relation lifting, coincides with Kripke bisimilarity (with respect to the underlying Kripke models), with behavioural equivalence, and with modal equivalence, but not with Aczel–Mendler bisimilarity. As a corollary, we obtain that the Vietoris functor does not preserve weak pullbacks. Comparing Vietoris bisimulations between descriptive models to Kripke bisimulations on the underlying Kripke models, we prove that the closure of such a Kripke bisimulation is a Vietoris bisimulation. As a corollary, we show that the collection of Vietoris bisimulations between two descriptive models forms a complete lattice. Finally, we provide a game-theoretic characterization of Vietoris bisimilarity.},
author = {Bezhanishvili, Nick and Fontaine, Ga{\"{e}}lle M.M. and Venema, Yde},
doi = {10.1093/logcom/exn091},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {Modal logic,Vietoris construction,bisimulation,coalgebra,descriptive frame},
month = oct,
number = {5},
pages = {1017--1040},
title = {Vietoris Bisimulations},
volume = {20},
year = {2010}
}
@article{Frankowski2006,
abstract = {Main investigations concerning Kripke models refer to two valued case. The papers devoted to many-valued modal logics do not contain even elementary theory of appropriate models. This paper provides very general notion of many valued Kripke model for every standard multimodality, and displays the suitable generalizations of the ideas known from the classical case: disjoint sum of Kripke models, bounded morphism (sometimes called p-morphism), bisimulation.},
author = {Frankowski, Szymon},
journal = {Bull. Sect. Log.},
number = {1},
pages = {11--26},
title = {General approach to many valued Kripke models},
volume = {35},
year = {2006}
}
@article{Awodey2012,
abstract = {Homotopy type theory is an interpretation of Martin-L\"of's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq. The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.},
archivePrefix = {arXiv},
arxivId = {1201.3898},
author = {Awodey, Steve and Gambino, Nicola and Sojakova, Kristina},
eprint = {1201.3898},
journal = {ArXiv e-prints},
month = jan,
pages = {19},
title = {Inductive types in homotopy type theory},
year = {2012}
}
@inproceedings{Milius2012,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Bowler, Nathan and Levy, Paul Blain},
booktitle = {2012 27th Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2012.16},
isbn = {978-1-4673-2263-8},
month = jun,
pages = {45--54},
publisher = {Ieee},
title = {Coproducts of Monads on Set},
year = {2012}
}
@misc{TheMendeleySupportTeam2011c,
abstract = {A quick introduction to Mendeley. Learn how Mendeley creates your personal digital library, how to organize and annotate documents, how to collaborate and share with colleagues, and how to generate citations and bibliographies.},
address = {London},
author = {{The Mendeley Support Team}},
booktitle = {Mendeley Deskt.},
keywords = {Mendeley,how-to,user manual},
pages = {1--16},
publisher = {Mendeley Ltd.},
title = {Getting Started with Mendeley},
url = {http://www.mendeley.com},
year = {2011}
}
@article{Bonchi2014,
author = {Bonchi, Filippo and Bonsangue, Marcello M. and Hansen, Helle Hvid and Panangaden, Prakash and Rutten, Jan J.M.M. and Silva, Alexandra},
doi = {10.1145/2490818},
issn = {15293785},
journal = {ACM Trans. Comput. Log.},
month = feb,
number = {1},
pages = {1--29},
title = {Algebra-coalgebra duality in brzozowski's minimization algorithm},
volume = {15},
year = {2014}
}
@book{Nordstrom1990,
author = {Nordstr{\"{o}}m, Bengt and Petersson, Kent and Smith, Jan M.},
booktitle = {Evaluation},
isbn = {9780198538141},
publisher = {Oxford University Press},
title = {Programming in Martin-L{\"{o}}f Type Theory: An Introduction},
year = {1990}
}
@article{Kurz2005,
author = {Kurz, Alexander and Pattinson, Dirk},
doi = {10.1017/S0960129505004755},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = jun,
number = {3},
pages = {453--473},
title = {Coalgebraic modal logic of finite rank},
volume = {15},
year = {2005}
}
@article{Martin1991a,
author = {Martin, C. E. and Hoare, C. A. R. and Jifeng, He},
doi = {10.1017/S0960129500001262},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = jul,
number = {02},
pages = {141},
title = {Pre-adjunctions in order enriched categories},
volume = {1},
year = {1991}
}
@book{Shafer1976,
author = {Shafer, Glenn},
pages = {314},
publisher = {Princeton University Press},
title = {A mathematical theory of evidence},
year = {1976}
}
@article{Hunter2010,
abstract = {There are relatively few proposals for inconsistency measures for propositional belief bases. However inconsistency measures are potentially as important as information measures for artificial intelligence, and more generally for computer science. In particular, they can be useful to define various operators for belief revision, belief merging, and negotiation. The measures that have been proposed so far can be split into two classes. The first class of measures takes into account the number of formulae required to produce an inconsistency: the more formulae required to produce an inconsistency, the less inconsistent the base. The second class takes into account the proportion of the language that is affected by the inconsistency: the more propositional variables affected, the more inconsistent the base. Both approaches are sensible, but there is no proposal for combining them. We address this need in this paper: our proposal takes into account both the number of variables affected by the inconsistency and the distribution of the inconsistency among the formulae of the base. Our idea is to use existing inconsistency measures in order to define a game in coalitional form, and then to use the Shapley value to obtain an inconsistency measure that indicates the responsibility/contribution of each formula to the overall inconsistency in the base. This allows us to provide a more reliable image of the belief base and of the inconsistency in it.},
author = {Hunter, Anthony and Konieczny, S{\'{e}}bastien},
doi = {10.1016/j.artint.2010.06.001},
issn = {00043702},
journal = {Artif. Intell.},
keywords = {Conflict resolution,Inconsistency management,Inconsistency measures,Inconsistency tolerance,Paraconsistency,Shapley values},
month = sep,
number = {14},
pages = {1007--1026},
publisher = {Elsevier B.V.},
title = {On the measure of conflicts: Shapley Inconsistency Values},
volume = {174},
year = {2010}
}
@inproceedings{Fredrikson2014,
abstract = {Describes how inverse model attacks can use a model with a high epsilon value for epislon-differential privacy in order to find out the value of one of the predictor variables. This is much more possible for large value of epsilons (>5) than smallvalues (<1).},
author = {Fredrikson, Matt and Lantz, Eric and Jha, Somesh and Lin, Simon and Page, David and Ristenpart, Thomas},
booktitle = {Proc. 23rd {USENIX} Secur. Symp.},
isbn = {9781931971157},
pages = {17--32},
pmid = {27077138},
publisher = {{USENIX} Association},
title = {Privacy in Pharmacogenetics: An End-to-End Case Study of Personalized Warfarin Dosing},
year = {2014}
}
@article{Alpern1985,
abstract = {A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that 'something good' eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property. ?? 1985.},
author = {Alpern, Bowen and Schneider, Fred B.},
doi = {10.1016/0020-0190(85)90056-0},
issn = {00200190},
journal = {Inf. Process. Lett.},
keywords = {Liveness,absolute liveness,concurrency,property,safety,semantics,topology,uniform liveness},
month = oct,
number = {4},
pages = {181--185},
title = {Defining liveness},
volume = {21},
year = {1985}
}
@inproceedings{Lin2012,
abstract = {In statistical privacy, privacy definitions are contracts that guide the\nbehavior of algorithms that take in sensitive data and produce sanitized\ndata. Historically, data privacy breaches have been the result of\nfundamental misunderstandings about what a particular privacy definition\nguarantees.\nPrivacy definitions are often analyzed using a hit-or-miss approach: a\nspecific attack strategy is evaluated to determine if a specific type of\ninformation can be inferred. If the attack works, the privacy definition\nis known to be too weak. If it doesn't work, little information is\ngained. Furthermore, these strategies will not identify cases where a\nprivacy definition protects unnecessary pieces of information.\nA systematic analysis of privacy definitions is a long-standing open\nproblem. In this paper, we present initial steps towards a solution.\nUsing privacy axioms, we identify two mathematical objects that are\nassociated with privacy definitions - the consistent closure and the row\ncone (which is constructed from the consistent closure). The row cone is\na geometric object which neatly encapsulates Bayesian guarantees\nprovided by a privacy definition.\nWe apply these ideas to the study of randomized response to show that it\nprovides unnecessarily strong protections on the parity of a dataset.},
author = {Lin, Bing-Rong and Kifer, Daniel},
booktitle = {2012 Conf. Rec. Forty Sixth Asilomar Conf. Signals, Syst. Comput.},
doi = {10.1109/ACSSC.2012.6489162},
isbn = {978-1-4673-5051-8},
issn = {10586393},
month = nov,
pages = {975--979},
publisher = {IEEE},
title = {Reasoning about privacy using axioms},
year = {2012}
}
@article{Basin2011,
abstract = {The distributed temporal logic DTL is an expressive logic, well suited for formalizing properties of concurrent, communicating agents. We show how DTL can be used as a metalogic to reason about and relate different security protocol models. This includes reasoning about model simplifications, where models are transformed to have fewer agents or behaviors, and verifying model reductions, where to establish the validity of a property it suffices to consider its satisfaction on only a subset of models. We illustrate how DTL can be used to formalize security models, protocols, and properties, and then present three concrete examples of metareasoning. First, we prove a general theorem about sufficient conditions for data to remain secret during communication. Second, we prove the equivalence of two models for guaranteeing message-origin authentication. Finally, we relate channel-based and intruder-centric models, showing that it is sufficient to consider models in which the intruder completely controls the network. While some of these results belong to the folklore or have been shown, mutatis mutandis, using other formalisms, DTL provides a uniform means to prove them within the same formalism. It also allows us to clarify subtle aspects of these model transformations that are often neglected or cannot be specified in the first place. ?? 2011 Elsevier B.V. All rights reserved.},
author = {Basin, David and Caleiro, Carlos and Ramos, Jaime and Vigan??, Luca},
doi = {10.1016/j.tcs.2011.04.006},
isbn = {0304-3975},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Distributed temporal logic,Security protocol analysis,Security protocol models,Security protocols,Temporal logic},
number = {31},
pages = {4007--4043},
publisher = {Elsevier B.V.},
title = {Distributed temporal logic for the analysis of security protocol models},
volume = {412},
year = {2011}
}
@incollection{Barendregt1992,
author = {Barendregt, Henk},
booktitle = {Handb. Log. Comput. Sci.},
doi = {10.1.1.26.4391},
editor = {Abramsky, Samson and Gabbay, Dov and Maibaum, Thomas S.E.},
isbn = {9780198537618},
pages = {117--309},
publisher = {Oxford University Press},
title = {Lambda calculi with types},
volume = {2},
year = {1993}
}
@article{Palmigiano2004,
author = {Palmigiano, Alessandra},
doi = {10.1016/j.tcs.2004.07.026},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {positive modal algebra,positive modal logic,priestley space,vietoris functor},
month = oct,
number = {1-2},
pages = {175--195},
title = {A coalgebraic view on positive modal logic},
volume = {327},
year = {2004}
}
@article{Pavlovic2012,
abstract = {Man-in-the-Middle (MM) is not only a ubiquitous attack pattern in security, but also an important paradigm of network computation and economics. Recognizing ongoing MM-attacks is an important security task; modeling MM-interactions is an interesting task for semantics of computation. Traced monoidal categories are a natural framework for MM-modelling, as the trace structure provides a tool to hide what happens *in the middle*. An effective analysis of what has been traced out seems to require an additional property of traces, called *normality*. We describe a modest model of network computation, based on partially ordered multisets (pomsets), where basic network interactions arise from the monoidal trace structure, and a normal trace structure arises from an iterative, i.e. coalgebraic structure over terms and messages used in computation and communication. The correspondence is established using a convenient monadic description of normally traced monoidal categories.},
archivePrefix = {arXiv},
arxivId = {1203.6324},
author = {Pavlovi{\'{c}}, Dusko},
eprint = {1203.6324},
journal = {ArXiv e-prints},
month = mar,
pages = {23},
title = {Tracing the Man in the Middle in Monoidal Categories},
year = {2012}
}
@book{Streicher2006a,
abstract = {This textbook provides a basis for a PhD course on domain-theoretic semantics of functional programming languages and their meta-mathematical properties. It introduces basic domain theory and the technique of logical relations as developed by Scott and Plotkin. The solution of recursive domain equations is explained in detail. A complete discussion of the famous full abstraction problem for PCF (a functional Kernel language due to Scott and Plotkin) is given including a construction of the fully abstract Milner model using Kripke logical relations. A final chapter introduces computability in Scott domains and shows that this model is fully abstract and universal for appropriate extensions of PCF by parallel language constructs.},
author = {Streicher, Thomas},
doi = {10.1142/6284},
isbn = {978-981-270-142-8},
month = dec,
pages = {132},
publisher = {World Scientific},
title = {Domain-Theoretic Foundations of Functional Programming},
year = {2006}
}
@article{Hermida2014,
author = {Hermida, Claudio and Reddy, Uday S. and Robinson, Edmund P.},
doi = {10.1016/j.entcs.2014.02.008},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {category theory,data abstraction,definability,fibrations,hiding,homomorphisms,information,logical relations,natural,parametric polymorphism,reflexive graphs,relation lifting,relational parametricity,transformations,universal algebra},
month = mar,
pages = {149--180},
publisher = {Elsevier B.V.},
title = {Logical Relations and Parametricity – A Reynolds Programme for Category Theory and Programming Languages},
volume = {303},
year = {2014}
}
@article{Pin1996,
author = {Pin, Jean-{\'{E}}ric and Weil, Pascal},
doi = {10.1007/BF01243597},
issn = {0002-5240},
journal = {Algebr. Universalis},
month = dec,
number = {4},
pages = {577--595},
title = {A Reiterman theorem for pseudovarieties of finite first-order structures},
volume = {35},
year = {1996}
}
@article{Rosicky1990,
author = {Rosick{\'{y}}, Jiř{\'{i}} and Trnkov{\'{a}}, V{\v{e}}ra and Ad{\'{a}}mek, Jiř{\'{i}}},
doi = {10.1007/BF01182450},
issn = {0002-5240},
journal = {Algebr. Universalis},
month = jun,
number = {2},
pages = {153--170},
title = {Unexpected properties of locally presentable categories},
volume = {27},
year = {1990}
}
@article{Aczel2003,
abstract = {Infinite trees form a free completely iterative theory over any given signature - this fact, proved by Elgot, Bloom and Tindell, turns out to be a special case of a much more general categorical result exhibited in the present paper. We prove that whenever an endofunctor H of a category has final coalgebras for all functors H(_)+X, then those coalgebras, TX, form a monad. This monad is completely iterative, i.e., every guarded system of recursive equations has a unique solution. And it is a free completely iterative monad on H. The special case of polynomial endofunctors of the category Set is the above mentioned theory, or monad, of infinite trees. This procedure can be generalized to monoidal categories satisfying a mild side condition: if, for an object H, the endofunctor H ⊗_+I has a final coalgebra, T, then T is a monoid. This specializes to the above case for the monoidal category of all endofunctors. {\textcopyright} 2002 Elsevier Science B.V. All rights reserved.},
author = {Aczel, Peter and Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1016/S0304-3975(02)00728-4},
isbn = {0960129502},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Coalgebra,Completely iterative theory,Monad,Monoidal category,Solution Theorem},
number = {1-3},
pages = {1--45},
title = {Infinite trees and completely iterative theories: A coalgebraic view},
volume = {300},
year = {2003}
}
@article{Schroder2010b,
abstract = {Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The mu-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics tend to trade expressivity for simplicity and readability, and in fact often live within the single variable fragment of the mu-calculus. The family of such flat fixpoint logics includes, e.g., LTL, CTL, and the logic of common knowledge. Extending this notion to the generic semantic framework of coalgebraic logic enables covering a wide range of logics beyond the standard mu-calculus including, e.g., flat fragments of the graded mu-calculus and the alternating-time mu-calculus (such as alternating-time temporal logic ATL), as well as probabilistic and monotone fixpoint logics. We give a generic proof of completeness of the Kozen-Park axiomatization for such flat coalgebraic fixpoint logics.},
archivePrefix = {arXiv},
arxivId = {1004.2717},
author = {Schr{\"{o}}der, Lutz and Venema, Yde},
doi = {10.1007/978-3-642-15375-4_36},
eprint = {1004.2717},
title = {Completeness of Flat Coalgebraic Fixpoint Logics},
year = {2010}
}
@article{Truta2006,
abstract = {In this paper, we introduce a new privacy protection property called p-sensitive k-anonymity. The existing kanonymity property protects against identity disclosure, but it fails to protect against attribute disclosure. The new introduced privacy model avoids this shortcoming. Two necessary conditions to achieve p-sensitive kanonymity property are presented, and used in developing algorithms to create masked microdata with p-sensitive k-anonymity property using generalization and suppression.},
author = {Truta, Traian Marius and Vinay, Bindu},
doi = {10.1109/ICDEW.2006.116},
isbn = {0769525717},
journal = {ICDEW 2006 - Proc. 22nd Int. Conf. Data Eng. Work.},
title = {Privacy protection: p-Sensitive k-Anonymity property},
year = {2006}
}
@incollection{Pare1978,
author = {Par{\'{e}}, Robert and Schumacher, Dietmar},
booktitle = {Index. Categ. Their Appl.},
doi = {10.1007/BFb0061361},
isbn = {978-3-540-08914-8},
pages = {1--125},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Abstract families and the adjoint functor theorems},
year = {1978}
}
@incollection{Chatzikokolakis2013,
author = {Chatzikokolakis, Konstantinos and Andr{\'{e}}s, Miguel E. and Bordenabe, Nicol{\'{a}}s Emilio and Palamidessi, Catuscia},
booktitle = {Priv. Enhancing Technol. PETS 2013},
doi = {10.1007/978-3-642-39077-7_5},
editor = {Cristofaro, Emiliano De and Wright, Matthew},
isbn = {9783642390777},
pages = {82--102},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Broadening the Scope of Differential Privacy Using Metrics},
volume = {7981},
year = {2013}
}
@article{Yager1987,
abstract = {We discuss the basic concepts of the Dempster-Shafer approach, basic probability assignments, belief functions, and probability functions. We discuss how to represent various types of knowledge in this framework. We discuss measures of entropy and specificity for belief structures. We discuss the combination and extension of belief structures. We introduce some concerns associated with the Dempster rule of combination inherent in the normalization due to conflict. We introduce two alternative techniques for combining belief structures. The first uses Dempster's rule, while the second is based upon a modification of this rule. We discuss the issue of credibility of a witness. {\textcopyright} 1987.},
author = {Yager, Ronald R.},
doi = {10.1016/0020-0255(87)90007-7},
isbn = {0020-0255},
issn = {00200255},
journal = {Inf. Sci. (Ny).},
month = mar,
number = {2},
pages = {93--137},
title = {On the dempster-shafer framework and new combination rules},
volume = {41},
year = {1987}
}
@inproceedings{Garg2011a,
address = {New York, New York, USA},
author = {Garg, Deepak and Jia, Limin and Datta, Anupam},
booktitle = {Proc. 18th ACM Conf. Comput. Commun. Secur. - CCS '11},
doi = {10.1145/2046707.2046726},
isbn = {9781450309486},
keywords = {audit,formal logic,incomplete logs,privacy policy},
pages = {151},
publisher = {ACM Press},
title = {Policy auditing over incomplete logs},
year = {2011}
}
@article{Guitart2013,
author = {Guitart, Ren{\'{e}}},
journal = {Cah. Topol. g{\'{e}}om{\'{e}}trie diff{\'{e}}rentielle cat{\'{e}}goriques},
keywords = {06a15,18a40,18b10,2010,adjunction,algebraic universes,bi-adjunction,bration,galois connection,mathematics subject classification,topos,trifi-,trijunction},
pages = {13--27},
title = {TRIJUNCTIONS AND TRIADIC GALOIS CONNECTIONS},
volume = {LIV-1},
year = {2013}
}
@incollection{Samarati2001,
abstract = {Access control is the process of mediating every request to resources and data maintained by a system and determining whether the request should be granted or denied. The access control decision is enforced by a mechanism implementing regulations established by a security policy. Different access control policies can be applied, corresponding to different criteria for defining what should, and what should not, be allowed, and, in some sense, to different definitions of what ensuring security means. In this chapter we investigate the basic concepts behind access control design and enforcement, and point out different security requirements that may need to be taken into consideration. We discuss several access control policies, and models formalizing them, that have been proposed in the literature or that are currently under investigation.},
author = {Samarati, Pierangela and de Vimercati, Sabrina Capitani},
booktitle = {Found. Secur. Anal. Des.},
doi = {10.1007/3-540-45608-2_3},
isbn = {3540428968},
keywords = {Computer Science,authorization},
pages = {137--196},
title = {Access control: policies, models, and mechanisms},
volume = {2171},
year = {2001}
}
@book{Nielson2007,
address = {London},
author = {Nielson, Hanne Riis and Nielson, Flemming},
doi = {10.1007/978-1-84628-692-6},
isbn = {978-1-84628-691-9},
publisher = {Springer London},
series = {Undergraduate Topics in Computer Science},
title = {Semantics with Applications: An Appetizer},
year = {2007}
}
@article{Clark2008,
abstract = {We investigate first-order axiomatic descriptions of naturally occurring classes of Boolean topological structures (these structures can have operations and relations, and carry a compatible compact Hausdorff topology with a basis of clopen sets). Our methods utilize inverse limits and ultraproducts of finite structures. We illustrate the range of possible axiomatizations of these classes with applications of our methods to Boolean topological lattices, graphs, ordered structures, unary algebras and semigroups. For example, whereas the class of all k-colorable graphs is known to be axiomatizable by universal Horn sentences, we find the class of continuously k-colorable Boolean topological graphs is not even first-order axiomatizable. ?? 2008 Elsevier Inc. All rights reserved.},
author = {Clark, D. M. and Davey, Brian A. and Jackson, M. G. and Pitkethly, Jane G.},
doi = {10.1016/j.aim.2008.03.020},
issn = {00018708},
journal = {Adv. Math. (N. Y).},
keywords = {Graph,Inverse limit,Lattice,Natural duality,Ordered set,Profinite,Semigroup,Topological prevariety,Topological quasivariety,Unary algebra,Universal Horn class},
number = {5},
pages = {1604--1653},
title = {The axiomatizability of topological prevarieties},
volume = {218},
year = {2008}
}
@article{Gibbons2011,
author = {Gibbons, Jeremy and Hinze, Ralf},
doi = {10.1145/2034574.2034777},
isbn = {978-1-4503-0865-6},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {algebraic specification,equational reasoning,lawvere theories,monads},
month = sep,
number = {9},
pages = {2},
title = {Just do it: Simple monadic equational reasoning},
volume = {46},
year = {2011}
}
@article{Rutten2008,
author = {Rutten, Jan J.M.M.},
doi = {10.2168/LMCS-4(3:9)2008},
editor = {Mossakowski, Till},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = sep,
number = {3},
pages = {1--22},
title = {Rational streams coalgebraically},
volume = {4},
year = {2008}
}
@article{Urban2004,
author = {Urban, Christian and Pitts, Andrew M. and Gabbay, Murdoch J.},
doi = {10.1016/j.tcs.2004.06.016},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {abstract syntax,alpha-conversion,binding operations,uni{\"{y}}cation},
month = sep,
number = {1-3},
pages = {473--497},
title = {Nominal unification},
volume = {323},
year = {2004}
}
@article{Lambek1968a,
author = {Lambek, Joachim},
doi = {10.1007/BF01110627},
journal = {Math. Zeitschrift},
month = apr,
number = {2},
pages = {151--161},
title = {A fixpoint theorem for complete categories},
type = {Journal article},
volume = {103},
year = {1968}
}
@incollection{Hasuo2006,
address = {Berlin, Heidelberg},
author = {Hasuo, Ichiro},
booktitle = {CONCUR 2006--Concurrency Theory},
doi = {10.1007/11817949_27},
editor = {Baier, Christel and Hermanns, Holger},
isbn = {978-3-540-37376-6},
pages = {406--420},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Generic forward and backward simulations},
volume = {4137},
year = {2006}
}
@book{Ribes2010,
address = {Berlin, Heidelberg},
author = {Ribes, Luis and Zalesskii, Pavel},
doi = {10.1007/978-3-642-01642-4},
isbn = {978-3-642-01641-7},
publisher = {Springer Berlin Heidelberg},
series = {A Series of Modern Surveys in Mathematics},
title = {Profinite Groups},
year = {2010}
}
@article{Ghilardi1995a,
author = {Ghilardi, Silvio},
doi = {10.1016/0168-0072(93)E0084-2},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
month = feb,
number = {3},
pages = {189--245},
title = {An algebraic theory of normal forms},
volume = {71},
year = {1995}
}
@article{Adamek2010b,
abstract = {Sifted colimits, important for algebraic theories, are “almost” just the combination of filtered colimits and reflexive coequalizers. For example, given a finitely cocomplete category A, then a functor with domain A preserves sifted colimits iff it preserves filtered colimits and reflexive coequalizers. But for general categories A that statement is not true: we provide a counter-example.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Rosick{\'{y}}, Jiř{\'{i}} and Vitale, Enrico M.},
journal = {Theory Appl. Categ.},
keywords = {and phrases,filtered colimit,reflexive coequalizer,sifted colimit},
number = {13},
pages = {251--260},
title = {What are sifted colimits?},
volume = {23},
year = {2010}
}
@incollection{Benabou1967,
author = {Benabou, Jean},
booktitle = {Reports Midwest Categ. Semin.},
doi = {10.1007/BFb0074298},
isbn = {978-3-540-03918-1},
pages = {1--77},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Introduction to bicategories},
volume = {47},
year = {1967}
}
@article{Rot2015,
abstract = {We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method for a large class of state based systems, including labelled transition systems but also stream systems and weighted automata. Our approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. All in all, this gives a powerful and modular framework for simplified coinductive proofs of equivalence.},
author = {Rot, Jurriaan and Bonchi, Filippo and Bonsangue, Marcello M. and Pous, Damien and Rutten, Jan J.M.M. and Silva, Alexandra},
doi = {10.1017/S0960129515000523},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = dec,
pages = {1--29},
title = {Enhanced coalgebraic bisimulation},
year = {2015}
}
@article{Desharnais2003,
abstract = {In a recent paper Baier et al. [Lecture Notes in Computer Science, Springer-Verlag, 2000, p. 358] analyzed a new way of model-checking formulas of a logic for continuous-time processes - called continuous stochastic logic (henceforth CSL) - against continuous-time Markov chains - henceforth CTMCs. One of the important results of that paper was the proof that if two CTMCs were bisimilar then they would satisfy exactly the same formulas of CSL. This raises the converse question - does satisfaction of the same collection of CSL formulas imply bisimilarity? In other words, given two CTMCs which are known to satisfy exactly the same formulas of CSL does it have to be the case that they are bisimilar? We prove that the answer to the question just raised is "yes". In fact we prove a significant extension, namely that a subset of CSL suffices even for systems where the state space may be a continuum. Along the way we prove a result to the effect that the set of Zeno paths has measure zero provided that the transition rates are bounded. {\textcopyright} 2002 Published by Elsevier Science Inc.},
author = {Desharnais, Jos{\'{e}}e and Panangaden, Prakash},
doi = {10.1016/S1567-8326(02)00068-1},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
keywords = {Bisimulation,CSL logic,Continuous-time,Markov processes,Zeno paths},
month = may,
number = {1-2},
pages = {99--115},
title = {Continuous stochastic logic characterizes bisimulation of continuous-time Markov processes},
volume = {56},
year = {2003}
}
@article{Constable2011a,
abstract = {We establish completeness for intuitionistic first-order logic, iFOL, showing that a formula is provable if and only if its embedding into minimal logic, mFOL, is uniformly valid under the Brouwer Heyting Kolmogorov (BHK) semantics, the intended semantics of iFOL and mFOL. Our proof is intuitionistic and provides an effective procedure Prf that converts uniform minimal evidence into a formal first-order proof. We have implemented Prf. Uniform validity is defined using the intersection operator as a universal quantifier over the domain of discourse and atomic predicates. Formulas of iFOL that are uniformly valid are also intuitionistically valid, but not conversely. Our strongest result requires the Fan Theorem; it can also be proved classically by showing that Prf terminates using Konig's Theorem. The fundamental idea behind our completeness theorem is that a single evidence term evd witnesses the uniform validity of a minimal logic formula F. Finding even one uniform realizer guarantees intuitionistic validity because Prf(F, evd) builds a first-order proof of F, establishing its intuitionistic validity and providing a purely logical normalized realizer. We establish completeness for iFOL as follows. Friedman showed that iFOL can be embedded in minimal logic (mFOL) by his A-transformation, mapping formula F to FA. If F is uniformly valid, then so is FA, and by our completeness theorem, we can find a proof of FA in minimal logic. Then we intuitionistically prove F from FFalse, i.e. by taking False for A and for \bot of mFOL. Our result resolves an open question posed by Beth in 1947.},
archivePrefix = {arXiv},
arxivId = {1110.1614},
author = {Constable, Robert and Bickford, Mark},
doi = {10.1016/j.apal.2013.07.009},
eprint = {1110.1614},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
number = {1},
pages = {1--24},
publisher = {Elsevier B.V.},
title = {Intuitionistic Completeness of First-Order Logic},
volume = {165},
year = {2011}
}
@article{Fellegi1969,
abstract = {JSTOR is a not-for-profit service that helps scholars, researchers, and students discover, use, and build upon a wide range of content in a trusted digital archive. We use information technology and tools to increase productivity and facilitate new forms of scholarship. For more information about JSTOR, please contact support@jstor.org. A mathematical model is developed to provide a theoretical frame-work for a computer-oriented solution to the problem of recognizing those records in two files which represent identical persons, objects or events (said to be matched). A comparison is to be made between the recorded characteristics and values in two records (one from each file) and a decision made as to whether or not the members of the comparison-pair represent the same person or event, or whether there is insufficient evidence to justify either of these decisions at stipulated levels of error. These three decisions are referred to as link (A1), a non-link (A3), and a possible link (A2). The first two decisions are called positive dispositions. The two types of error are defined as the error of the decision A, when the members of the comparison pair are in fact unmatched, and the error of the decision A, when the members of the comparison pair are, in fact matched. The probabilities of these errors are defined as = E u(y)P(A,I y) rer and X m(r)P(AaIr) yTr respectively where u(y), m(y) are the probabilities of realizing y (a comparison vector whose components are the coded agreements and disagreements on each characteristic) for unmatched and matched record pairs respectively. The summation is over the whole comparison space r of possible realizations. A linkage rule assigns probabilities P(A, Iy), and P(A2 1y), and P(A3 'y) to each possible realization of y e P. An optimal linkage rule L (u, X, r) is defined for each value of (,u, X) as the rule that minimizes P(A2) at those error levels. In other words, for fixed levels of error, the rule minimizes the probability of failing to make positive dispositions. A theorem describing the construction and properties of the optimal linkage rule and two corollaries to the theorem which make it a practical working tool are given.},
archivePrefix = {arXiv},
arxivId = {arXiv:1011.2649v3},
author = {Fellegi, Ivan P. and Sunter, Alan B.},
doi = {10.2307/2286061},
eprint = {arXiv:1011.2649v3},
isbn = {01621459},
issn = {01621459},
journal = {J. Am. Stat. Assoc.},
month = dec,
number = {328},
pages = {1183},
title = {A Theory for Record Linkage},
volume = {64},
year = {1969}
}
@inproceedings{Delaware2013,
address = {New York, New York, USA},
author = {Delaware, Benjamin and Keuchel, Steven and Schrijvers, Tom and Oliveira, Bruno C.d.S.},
booktitle = {Proc. 18th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '13},
doi = {10.1145/2500365.2500587},
isbn = {9781450323260},
pages = {319},
publisher = {ACM Press},
title = {Modular monadic meta-theory},
year = {2013}
}
@article{Rosicky1994a,
author = {Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1016/0022-4049(94)90023-X},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = mar,
number = {2},
pages = {185--190},
title = {Models of Horn theories revisited},
volume = {92},
year = {1994}
}
@book{Vickers1996a,
author = {Vickers, Steven},
doi = {10.2277/0521576512},
isbn = {0521576512},
month = sep,
publisher = {Cambridge University Press},
title = {Topology via Logic},
type = {Book},
year = {1996}
}
@article{Lambek1968,
author = {Lambek, Joachim},
doi = {10.1007/BF01703261},
issn = {0025-5661},
journal = {Math. Syst. Theory},
month = dec,
number = {4},
pages = {287--318},
publisher = {Springer-Verlag},
title = {Deductive systems and categories},
volume = {2},
year = {1968}
}
@article{Ferrari2005a,
author = {Ferrari, Gianluigi and Montanari, Ugo and Tuosto, Emilio},
isbn = {0304-3975},
journal = {Theor. Comput. Sci.},
keywords = {Finite state verification,Name passing calculi,P,algorithm,bisimulation,calculi,checking,co-algebras,dependent,finite,name,partition,passing,refinement,state,types,verification},
mendeley-tags = {algorithm,bisimulation,calculi,checking,co-algebras,dependent,finite,name,partition,passing,refinement,state,types,verification},
number = {2--3},
pages = {325--365},
title = {Coalgebraic minimization of HD-automata for the $\pi$-calculus using polymorphic types},
type = {Journal article},
volume = {331},
year = {2005}
}
@article{Nanz2006,
abstract = {We present a framework for specification and security analysis of communication protocols for mobile wireless networks. This setting introduces new challenges which are not being addressed by classical protocol analysis techniques. The main complication stems from the fact that the actions of intermediate nodes and their connectivity can no longer be abstracted into a single unstructured adversarial environment as they form an inherent part of the system's security. In order to model this scenario faithfully, we present a broadcast calculus which makes a clear distinction between the protocol processes and the network's connectivity graph, which may change independently from protocol actions. We identify a property characterising an important aspect of security in this setting and express it using behavioural equivalences of the calculus. We complement this approach with a control flow analysis which enables us to automatically check this property on a given network and attacker specification. ?? 2006 Elsevier B.V. All rights reserved.},
author = {Nanz, Sebastian and Hankin, Chris},
doi = {10.1016/j.tcs.2006.08.036},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Control flow analysis,Mobile ad hoc networks,Process calculi,Security analysis},
month = nov,
number = {1-2},
pages = {203--227},
title = {A framework for security analysis of mobile wireless networks},
volume = {367},
year = {2006}
}
@article{White2012,
abstract = {We analyse the philosopher Davidson's semantics of actions, using a strongly typed logic with contexts given by sets of partial equations between the outcomes of actions. This provides a perspicuous and elegant treatment of reasoning about action, analogous to Reiter's work on artificial intelligence. We define a sequent calculus for this logic, prove cut elimination, and give a semantics based on fibrations over partial cartesian categories: we give a structure theory for such fibrations. The existence of lax comma objects is necessary for the proof of cut elimination, and we give conditions on the domain fibration of a partial cartesian category for such comma objects to exist.},
archivePrefix = {arXiv},
arxivId = {1202.0255},
author = {White, Graham},
eprint = {1202.0255},
month = feb,
title = {Reasoning about Unreliable Actions},
year = {2012}
}
@inproceedings{Gordon2014,
abstract = {Probabilistic programming means two strongly connected models as well as the study of their mathematical properties, solutions of the relevant optimization problems and their applications. The two models are: maximizing (or minimizing) a probability under constraints and programming under probabilistic constraints. There are a number of variants and special cases of these models and we present them in Section 1. In Section 2 we summarize those mathematical theories which can be used to prove the convexity of large classes of our problems and we also show how they can be applied in this context. In Section 3 we present solution algorithms of our stochastic programming problems. Since we are handling probabilities of sets in higher dimensional spaces, it is necessary to use bounding and other approximation algorithms to find these probabilities with satisfactory precision. This is the subject of Section 5. In Section 4 we present two-stage and multi-stage problems which are combined with probabilistic constraints. Some duality and stability theorems are presented in Section 6. Finally, in Section 7, we present applications of our model constructions. {\textcopyright} 2003 Elsevier Inc. All rights reserved.},
archivePrefix = {arXiv},
arxivId = {1312.4328},
author = {Gordon, Andrew D. and Henzinger, Thomas A. and Nori, Aditya V. and Rajamani, Sriram K.},
booktitle = {Proc. Futur. Softw. Eng.},
doi = {10.1145/2593882.2593900},
eprint = {1312.4328},
isbn = {9781450328654},
issn = {09270507},
pages = {167--181},
publisher = {ACM Press},
series = {FOSE 2014},
title = {Probabilistic programming},
volume = {10},
year = {2014}
}
@article{Ghani2012,
author = {Ghani, Neil and Johann, Patricia and Fumex, Clement},
doi = {10.2168/LMCS-8(2:12)2012},
editor = {Veith, Helmut},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = jun,
number = {2},
pages = {1--27},
title = {Generic fibrational induction},
volume = {8},
year = {2012}
}
@article{Atkey2013,
author = {Atkey, Robert and McBride, Conor},
doi = {10.1145/2544174.2500597},
isbn = {9781450323260},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {coalgebras,corecursion,guarded recursion,total func-},
month = nov,
number = {9},
pages = {197--208},
title = {Productive coprogramming with guarded recursion},
volume = {48},
year = {2013}
}
@article{Cirstea2016,
abstract = {We define quantitative fixpoint logics for reasoning about linear time properties of states in systems with branching behaviour. We model such systems as coalgebras whose type arises as the composition of a branching monad with one or more polynomial endofunctors on the category of sets. The domain of truth values for our logics is determined by the choice of branching monad, as is the special modality used to abstract away branching in the semantics of the logics. To justify our choice of syntax and semantics for the logics, we prove the equivalence between their step-wise semantics and an alternative path-based semantics for the fixpoint-free fragments of the logics. Instances of these logics support reasoning about the possibility, probability or minimal cost of exhibiting a given linear time property. We conclude with two examples of logics that have a linear time flavour but do not admit a path-based semantics, namely a logic for reasoning about resource usage in infinitely-running computations, and a quantitative logic for reasoning about component interaction.},
archivePrefix = {arXiv},
arxivId = {1612.07844},
author = {C{\^{i}}rstea, Corina},
doi = {10.2168/LMCS-},
eprint = {1612.07844},
isbn = {9783642548611},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {Algebraic theories,Equational logic,Rewriting,Soundness and completeness,Variable binding,$\alpha$-equivalence},
month = dec,
number = {3},
pages = {1--26},
title = {A coalgebraic approach to quantitative linear time logics},
volume = {7},
year = {2016}
}
@article{Bartels2003,
abstract = {We introduce the $\lambda$-coiteration schema for a distributive law $\lambda$ of a functor T over a functor F. Under certain conditions it can be shown to uniquely characterise functions into the carrier of a final F-coalgebra, generalising the basic coiteration schema as given by finality. The duals of primitive recursion and course-of-value iteration, which are known extensions of coiteration, arise as instances of our framework. One can furthermore obtain schemata justifying recursive specifications that involve operators such as addition of power series, regular operators on languages, or parallel and sequential composition of processes. Next, the same type of distributive law $\lambda$ is used to generalise coinductive proof techniques. To this end, we introduce the notion of a $\lambda$-bisimulation relation. It specialises to what could be called bisimulation up-to-equality or bisimulation up-to-context for contexts built from operators of the type mentioned above. We state that every such relation is contained in some larger conventional bisimulation and demonstrate that this principle leads to simpler bisimilarity proofs using less complex relations. {\textcopyright}2001 Published by Elsevier Science B.V.},
author = {Bartels, Falk},
doi = {10.1017/S0960129502003900},
isbn = {0960129502},
issn = {09601295},
journal = {Math. Struct. Comput. Sci.},
month = apr,
number = {2},
pages = {321--348},
title = {Generalised coinduction},
volume = {13},
year = {2003}
}
@article{Hashiguchi2004,
author = {Hashiguchi, Kosaburo and Sakakibara, Naoto and Jimbo, Shuji},
doi = {10.1016/j.tcs.2003.09.005},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Free binoid,Regular (monoid) expression,Regular binoid expression,Regular language},
month = jan,
number = {2-3},
pages = {251--266},
title = {Equivalence of regular binoid expressions and regular expressions denoting binoid languages over free binoids},
volume = {312},
year = {2004}
}
@article{Shafer2015,
abstract = {The theory of belief functions is a generalization of probability theory; a belief function is a set function more general than a probability measure but whose values can still be interpreted as degrees of belief. Dempster's rule of combination is a rule for combining two or more belief functions; when the belief functions combined are based on distinct or "independent" sources of evidence, the rule corresponds intuitively to the pooling of evidence. As a special case, the rule yields a rule of conditioning which generalizes the usual rule for conditioning probability measures. The rule of combination was studied extensively, but only in the case of finite sets of possibilities, in the author's monograph A Mathematical Theory of Evidence. The present paper describes the rule for general, possibly infinite, sets of possibilities. We show that the rule preserves the regularity conditions of continuity and condensability, and we investigate the two distinct generalizations of probabilistic independence which the rule suggests.},
author = {Shafer, Glenn},
doi = {10.1016/j.ijar.2015.12.009},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Belief function,Cognitive independence,Conditioning,Dempster's rule,Evidential independence,Upper probabilities},
month = dec,
pages = {26--40},
publisher = {Elsevier Inc.},
title = {Dempster's rule of combination},
volume = {79},
year = {2016}
}
@incollection{Levy2002,
abstract = {We describe a simple denotational semantics, using possible worlds, for a call-by-value language with ML-like storage facilities, allowing the storage of values of any type, and the generation of new storage cells. We first present a criticism of traditional Strachey semantics for such a language: that it requires us to specify what happens when we read non-existent cells. We then obtain our model by modifying the Strachey semantics to avoid this problem. We describe our model in 3 stages: first no storage of functions or recursion (but allowing storage of cells), then we add recursion, and finally we allow storage of functions. We discuss similarities and differences between our model and Moggi's model of ground store. A significant difference is that our model does not use monadic decomposition of the function type.},
author = {Levy, Paul Blain},
booktitle = {Comput. Sci. Log.},
doi = {10.1007/3-540-45793-3_16},
editor = {Bradfield, Julian},
isbn = {978-3-540-44240-0},
pages = {559--594},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Possible World Semantics for General Storage in Call-By-Value},
type = {Book part (with own title)},
volume = {2471},
year = {2002}
}
@incollection{Hasuo2010,
abstract = {The technique of forward/backward simulations has been applied successfully in many distributed and concurrent applications. In this paper, however, we claim that the technique can actually have more genericity and mathematical clarity. We do so by identifying forward/backward simulations as lax/oplax morphisms of coalgebras. Starting from this observation, we present a systematic study of this generic notion of simulations. It is meant to be a generic version of the study by Lynch and Vaandrager, covering both non-deterministic and probabilistic systems. In particular we prove soundness and completeness results with respect to trace inclusion: the proof is by coinduction using the generic theory of traces developed by Jacobs, Sokolova and the author. By suitably instantiating our generic framework, one obtains the appropriate definition of forward/backward simulations for various kinds of systems, for which soundness and completeness come for free.},
author = {Hasuo, Ichiro},
booktitle = {CONCUR 2010–Concurrency Theory},
doi = {10.1007/11817949_27},
editor = {Gastin, Paul and Laroussinie, Francois},
isbn = {978-3-540-37376-6},
issn = {03029743},
pages = {447--461},
publisher = {Springer, Berlin, Heidelberg},
series = {LNCS},
title = {Generic forward and backward simulations II: Probabilistic simulation},
volume = {6269},
year = {2010}
}
@article{Brady2013,
author = {Brady, Edwin},
doi = {10.1145/2544174.2500581},
isbn = {9781450323260},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
keywords = {algebraic effects,and hence be built,dependent types,difficulties,however,i,monad using the statet,o,the order in which,this can create,transformed into a state,transformer,transformers are applied matters,with an io monad},
month = nov,
number = {9},
pages = {133--144},
title = {Programming and reasoning with algebraic effects and dependent types},
volume = {48},
year = {2013}
}
@article{Herrlich1979,
author = {Herrlich, Horst and Salicrup, G. and Vazquez, R.},
doi = {10.4153/CJM-1979-097-7},
issn = {1496-4279},
journal = {Can. J. Math.},
month = oct,
number = {5},
pages = {1059--1071},
publisher = {The Canadian Mathematical Society},
title = {Dispersed factorization structures},
volume = {31},
year = {1979}
}
@article{Seely1983,
author = {Seely, Robert A. G.},
doi = {10.1002/malq.19830291005},
issn = {00443050},
journal = {Math. Log. Q.},
number = {10},
pages = {505--542},
title = {Hyperdoctrines, Natural Deduction and the Beck Condition},
volume = {29},
year = {1983}
}
@article{Szlach??nyi2003,
abstract = {Strong monoidal functors U:C???M with left adjoints determine, in a universal way, monoids T in the category of opmonoidal endofunctors on M. Treating such opmonoidal monads as abstract "quantum groupoids" we derive Tannaka duality between right adjoint strong monoidal functors and opmonoidal monads. Bialgebroids, i.e., Takeuchi's ??R-bialgebras, appear as the special case when T has also a right adjoint. Street's 2-category of monads then leads to a natural definition of the 2-category of bialgebroids. ?? 2003 Elsevier Science B.V. All rights reserved.},
archivePrefix = {arXiv},
arxivId = {math/0208198},
author = {Szlach{\'{a}}nyi, Korn{\'{e}}l},
doi = {10.1016/S0022-4049(03)00018-5},
eprint = {0208198},
isbn = {3613959151},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = aug,
number = {2-3},
pages = {287--315},
primaryClass = {math},
title = {The monoidal Eilenberg–Moore construction and bialgebroids},
volume = {182},
year = {2003}
}
@phdthesis{Mansfield2013,
author = {Mansfield, Shane},
school = {University of Oxford},
title = {The Mathematical Structure of Non-locality & Contextuality},
year = {2013}
}
@article{Harper1993,
author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon D.},
doi = {10.1145/138027.138060},
issn = {00045411},
journal = {J. ACM},
month = jan,
number = {1},
pages = {143--184},
title = {A framework for defining logics},
volume = {40},
year = {1993}
}
@article{Kurz2012,
abstract = {Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations and equations. Moreover, the presentation of the category of algebras for the functor is obtained compositionally from the presentations of the underlying category and of the functor. Part II investigates algebras for a functor over ind-completions and extends the theorem of J{\'o}nsson and Tarski on canonical extensions of Boolean algebras with operators to this setting. Part III shows, based on Part I, how to associate a finitary logic to any finite-sets preserving functor T. Based on Part II we prove the logic to be strongly complete under a reasonable condition on T.},
archivePrefix = {arXiv},
arxivId = {1207.2732},
author = {Kurz, Alexander and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.2168/LMCS-8(3:14)2012},
eprint = {1207.2732},
journal = {Log. Methods Comput. Sci.},
keywords = {algebraic theories,and phrases,coalgebras,modal logic,presen-,sifted colimits,stone duality},
month = jul,
pages = {1--32},
title = {Strongly complete logics for coalgebras},
volume = {8},
year = {2012}
}
@incollection{Wood1978,
author = {Wood, R. J.},
booktitle = {Index. Categ. Their Appl.},
doi = {10.1007/BFb0061362},
pages = {126--140},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {V-indexed categories},
year = {1978}
}
@article{Hugues2006,
abstract = {"[M]athematicians care no more for logic than logicians for mathematics." Augustus de Morgan, 1868.   Proofs are traditionally syntactic, inductively generated objects. This paper presents an abstract mathematical formulation of propositional calculus (propositional logic) in which proofs are combinatorial (graph-theoretic), rather than syntactic. It defines a *combinatorial proof* of a proposition P as a graph homomorphism h : C -> G(P), where G(P) is a graph associated with P and C is a coloured graph. The main theorem is soundness and completeness: P is true iff there exists a combinatorial proof h : C -> G(P).},
archivePrefix = {arXiv},
arxivId = {math/0408282},
author = {Hugues, D. J D},
doi = {10.4007/annals.2006.164.1065},
eprint = {0408282},
issn = {0003486X},
journal = {Ann. Math.},
pages = {1065--1076},
primaryClass = {math},
title = {Proofs without syntax},
volume = {164},
year = {2006}
}
@inproceedings{DeMarchi2005,
abstract = {There are several approaches to the problem of giving a categorical semantics to Martin-L{\"{o}}f type theory with dependent sums and products and extensional equality types. The most established one relies on the notion of a type-category (or category with attributes) with $\Sigma$ and $\Pi$ types. We extend such a semantics by introducing coinductive types both on the syntactic level and in a type-category. Soundness of the semantics is preserved. As an example of such a category, we prove that the type-category built over a locally cartesian closed category C admits coinductive types whenever C has final coalgebras for all polynomial functors.},
address = {Swansea},
author = {{De Marchi}, Federico},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/11548133_8},
editor = {Fiadeiro, Jos{\'{e}} Luiz and Harman, Neil and Roggenbach, Markus and Rutten, Jan},
pages = {114--126},
publisher = {Springer Berlin Heidelberg},
title = {On the Semantics of Coinductive Types in Martin-L{\"{o}}f Type Theory},
year = {2005}
}
@article{Appel2001,
abstract = {The proofs of {"traditional"} proof carrying code {(PCC)} are type-specialized in the sense that they require axioms about a specific type system. In contrast, the proofs of foundational {PCC} explicitly define all required types and explicitly prove all the required properties of those types assuming only a fixed foundation of mathematics such as higher-order logic. Foundational {PCC} is both more flexible and more secure than type-specialized {PCC.For} foundational {PCC} we need semantic models of type systems on von Neumann machines. Previous models have been either too weak (lacking general recursive types and first-class function-pointers), too complex (requiring machine-checkable proofs of large bodies of computability theory), or not obviously applicable to von Neumann machines. Our new model is strong, simple, and works either in {{\OE}}�-calculus or on Pentiums.},
author = {Appel, Andrew W. and McAllester, David},
doi = {10.1145/504709.504712},
issn = {01640925},
journal = {ACM Trans. Program. Lang. Syst.},
month = sep,
number = {5},
pages = {657--683},
title = {An indexed model of recursive types for foundational proof-carrying code},
volume = {23},
year = {2001}
}
@article{Lynch1995,
abstract = {A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model. In particular, (1) refinements, (2) forward and backward simulations, (3) hybrid forward-backward and backward-forward simulations, and (4) history and prophecy relations are defined. History and prophecy relations are abstract versions of the history and prophecy variables of Abadi and Lamport, as well as the auxiliary variables of Owicki and Gries, Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. Finally, it is shown how invariants can be incorporated into all the simulations. Even though many results are presented here for the first time, this paper can also be read as a survey (in a simple setting) of the research literature on simulation techniques. The development for untimed automata is designed to support a similar development for timed automata, Part II of this paper will show how the results of this paper can be carried over to the setting of timed automata.},
author = {Lynch, N. and Vaandrager, F.},
doi = {10.1006/inco.1995.1134},
issn = {08905401},
journal = {Inf. Comput.},
month = sep,
number = {2},
pages = {214--233},
title = {Forward and backward simulations},
volume = {121},
year = {1995}
}
@inproceedings{Jacobs2013a,
abstract = {So-called effect algebras and modules are basic mathematical structures that were first identified in mathematical physics, for the study of quantum logic and quantum probability. They incorporate a double negation law $p^{\perp\perp} = p. Since then it has been realised that these effect structures form a useful abstraction that covers not only quantum logic, but also Boolean logic and probabilistic logic. Moreover, the duality between effect and convex structures lies at the heart of the duality between predicates and states. These insights are leading to a uniform framework for the semantics of computation and logic. This framework has been elaborated elsewhere for set-theoretic, discrete probabilistic, and quantum computation. Here the missing case of continuous probability is shown to fit in the same uniform framework. On a technical level, this involves an investigation of the logical aspects of the Giry monad on measurable spaces and of Lebesgue integration.},
author = {Jacobs, Bart},
booktitle = {2013 28th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2013.13},
isbn = {978-1-4799-0413-6},
issn = {10436871},
keywords = {Giry monad,Probabilistic system,duality,effect algebra,measurable space},
month = jun,
pages = {83--92},
publisher = {IEEE},
title = {Measurable Spaces and Their Effect Logic},
year = {2013}
}
@article{Adamek2004a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Porst, Hans-E.},
doi = {10.1016/S0304-3975(03)00378-5},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebras},
month = jan,
number = {1-3},
pages = {257--283},
title = {On tree coalgebras and coalgebra presentations},
volume = {311},
year = {2004}
}
@article{Joyal2014,
author = {Joyal, Andr{\'{e}} and Street, Ross},
keywords = {autonomous tensor category,balanced,braiding,monoidal category,morse function,pivotal,progressive diagram,ribbon,rigid tensor category,spherical category,tensor cateory,tortile,trace},
title = {The geometry of tensor calculus II},
year = {2014}
}
@incollection{Bernardo2012a,
abstract = {One of the most studied extensions of testing theory to nondeterministic and probabilistic processes yields unrealistic probabilities estimations that give rise to two anomalies. First, probabilistic testing equivalence does not imply probabilistic trace equivalence. Second, probabilistic testing equivalence differentiates processes that perform the same sequence of actions with the same probability but make internal choices in different moments and thus, when applied to processes without probabilities, does not coincide with classical testing equivalence. In this paper, new versions of probabilistic trace and testing equivalences are presented for nondeterministic and probabilistic processes that resolve the two anomalies. Instead of focussing only on suprema and infima of the set of success probabilities of resolutions of interaction systems, our testing equivalence matches all the resolutions on the basis of the success probabilities of their identically labeled computations. A simple spectrum is provided to relate the new relations with existing ones. It is also shown that, with our approach, the standard probabilistic testing equivalences for generative and reactive probabilistic processes can be retrieved.},
author = {Bernardo, Marco and {De Nicola}, Rocco and Loreti, Michele},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-28729-9_13},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {195--209},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Revisiting Trace and Testing Equivalences for Nondeterministic and Probabilistic Processes},
volume = {7213},
year = {2012}
}
@article{Power2006,
author = {Power, A. John},
doi = {10.1016/j.tcs.2006.08.006},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {canonical model,conical colimit completion,enriched yoneda embedding,freyd -category},
month = nov,
number = {2},
pages = {254--269},
title = {Generic models for computational effects},
volume = {364},
year = {2006}
}
@inproceedings{Li2011,
abstract = {This paper aims at answering the following two questions in privacy-preserving data analysis and publishing: What formal privacy guarantee (if any) does $k$-anonymization provide? How to benefit from the adversary's uncertainty about the data? We have found that random sampling provides a connection that helps answer these two questions, as sampling can create uncertainty. The main result of the paper is that $k$-anonymization, when done "safely", and when preceded with a random sampling step, satisfies $(\epsilon,\delta)$-differential privacy with reasonable parameters. This result illustrates that "hiding in a crowd of $k$" indeed offers some privacy guarantees. This result also suggests an alternative approach to output perturbation for satisfying differential privacy: namely, adding a random sampling step in the beginning and pruning results that are too sensitive to change of a single tuple. Regarding the second question, we provide both positive and negative results. On the positive side, we show that adding a random-sampling pre-processing step to a differentially-private algorithm can greatly amplify the level of privacy protection. Hence, when given a dataset resulted from sampling, one can utilize a much large privacy budget. On the negative side, any privacy notion that takes advantage of the adversary's uncertainty likely does not compose. We discuss what these results imply in practice.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {1101.2604},
author = {Li, Ninghui and Qardaji, Wahbeh and Su, Dong},
booktitle = {Proc. 7th ACM Symp. Information, Comput. Commun. Secur. - ASIACCS '12},
doi = {10.1145/2414456.2414474},
eprint = {1101.2604},
isbn = {9781450316484},
keywords = {all or part of,anonymization,data privacy,differential privacy,is granted without fee,or hard copies of,permission to make digital,personal or classroom use,provided that copies are,this work for},
pages = {32},
publisher = {ACM Press},
title = {On sampling, anonymization, and differential privacy or, $k$-anonymization meets differential privacy},
year = {2012}
}
@incollection{Hennessy1980,
author = {Hennessy, Matthew and Milner, Robin},
booktitle = {Autom. Lang. Program. 7th Colloquium, Noordweijkerhout, Netherland, July 14-18, 1980, Proc.},
doi = {10.1007/3-540-10003-2_79},
editor = {Bakker, Jaco and Leeuwen, Jan},
isbn = {978-3-540-10003-4},
pages = {299--309},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {On observing nondeterminism and concurrency},
volume = {85},
year = {1980}
}
@incollection{Lazrig2016,
author = {Lazrig, Ibrahim and Ong, Toan and Ray, Indrajit and Ray, Indrakshi and Kahn, Michael},
booktitle = {Data Appl. Secur. Priv. XXX. DBSec 2016},
doi = {10.1007/978-3-319-41483-6_5},
editor = {Ranise, Silvio and Swarup, Vipin},
isbn = {978-3-319-41482-9},
pages = {61--76},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {Privacy Preserving Probabilistic Record Linkage Using Locality Sensitive Hashes},
volume = {9766},
year = {2016}
}
@article{Baldan2014,
archivePrefix = {arXiv},
arxivId = {1410.3385},
author = {Baldan, Paolo and Bonchi, Filippo and Kerstan, Henning and K{\"{o}}nig, Barbara},
eprint = {1410.3385},
journal = {ArXiv e-prints},
keywords = {behavioral metric,coalgebra,functor lifting,pseudometric},
month = oct,
title = {Behavioral Metrics via Functor Lifting},
year = {2014}
}
@article{Barendregt1984,
author = {Barendregt, Henk and Barendsen, Erik},
issn = {0028-9825},
journal = {Nieuw Arch. voor Wiskd.},
number = {2},
pages = {337--372},
title = {Introduction to lambda calculus},
volume = {4},
year = {1984}
}
@phdthesis{Forsberg2013,
author = {Forsberg, Fredrik Nordvall},
school = {Swansea University},
title = {Inductive-inductive Definitions},
type = {PhD Thesis},
year = {2013}
}
@article{Weirich2017,
author = {Weirich, Stephanie and Voizard, Antoine and de Amorim, Pedro Henrique Azevedo and Eisenberg, Richard A.},
doi = {10.1145/3110275},
issn = {24751421},
journal = {Proc. ACM Program. Lang.},
keywords = {Dependent Types,Haskell},
month = aug,
number = {ICFP},
pages = {1--29},
title = {A specification for dependent types in Haskell},
volume = {1},
year = {2017}
}
@article{Baier2005,
abstract = {This paper presents various semantics in the branching-time spectrum of discrete-time and continuous-time Markov chains (DTMCs and CTMCs). Strong and weak bisimulation equivalence and simulation pre-orders are covered and are logically characterized in terms of the temporal logics Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). Apart from presenting various existing branching-time relations in a uniform manner, this paper presents the following new results: (i) strong simulation for CTMCs, (ii) weak simulation for CTMCs and DTMCs, (iii) logical characterizations thereof (including weak bisimulation for DTMCs), (iv) a relation between weak bisimulation and weak simulation equivalence, and (v) various connections between equivalences and pre-orders in the continuous- and discrete-time setting. The results are summarized in a branching-time spectrum for DTMCs and CTMCs elucidating their semantics as well as their relationship. ?? 2005 Elsevier Inc. All rights reserved.},
author = {Baier, Christel and Katoen, Joost Pieter and Hermanns, Holger and Wolf, Verena},
doi = {10.1016/j.ic.2005.03.001},
isbn = {08905401},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {(Weak) Bisimulation,(Weak) Simulation,Comparative semantics,Markov chain,Temporal logic},
number = {2},
pages = {149--214},
title = {Comparative branching-time semantics for Markov chains},
volume = {200},
year = {2005}
}
@inproceedings{Filinski2007,
address = {New York, New York, USA},
author = {Filinski, Andrzej and St{\o}vring, Kristian},
booktitle = {Proc. 2007 ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '07},
doi = {10.1145/1291151.1291168},
isbn = {9781595938152},
issn = {03621340},
keywords = {abstract effects,backtracking,cons,equational reasoning,for l 1,for t,h,logical,monads,nil and l 1,recursive types,relations,streams,t,that the equation holds,with the induction hypothesis},
month = oct,
number = {9},
pages = {97},
publisher = {ACM Press},
title = {Inductive reasoning about effectful data types},
volume = {42},
year = {2007}
}
@incollection{Riecanova2006,
author = {Rie{\v{c}}anov{\'{a}}, Zdenka and Marinov{\'{a}}, Ivica and Zajac, Michal},
booktitle = {Theory Appl. Relational Struct. as Knowl. Instruments II},
doi = {10.1007/11964810_14},
editor = {de Swart, Harrie and Or{\l}owska, Ewa and Schmidt, Gunther and Roubens, Marc},
pages = {290--317},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Some Aspects of Lattice and Generalized Prelattice Effect Algebras},
volume = {4342},
year = {2006}
}
@article{Moggi1991,
author = {Moggi, Eugenio},
doi = {10.1016/0890-5401(91)90052-4},
issn = {08905401},
journal = {Inf. Comput.},
month = jul,
number = {1},
pages = {55--92},
title = {Notions of computation and monads},
volume = {93},
year = {1991}
}
@article{Fiech1996,
author = {Fiech, Adrian},
journal = {Math. Struct. Comput. Sci.},
number = {5},
pages = {455--468},
title = {Colimits in the Category DCPO},
volume = {6},
year = {1996}
}
@incollection{Atkey2012,
abstract = {This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs' fibrational formulation of induction for polynomial data types and its extension to all inductive data types by Ghani, Johann, and Fumex. An effectful data type $\mu$ ( TF ) is built from a functor F that describes data, and a monad T that computes effects. Our main contribution is to derive induction rules that are generic over all functors F and monads T such that $\mu$ ( TF ) exists. Along the way, we also derive a principle of definition by structural recursion for effectful data types that is similarly generic. Our induction rule is also generic over the kinds of properties to be proved: like the work on which we build, we work in a general fibrational setting and so can accommodate very general notions of properties, rather than just those of particular syntactic forms. We give examples exploiting the generality of our results, and show how our results specialize to those in the literature, particularly those of Filinski and St{\o}vring.},
author = {Atkey, Robert and Ghani, Neil and Jacobs, Bart and Johann, Patricia},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {42--57},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Fibrational induction meets effects},
volume = {7213},
year = {2012}
}
@article{Barthe2016a,
author = {Barthe, Gilles and Gaboardi, Marco and Hsu, Justin and Pierce, Benjamin},
doi = {10.1145/2893582.2893591},
issn = {2372-3491},
journal = {ACM SIGLOG News},
number = {1},
pages = {34--53},
title = {Programming language techniques for differential privacy},
volume = {3},
year = {2016}
}
@incollection{Gheri2017,
author = {Gheri, Lorenzo and Popescu, Andrei},
booktitle = {Interact. Theorem Proving. ITP 2017},
doi = {10.1007/978-3-319-66107-0_16},
editor = {Ayala-Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.},
isbn = {9783319661070},
pages = {241--261},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {A Formalized General Theory of Syntax with Bindings},
volume = {10499},
year = {2017}
}
@article{JEANNIN2016,
abstract = {Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well founded.},
author = {Jeannin, Jean-Baptiste and Kozen, Dexter and Silva, Alexandra},
doi = {10.1017/S0960129515000481},
isbn = {0960129515000},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = feb,
pages = {1--21},
title = {Well-founded coalgebras, revisited},
year = {2016}
}
@article{Sokolova2011,
abstract = {We survey the work on both discrete and continuous-space probabilistic systems as coalgebras, starting with how probabilistic systems are modeled as coalgebras and followed by a discussion of their bisimilarity and behavioral equivalence, mentioning results that follow from the coalgebraic treatment of probabilistic systems. It is interesting to note that, for different reasons, for both discrete and continuous probabilistic systems it may be more convenient to work with behavioral equivalence than with bisimilarity.},
author = {Sokolova, Ana},
doi = {10.1016/j.tcs.2011.05.008},
issn = {0304-3975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebra,markov chains,markov processes,probabilistic systems},
month = sep,
number = {38},
pages = {5095--5110},
pmid = {21998490},
title = {Probabilistic systems coalgebraically: A survey},
volume = {412},
year = {2011}
}
@article{Jonsson1952,
author = {J{\'{o}}nsson, Bjarni and Tarski, Alfred},
journal = {Am. J. Math.},
number = {1},
pages = {127--162},
title = {Boolean algebras with operators},
volume = {74},
year = {1952}
}
@inproceedings{Narayanan2009,
archivePrefix = {arXiv},
arxivId = {0903.3276},
author = {Narayanan, Arvind and Shmatikov, Vitaly},
booktitle = {2009 30th IEEE Symp. Secur. Priv.},
doi = {10.1109/SP.2009.22},
eprint = {0903.3276},
isbn = {978-0-7695-3633-0},
issn = {10816011},
month = may,
pages = {173--187},
pmid = {26482121},
publisher = {IEEE},
title = {De-anonymizing Social Networks},
year = {2009}
}
@article{Day1977,
author = {Day, Brian J.},
doi = {10.1017/S0004972700023509},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = apr,
number = {03},
pages = {427--448},
title = {Density presentations of functors},
volume = {16},
year = {1977}
}
@article{Ulmer1968a,
author = {Ulmer, Friedrich},
doi = {10.1016/0021-8693(68)90037-9},
issn = {00218693},
journal = {J. Algebr.},
month = jan,
number = {1},
pages = {96--129},
title = {Representable functors with values in arbitrary categories},
volume = {8},
year = {1968}
}
@inproceedings{Bonchi2015a,
address = {New York, New York, USA},
author = {Bonchi, Filippo and Sobocinski, Pawel and Zanasi, Fabio},
booktitle = {Proc. 42nd Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '15},
doi = {10.1145/2676726.2676993},
isbn = {9781450333009},
issn = {15232867},
keywords = {a simple mathematical meaning,at least,can be given to,full abstraction,it is,one delay component,props,signal flow graphs,string diagrams,struc-,those sfgs,tural operational semantics,where feedbacks pass through},
pages = {515--526},
publisher = {ACM Press},
title = {Full abstraction for signal flow graphs},
year = {2015}
}
@article{Im2009,
abstract = {An adjoint-triangle theorem contemplates functors P: C → A and T: A → B where T and TP have left adjoints, and gives sufficient conditions for P also to have a left adjoint. We are concerned with the case where T is conservative - that is, isomorphism-reflecting; then P has a left adjoint under various combinations of completeness or cocompleteness conditions on C and A, with no explicit condition on P itself. We list systematically the strongest results we know of in this direction, augmenting those in the literature by some new ones.},
author = {Im, G. B. and Kelly, Gregory Maxwell},
doi = {10.1017/S000497270002637X},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
month = apr,
number = {01},
pages = {133},
title = {Adjoint-triangle theorems for conservative functors},
volume = {36},
year = {2009}
}
@article{Kreuzer2013,
author = {Bauer, Andrej and Pretnar, Matija},
doi = {10.2168/LMCS-10(4:9)2014},
editor = {Milius, Stefan},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,bounded variation,compactness,computational analysis,reverse mathematics},
month = dec,
number = {4},
pages = {1--15},
title = {An Effect System for Algebraic Effects and Handlers},
volume = {10},
year = {2014}
}
@article{Shulman2008a,
abstract = {In some bicategories, the 1-cells are 'morphisms' between the 0-cells, such as functors between categories, but in others they are 'objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the 'morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change 'nonalgebraically', us-ing categorical fibrations. The resulting 'framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a 'monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.},
archivePrefix = {arXiv},
arxivId = {0706.1286},
author = {Shulman, Michael},
eprint = {0706.1286},
journal = {Theory Appl. Categ.},
number = {18},
pages = {650--738},
title = {Framed bicategories and monoidal fibrations},
volume = {20},
year = {2008}
}
@article{Dubuc1974,
author = {Dubuc, Eduardo J.},
doi = {10.1016/0021-8693(74)90095-7},
issn = {00218693},
journal = {J. Algebr.},
month = may,
number = {2},
pages = {208--228},
publisher = {Elsevier},
title = {Free monoids},
volume = {29},
year = {1974}
}
@book{Gabbay2005,
address = {Berlin/Heidelberg},
doi = {10.1007/1-4020-3092-4},
edition = {2},
editor = {Gabbay, Dov M. and Guenthner, F.},
isbn = {1-4020-3091-6},
pages = {372},
publisher = {Springer Netherlands},
series = {Handbook of Philosophical Logic},
title = {Handbook of Philosophical Logic},
volume = {12},
year = {2005}
}
@article{Walukiewicz2000,
abstract = {Propositional $\mu$-calculus is an extension of the propositional modal logic with the least fixpoint operator. In the paper introducing the logic Kozen posed a question about completeness of the axiomatisation which is a small extension of the axiomatisation of the model system K. It is shown that this axiomatisation is complete.},
author = {Walukiewicz, Igor},
doi = {10.1006/inco.1999.2836},
isbn = {0-8186-7050-9},
issn = {08905401},
journal = {Inf. Comput.},
number = {1-2},
pages = {142--182},
title = {Completeness of Kozen's axiomatisation of the propositional $\mu$-calculus},
volume = {157},
year = {2000}
}
@article{Street1980a,
author = {Street, Ross},
journal = {Cah. Topol. G{\'{e}}om. Diff{\'{e}}rentielle},
number = {2},
pages = {111--160},
title = {Fibrations in bicategories bicategories},
volume = {21},
year = {1980}
}
@article{DiNola2005,
abstract = {We define the entropy, lower and upper entropy, and the conditional entropy of a dynamical system consisting of an effect algebra with the Riesz decomposition property, a state, and a transformation. Such effect algebras allow many refinements of two partitions. We present the basic properties of these entropies and these notions are illustrated

license_type: permissive

branch_name: refs/heads/master

extension: bib