text:
of economic value despite only cursory analysis of the system's design. Since then a growing literature has identified hidden-but-important properties of the system, discovered attacks, proposed promising alternatives, and singled out difficult future challenges. Meanwhile a large and vibrant open-source community has proposed and deployed numerous modifications and extensions. We provide the first systematic exposition Bitcoin and the many related cryptocurrencies or ‘altcoins.' Drawing from a scattered body of knowledge, we identify three key components of Bitcoin's design that can be decoupled. This enables a more insightful analysis of Bitcoin's properties and future stability. We map the design space for numerous proposed modifications, providing comparative analyses for alternative consensus mechanisms, currency allocation mechanisms, computational puzzles, and key management tools. We survey anonymity issues in Bitcoin and provide an evaluation framework for analyzing a variety of privacy-enhancing proposals. Finally we provide new insights on what we term disintermediation protocols, which absolve the need for trusted intermediaries in an interesting set of applications. We identify three general disintermediation strategies and provide a detailed comparison.},
author = {Bonneau, Joseph and Miller, Andrew and Clark, Jeremy and Narayanan, Arvind and Kroll, Joshua A. and Felten, Edward W.},
doi = {10.1109/SP.2015.14},
isbn = {9781467369497},
issn = {10816011},
journal = {Proc. - IEEE Symp. Secur. Priv.},
pages = {104--121},
title = {SoK: Research perspectives and challenges for bitcoin and cryptocurrencies},
volume = {2015-July},
year = {2015}
}
@inproceedings{Urabe2016,
address = {Dagstuhl, Germany},
author = {Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
booktitle = {27th Int. Conf. Concurr. Theory (CONCUR 2016)},
doi = {http://dx.doi.org/10.4230/LIPIcs.CONCUR.2016.24},
editor = {Desharnais, Jos{\'{e}}e and Jagadeesan, Radha},
isbn = {978-3-95977-017-0},
issn = {1868-8969},
pages = {24:1----24:15},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Coalgebraic trace semantics for B{\"{u}}chi and parity automata},
volume = {59},
year = {2016}
}
@article{Silva2013,
abstract = {The powerset construction is a standard method for converting a nondeterministic automaton into a deterministic one recognizing the same language. In this paper, we lift the powerset construction from automata to the more general framework of coalgebras with structured state spaces. Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the type of systems (F-coalgebras) and a notion of behavioural equivalence ($\sim$_F) amongst them. Many types of transition systems and their equivalences can be captured by a functor F. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. We give several examples of applications of our generalized determinization construction, including partial Mealy machines, (structured) Moore automata, Rabin probabilistic automata, and, somewhat surprisingly, even pushdown automata. To further witness the generality of the approach we show how to characterize coalgebraically several equivalences which have been object of interest in the concurrency community, such as failure or ready semantics.},
archivePrefix = {arXiv},
arxivId = {1302.1046},
author = {Silva, Alexandra and Bonchi, Filippo and Bonsangue, Marcello M. and Rutten, Jan J.M.M.},
doi = {10.2168/LMCS-9(1:9)2013},
eprint = {1302.1046},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,coalgebras,linear semantics,powerset construction},
month = feb,
pages = {1--27},
title = {Generalizing determinization from automata to coalgebras},
volume = {9},
year = {2013}
}
@article{Barr1992,
author = {Barr, Michael},
doi = {10.1016/0022-4049(92)90169-G},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = oct,
number = {3},
pages = {211--231},
title = {Algebraically compact functors},
volume = {82},
year = {1992}
}
@article{Kennison1971,
author = {Kennison, John F. and Gildenhuys, Dion},
doi = {10.1016/0022-4049(71)90001-6},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {4},
pages = {317--346},
title = {Equational completion, model induced triples and pro-objects},
volume = {1},
year = {1971}
}
@article{Barr2002,
author = {Barr, Michael},
journal = {Theory Appl. Categ.},
keywords = {birkhoff subcategories,factorizations,reflective subcategories},
number = {18},
pages = {461--468},
title = {HSP Subcategories of Eilenberg-Moore Algebras},
volume = {10},
year = {2002}
}
@inproceedings{Ganta2008,
abstract = {Privacy is an increasingly important aspect of data publishing. Reasoning about privacy, however, is fraught with pitfalls. One of the most significant is the auxiliary information (also called external knowledge, background knowledge, or side information) that an adversary gleans from other channels such as the web, public records, or domain knowledge. This paper explores how one can reason about privacy in the face of rich, realistic sources of auxiliary information. Specifically, we investigate the effectiveness of current anonymization schemes in preserving privacy when multiple organizations independently release anonymized data about overlapping populations. 1. We investigate composition attacks, in which an adversary uses independent anonymized releases to breach privacy. We explain why recently proposed models of limited auxiliary information fail to capture composition attacks. Our experiments demonstrate that even a simple instance of a composition attack can breach privacy in practice, for a large class of currently proposed techniques. The class includes k-anonymity and several recent variants. 2. On a more positive note, certain randomization-based notions of privacy (such as differential privacy) provably resist composition attacks and, in fact, the use of arbitrary side information.This resistance enables ``stand-alone'' design of anonymization schemes, without the need for explicitly keeping track of other releases. We provide a precise formulation of this property, and prove that an important class of relaxations of differential privacy also satisfy the property. This significantly enlarges the class of protocols known to enable modular design.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {0803.0032},
author = {Ganta, Srivatsava Ranjit and Kasiviswanathan, Shiva Prasad and Smith, Adam},
booktitle = {Proceeding 14th ACM SIGKDD Int. Conf. Knowl. Discov. data Min. - KDD 08},
doi = {10.1145/1401890.1401926},
eprint = {0803.0032},
isbn = {9781605581934},
keywords = {adversarial attacks,anonymization,privacy},
pages = {265},
publisher = {ACM Press},
title = {Composition attacks and auxiliary information in data privacy},
year = {2008}
}
@book{Roscoe1997,
abstract = {From the Publisher: Since the introduction of Hoares' Communicating Sequential Processes notation, powerful new tools have transformed CSP into a practical way of describing industrial-sized problems. This book gives you the fundamental grasp of CSP concepts you'll need to take advantage of those tools.Part I provides a detailed foundation for working with CSP, using as little mathematics as possible. It introduces the ideas behind operational, denotational and algebraic models of CSP. Parts II and III go into greater detail about theory and practice. Topics include&58; parallel operators, hiding and renaming, piping and enslavement, buffers and communication, termination and sequencing, and semantic theory. Three detailed practical case studies are also presented.For anyone interested in modeling sequential processes.},
author = {Roscoe, A. William},
isbn = {0136744095},
pages = {512},
publisher = {Prentice Hall},
series = {Prentice Hall Internationa Series in Computer Science},
title = {The Theory and Practice of Concurrency},
year = {1997}
}
@incollection{Damgard2007,
abstract = {In this paper, we identify some issues in the interplay between practice and theory in cryptography, issues that have repeatedly appeared in different incarnations over the years. These issues are related to fundamental concepts in the field, e.g., to what extent we can prove that a system is secure and what theoretic results on security mean for practical applications. We argue that several such issues are often overlooked or misunderstood, and that it may be very productive if both theoreticians and practitioners think more consciously about these issues and act accordingly.},
address = {Berlin, Heidelberg},
author = {Damg{\aa}rd, Ivan},
booktitle = {Autom. Lang. Program.},
doi = {10.1007/978-3-540-73420-8_2},
isbn = {978-3-540-73419-2, 978-3-540-73420-8},
issn = {03029743},
pages = {2--11},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A “proof-reading” of some issues in cryptography},
volume = {4596},
year = {2007}
}
@article{Smyth1983a,
author = {Smyth, Michael B.},
doi = {10.1007/BFb0036946},
editor = {Diaz, Josep},
journal = {Autom. Lang. Program.},
pages = {662--675},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Power domains and predicate transformers: A topological view},
type = {Journal article},
volume = {154},
year = {1983}
}
@incollection{Suenaga2011,
author = {Suenaga, Kohei and Hasuo, Ichiro},
booktitle = {Autom. Lang. Program.},
doi = {10.1007/978-3-642-22012-8_31},
editor = {Aceto, Luca and Henzinger, Monika and {Jiř{\'{i}} Sgall}},
pages = {392--403},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Programming with Infinitesimals: A While-Language for Hybrid System Modeling},
year = {2011}
}
@misc{Carboni1997,
abstract = {If (e, M )is a factorization system on a category C , we define new classes of maps as follows: a map f : A ? B is in e' if each of its pullbacks lies in e(that is, if it is stably in e), and is in M * if some pullback of it along an effective descent map lies in M (that is, if it is locally in M ). We find necessary and sufficient conditions for (e', M * ) to be another factorization system, and show that a number of interesting factorization systems arise in this way. We further make the connexion with Galois theory, where M * is the class of coverings; and include self-contained modern accounts of factorization systems, descent theory, and Galois theory.},
author = {Carboni, Aurelio and Janelidze, George and Kelly, Gregory Maxwell and Par{\'{e}}, Robert},
booktitle = {Appl. Categ. Struct.},
doi = {10.1023/A:1008620404444},
issn = {0927-2852},
keywords = {Mathematics and Statistics},
month = mar,
number = {1},
pages = {1--58},
publisher = {Springer Netherlands},
title = {On Localization and Stabilization for Factorization Systems},
url = {http://www.springerlink.com/content/x772343118423746/},
volume = {5},
year = {1997}
}
@article{Bergner2006,
abstract = {In this paper we give a summary of the comparisons between different definitions of so-called (\infty,1)-categories, which are considered to be models for \infty-categories whose n-morphisms are all invertible for n>1. They are also, from the viewpoint of homotopy theory, models for the homotopy theory of homotopy theories. The four different structures, all of which are equivalent, are simplicial categories, Segal categories, complete Segal spaces, and quasi-categories.},
archivePrefix = {arXiv},
arxivId = {math/0610239},
author = {Bergner, Julia E},
eprint = {0610239},
journal = {ArXiv e-prints},
month = oct,
pages = {13},
primaryClass = {math},
title = {A survey of (\infty, 1)-categories},
year = {2006}
}
@incollection{Hasuo2011,
author = {Hasuo, Ichiro},
booktitle = {4th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/978-3-642-22944-2_16},
editor = {Corradini, Andrea and Klin, Bartek and C{\^{i}}rstea, Corina},
pages = {222--236},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {The Microcosm Principle and Compositionality of GSOS-Based Component Calculi},
year = {2011}
}
@article{Staton2011,
author = {Staton, Sam},
doi = {10.2168/LMCS-7(1:13)2011},
editor = {Kurz, Alexander},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,bisimulation,category theory,coalgebra,coinduction},
month = mar,
number = {1},
pages = {1--21},
title = {Relating coalgebraic notions of bisimulation},
volume = {7},
year = {2011}
}
@article{Pattinson2001,
author = {Pattinson, Dirk},
doi = {10.1016/S1571-0661(04)80913-7},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = may,
number = {1},
pages = {271--284},
title = {Modal Languages for Coalgebras in a Topological Setting},
volume = {44},
year = {2001}
}
@article{Hutton1999,
abstract = {In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as a proof principle that avoids the need for inductive proofs, and as a definition principle that guides the transformation of recursive functions into definitions using fold. Secondly, we show that even though the pattern of recursion encapsulated by fold is simple, in a language with tuples and functions as first-class values the fold operator has greater expressive power than might first be expected.},
author = {Hutton, Graham},
doi = {10.1017/S0956796899003500},
issn = {09567968},
journal = {J. Funct. Program.},
month = jul,
number = {4},
pages = {355--372},
title = {A tutorial on the universality and expressiveness of fold},
volume = {9},
year = {1999}
}
@book{Kanamori2003,
address = {Berlin, Heidelberg},
author = {Kanamori, Akihiro},
doi = {10.1007/978-3-540-88867-3},
edition = {2},
isbn = {978-3-540-88866-6},
issn = {1439-7382},
pages = {536},
publisher = {Springer Berlin Heidelberg},
series = {Springer Monographs in Mathematics},
title = {The Higher Infinite},
year = {2003}
}
@incollection{Garay2015,
abstract = {We present a novel method for constructing linear secret sharing schemes (LSSS) from linear error correcting codes and linear universal hash functions in a blackbox way. The main advantage of this new construction is that the privacy property of the resulting secret sharing scheme essentially becomes independent of the code we use, only depending on its rate. This allows us to fully harness the algorithmic properties of recent code constructions such as efficient encoding and decoding or efficient list-decoding. Choosing the error correcting codes and universal hash functions involved carefully, we obtain solutions to the following open problems: – A linear near-threshold secret sharing scheme with both linear time sharing and reconstruction algorithms and large secrets (i.e. secrets of size $\Omega$(n)). Thus, the computational overhead per shared bit in this scheme is constant. – An efficiently reconstructible robust secret sharing scheme for n/3 ≤ t < (1−){\textperiodcentered}n/2 corrupted players (for any constant > 0) with shares of optimal size O(1 + $\lambda$/n) and secrets of size $\Omega$(n + $\lambda$), where $\lambda$ is the security parameter.},
address = {Berlin, Heidelberg},
author = {Garay, Juan and Kiayias, Aggelos and Leonardos, Nikos},
booktitle = {Adv. Cryptol. - EUROCRYPT 2015 34th Annu. Int. Conf. Theory Appl. Cryptogr. Tech. Sofia, Bulg. April 26-30, 2015, Proceedings, Part II},
doi = {10.1007/978-3-662-46803-6_10},
editor = {Oswald, Elisabeth and Fischlin, Marc},
isbn = {978-3-662-46803-6},
issn = {16113349},
pages = {281--310},
publisher = {Springer Berlin Heidelberg},
title = {The bitcoin backbone protocol: Analysis and applications},
volume = {9057},
year = {2015}
}
@article{Schroder2008,
abstract = {Modal logic has a good claim to being the logic of choice for describing the reactive behaviour of systems modeled as coalgebras. Logics with modal operators obtained from so-called predicate liftings have been shown to be invariant under behavioral equivalence. Expressivity results stating that, conversely, logically indistinguishable states are behaviorally equivalent depend on the existence of separating sets of predicate liftings for the signature functor at hand. Here, we provide a classification result for predicate liftings which leads to an easy criterion for the existence of such separating sets, and we give simple examples of functors that fail to admit expressive normal or monotone modal logics, respectively, or in fact an expressive (unary) modal logic at all. We then move on to polyadic modal logic, where modal operators may take more than one argument formula. We show that every accessible functor admits an expressive polyadic modal logic. Moreover, expressive polyadic modal logics are, unlike unary modal logics, compositional.},
author = {Schr{\"{o}}der, Lutz},
doi = {10.1016/j.tcs.2007.09.023},
editor = {Sassone, Vladimiro},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {coalgebra,expressivity,modal logic,predicate lifting},
number = {2-3},
pages = {230--247},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
title = {Expressivity of coalgebraic modal logic: The limits and beyond},
volume = {390},
year = {2008}
}
@incollection{Hughes2003,
author = {Hughes, Jesse and Jacobs, Bart},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/S1571-0661(04)80564-4},
issn = {15710661},
month = feb,
pages = {156--182},
title = {Factorization systems and fibrations},
volume = {69},
year = {2003}
}
@article{Chikhladze2015,
author = {Chikhladze, Dimitri},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Bicategories,Equipments,Formal theory of monads,Generalized multicategories,Lax categorification,Tricategories},
number = {10},
pages = {332--386},
title = {Lax formal theory of monads, monoidal approach to bicategorical structures and generalized operads},
volume = {30},
year = {2015}
}
@article{Manes2007,
author = {Manes, Ernie and Mulry, Philip S.},
journal = {Theory Appl. Categ.},
keywords = {2007,and phrases,c ernie manes and,distributive law,linear equation,permission to copy for,philip mulry,private use granted},
number = {7},
pages = {172--208},
title = {Monad compositions I: general constructions and recursive distributive laws},
volume = {18},
year = {2007}
}
@incollection{Beck1969,
author = {Beck, Jon},
booktitle = {Semin. Triples Categ. Homol. Theory},
doi = {10.1007/BFb0083084},
editor = {Eckmann, B.},
pages = {119--140},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Distributive Laws},
year = {1969}
}
@article{Milius2009,
abstract = {This paper provides a general account of the notion of recursive program schemes, studying both uninterpreted and interpreted solutions. It can be regarded as the category-theoretic version of the classical area of algebraic semantics. The overall assumptions needed are small indeed: working only in categories with "enough final coalgebras" we show how to formulate, solve, and study recursive program schemes. Our general theory is algebraic and so avoids using ordered, or metric structures. Our work generalizes the previous approaches which do use this extra structure by isolating the key concepts needed to study substitution in infinite trees, including second-order substitution. As special cases of our interpreted solutions we obtain the usual denotational semantics using complete partial orders, and the one using complete metric spaces. Our theory also encompasses implicitly defined objects which are not usually taken to be related to recursive program schemes. For example, the classical Cantor two-thirds set falls out as an interpreted solution (in our sense) of a recursive program scheme.},
archivePrefix = {arXiv},
arxivId = {0904.2385},
author = {Milius, Stefan and Moss, Lawrence S.},
eprint = {0904.2385},
journal = {ArXiv e-prints},
number = {March},
pages = {1--54},
title = {The Category Theoretic Solution of Recursive Program Schemes},
year = {2009}
}
@article{Haenni2004,
abstract = {The paper presents a generic approach of approximating inference. The method is based on the concept of valuation algebras with its wide range of possible applications in many different domains. We present convenient resource-bounded anytime algorithms, where the maximal time of computation is determined by the user. {\textcopyright} 2003 Elsevier Inc. All rights reserved.},
author = {Haenni, Rolf},
doi = {10.1016/j.ijar.2003.10.009},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Anytime algorithms,Approximation,Binary join trees,Bucket elimination,Local computation,Mini-buckets,Resource-bounded computation,Valuation algebras},
month = aug,
number = {1},
pages = {1--41},
title = {Ordered valuation algebras: a generic framework for approximating inference},
volume = {37},
year = {2004}
}
@incollection{Chen2015a,
abstract = {Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman's theorem states that they precisely specify pseudovarieties, i.e. classes of finite algebras closed under finite products, subalgebras and quotients. In this paper Reiterman's theorem is generalised to finite Eilenberg-Moore algebras for a monad T on a variety D of (ordered) algebras: a class of finite T-algebras is a pseudovariety iff it is presentable by profinite (in-)equations. As an application, quasivarieties of finite algebras are shown to be presentable by profinite implications. Other examples include finite ordered algebras, finite categories, finite infinity-monoids, etc.},
archivePrefix = {arXiv},
arxivId = {1511.02147},
author = {Chen, Liang-Ting and Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Urbat, Henning},
booktitle = {Proc. 19th Int. Conf. Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-662-49630-5_31},
editor = {Jacobs, Bart and L{\"{o}}ding, Christof},
eprint = {1511.02147},
pages = {531--547},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Profinite monads, profinite equations, and Reiterman's theorem},
volume = {9634},
year = {2016}
}
@incollection{Walt2013,
author = {Walt, Paul Van Der and Swierstra, Wouter},
booktitle = {Implement. Appl. Funct. Lang.},
doi = {10.1007/978-3-642-41582-1_10},
editor = {Hinze, Ralf},
isbn = {978-3-642-41581-4},
issn = {0302-9743},
keywords = {agda,dependently-typed programming,metaprogramming,proof by,reflection},
pages = {157--173},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Engineering Proof by Reflection in Agda},
year = {2013}
}
@article{Hoyrup2009,
abstract = {In this paper, we investigate algorithmic randomness on more general spaces than the Cantor space, namely computable metric spaces. To do this, we first develop a unified framework allowing computations with probability measures. We show that any computable metric space with a computable probability measure is isomorphic to the Cantor space in a computable and measure-theoretic sense. We show that any computable metric space admits a universal uniform randomness test (without further assumption). {\textcopyright} 2009 Elsevier Inc. All rights reserved.},
author = {Hoyrup, Mathieu and Rojas, Crist{\'{o}}bal},
doi = {10.1016/j.ic.2008.12.009},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Algorithmic randomness,Almost computable function,Computability,Computable metric space,Computable probability measure,Enumerative lattice,Kolmogorov-Chaitin complexity,Universal test},
month = jul,
number = {7},
pages = {830--847},
publisher = {Elsevier Inc.},
title = {Computability of probability measures and Martin-L{\"{o}}f randomness over metric spaces},
volume = {207},
year = {2009}
}
@article{Lack1999,
author = {Lack, Stephen},
doi = {10.1016/S0022-4049(99)00019-5},
isbn = {6129351453},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {1},
pages = {65--73},
title = {On the monadicity of finitary monads},
volume = {140},
year = {1999}
}
@article{Adamek2004,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Velebil, Jiř{\'{i}}},
doi = {10.1016/j.tcs.2003.12.022},
issn = {0304-3975},
journal = {Theor. Comput. Sci.},
keywords = {Category of classes,Iterative monad,Set-based endofunctor,Terminal coalgebra,category,classes,coalgebra,endofunctor,iterative,monad,of,set-based,terminal},
mendeley-tags = {category,classes,coalgebra,endofunctor,iterative,monad,of,set-based,terminal},
month = may,
number = {1-3},
pages = {3--23},
title = {On coalgebra based on classes},
type = {Journal article},
volume = {316},
year = {2004}
}
@article{Jacobs2004,
abstract = {Traditionally, traces are the sequences of labels associated with paths in transition systems X → P(A × X). Here we describe traces more generally, for coalgebras of the form X → P(F(X)), where F is a polynomial functor. The main result states that F's final coalgebra Z ≅→ F(Z) gives rise to a weakly final coalgebra with state space P(Z), in a suitable category of coalgebras. Weak finality means that there is a coalgebra map X → P(Z), but there is no uniqueness. We show that there is a canonical choice among these maps X → P(Z), namely the largest one, describing the traces in a suitably abstract formulation. A crucial technical ingredient in our construction is a general distributive law FP ⇒ PF, obtained via relation lifting.},
author = {Jacobs, Bart},
doi = {10.1016/j.entcs.2004.02.031},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Coalgebra,Distributive law,Final coalgebra,Polynomial functor,Trace semantics},
month = dec,
pages = {167--184},
title = {Trace semantics for coalgebras},
volume = {106},
year = {2004}
}
@article{Fiore1993,
abstract = {The concept of bisimulation from concurrency\ntheory$\sim$\cite{Park81,Milner89} is used to reason about\nrecursively defined data types. From two\nstrong-extensionality theorems stating that the\nequality (resp.\ inequality) relation is maximal among\nall bisimulations, a proof principle for the final\ncoalgebra of an endofunctor on a category of data types\n(resp.\ domains) is obtained. As an application of the\ntheory developed, an internal full abstraction result\n(in the sense of$\sim$\cite{AbramskyOng92}) for the\ncanonical model of the untyped call-by-value\n$\lambda$-calculus is proved. \par Also, the\noperational notion of bisimulation and the denotational\nnotion of final semantics are related by means of\nconditions under which both coincide.},
author = {Fiore, Marcelo P.},
doi = {10.1006/inco.1996.0058},
isbn = {0818631422},
issn = {08905401},
journal = {Inf. Comput.},
month = jun,
number = {2},
pages = {186--198},
title = {A Coinduction Principle for Recursive Data Types Based on Bisimulation},
volume = {127},
year = {1996}
}
@article{Tschantz2011a,
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. This paper presents the first results towards automated verification of source code for differentially private interactive systems. We develop a formal probabilistic automaton model of differential privacy for systems by adapting prior work on differential privacy for functions. The main technical result of the paper is a sound proof technique based on a form of probabilistic bisimulation relation for proving that a system modeled as a probabilistic automaton satisfies differential privacy. 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. To make our proof technique easier to apply to realistic systems, we prove a form of refinement theorem and apply it to show that a refinement of the abstract PINQ automaton also satisfies our differential privacy definition. Finally, we begin the process of automating our proof technique by providing an algorithm for mechanically checking a restricted class of relations from the proof technique.},
archivePrefix = {arXiv},
arxivId = {1101.2819},
author = {Tschantz, Michael Carl and Kaynar, Dilsun and Datta, Anupam},
doi = {10.1016/j.entcs.2011.09.015},
eprint = {1101.2819},
issn = {15710661},
journal = {ArXiv Prepr.},
keywords = {Bisimulation,Differential Privacy,Formal Methods,Privacy,Verification},
month = jan,
title = {Formal verification of differential privacy for interactive systems},
year = {2011}
}
@article{Li2014,
abstract = {Personal data has value to both its owner and to institutions who would like to analyze it. Privacy mechanisms protect the owner's data while releasing to analysts noisy versions of aggregate query results. But such strict protections of individual's data have not yet found wide use in practice. Instead, Internet companies, for example, commonly provide free services in return for valuable sensitive information from users, which they exploit and sometimes sell to third parties. As the awareness of the value of the personal data in- creases, so has the drive to compensate the end user for her private information. The idea of monetizing private data can improve over the narrower view of hiding private data, since it empowers individuals to control their data through financial means. In this paper we propose a theoretical framework for as- signing prices to noisy query answers, as a function of their accuracy, and for dividing the price amongst data owners who deserve compensation for their loss of privacy. Our framework adopts and extends key principles from both dif- ferential privacy and query pricing in data markets. We identify essential properties of the price function and micro- payments, and characterize valid solutions.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {arXiv:1208.5258v2},
author = {Li, Chao and Li, Daniel Yang and Miklau, Gerome and Suciu, Dan},
doi = {10.1145/3139457},
eprint = {arXiv:1208.5258v2},
isbn = {9781450315982},
issn = {00010782},
journal = {Commun. ACM},
keywords = {arbitrage,data pricing,differential privacy},
month = nov,
number = {12},
pages = {79--86},
publisher = {ACM Press},
title = {A theory of pricing private data},
volume = {60},
year = {2017}
}
@article{Santocanale2010a,
abstract = {This paper exhibits a general and uniform method to prove axiomatic completeness for certain modal fixpoint logics. Given a set ?? of modal formulas of the form ??(x,p1,. . .,pn), where x occurs only positively in ??, we obtain the flat modal fixpoint language L#(??) by adding to the language of polymodal logic a connective #?? for each ???????. The term #??(??1,. . .,??n) is meant to be interpreted as the least fixed point of the functional interpretation of the term ??(x,??1,. . .,??n). We consider the following problem: given ??, construct an axiom system which is sound and complete with respect to the concrete interpretation of the language L#(??) on Kripke structures. We prove two results that solve this problem.First, let K#(??) be the logic obtained from the basic polymodal K by adding a Kozen-Park style fixpoint axiom and a least fixpoint rule, for each fixpoint connective #??. Provided that each indexing formula ?? satisfies a certain syntactic criterion, we prove this axiom system to be complete.Second, addressing the general case, we prove the soundness and completeness of an extension K#+(??) of K#(??). This extension is obtained via an effective procedure that, given an indexing formula ?? as input, returns a finite set of axioms and derivation rules for #??, of size bounded by the length of ??. Thus the axiom system K#+(??) is finite whenever ?? is finite. ?? 2010 Elsevier B.V.},
archivePrefix = {arXiv},
arxivId = {0812.2390},
author = {Santocanale, Luigi and Venema, Yde},
doi = {10.1016/j.apal.2010.07.003},
eprint = {0812.2390},
isbn = {9783540755586},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {Axiomatization,Completeness,Fixpoint logic,Modal algebra,Modal logic,Representation theorem},
number = {1},
pages = {55--82},
publisher = {Elsevier B.V.},
title = {Completeness for flat modal fixpoint logics},
volume = {162},
year = {2010}
}
@techreport{Doberkat2012b,
abstract = {Parikh's game logic is a dynamic modal logic which models strategic two person games; it contains propositional dynamic logic (PDL) as a fragment. We propose a stochastic interpretation for the distributive variant of this logic based on stochastic Kripke models. The important operator which sets this logic apart from PDL is demonization, which receives due attention. The relationship of logical and behavioral equivalence of Kripke models is investigated.},
author = {Doberkat, Ernst-Erich},
institution = {Software Technology and Department of Mathematics Technische Universit{\"{a}}t Dortmund},
month = apr,
pages = {20},
title = {A Stochastic Interpretation of Parikh's Game Logic},
year = {2012}
}
@techreport{Kurz2006,
address = {M{\'{a}}laga},
author = {Kurz, Alexander},
month = oct,
title = {Coalgebras, Stone duality, modal Logic},
year = {2006}
}
@incollection{Manes2003,
author = {Manes, Ernie},
booktitle = {Handb. Algebr.},
doi = {10.1016/S1570-7954(03)80059-1},
editor = {Hazewinkel, M.},
isbn = {978-0444512642},
pages = {67--153},
publisher = {North Holland},
title = {Monads of sets},
volume = {3},
year = {2003}
}
@article{Urabe2016c,
abstract = {Notions of simulation, among other uses, provide a computationally tractable and sound (but not necessarily complete) proof method for language inclusion. They have been comprehensively studied by Lynch and Vaandrager for nondeterministic and timed systems; for (nondeterministic) Buechi automata the notion of fair simulation has been introduced by Henzinger, Kupferman and Rajamani. We contribute generalization of fair simulation in two different directions: one for nondeterministic tree automata (this has been studied previously by Bomhard); and the other for probabilistic word automata (with a finite state space), both under the Buechi acceptance condition. The former (nondeterministic) definition is formulated in terms of systems of fixed-point equations, hence is readily translated to parity games and then amenable to Jurdzinski's algorithm; the latter (probabilistic) definition bears a strong ranking-function flavor. These two different-looking definitions are derived from one source, namely our coalgebraic modeling of Buechi automata; the proofs of soundness (i.e. that a simulation indeed witnesses language inclusion) are based on these coalgebraic observations, too.},
archivePrefix = {arXiv},
arxivId = {1606.04680},
author = {Urabe, Natsuki and Shimizu, Shunsuke and Hasuo, Ichiro},
eprint = {1606.04680},
journal = {ArXiv Prepr.},
keywords = {and phrases},
month = jun,
pages = {1--33},
title = {Fair simulation for nondeterministic and probabilistic B{\"{u}}chi automata: a coalgebraic perspective},
year = {2016}
}
@incollection{Rosebrugh1978,
author = {Rosebrugh, Robert},
booktitle = {Index. Categ. Their Appl.},
doi = {10.1007/BFb0061364},
pages = {243--260},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Coequalizers in algebras for an internal type},
year = {1978}
}
@article{Meng2005,
abstract = {This paper introduces a generic semantic framework for component-based development, expressed in the unified modelling language UML. The principles of a coalgebraic semantics for class, object and statechart diagrams as well as for use cases, are developed. It is also discussed how to formalize the refinement steps in the development process based upon a suitable notion of behavior refinement. In this way, a formal basis for component-based development in UML is studied, which allows the construction of more complex and specific systems from independent components. {\textcopyright} 2005 Published by Elsevier B.V.},
author = {Meng, Sun and Aichernig, Bernhard K. and Barbosa, Lu{\'{i}}s S. and Naixiao, Zhang},
doi = {10.1016/j.entcs.2004.06.051},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Coalgebras,Refinement,UML,Unified modeling language},
month = mar,
pages = {229--245},
title = {A coalgebraic semantic framework for component-based development in UML},
volume = {122},
year = {2005}
}
@article{Rosicky1981a,
author = {Rosick{\'{y}}, Jiř{\'{i}}},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {1},
pages = {85--95},
title = {Equational categories},
volume = {22},
year = {1981}
}
@article{Watanabe2002,
author = {Watanabe, Hiroshi},
doi = {10.1016/S1571-0661(04)80372-4},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {337--357},
title = {Well-behaved Translations between Structural Operational Semantics},
volume = {65},
year = {2002}
}
@inproceedings{Hasuo2013,
abstract = {Coinductive predicates express persisting "safety" specifications of transition systems. Previous observations by Hermida and Jacobs identify coinductive predicates as suitable final coalgebras in a fibration - a categorical abstraction of predicate logic. In this paper we follow the spirit of a seminal work by Worrell and study final sequences in a fibration. Our main contribution is to identify some categorical "size restriction" axioms that guarantee stabilization of final sequences after ?? steps. In its course we develop a relevant categorical infrastructure that relates fibrations and locally presentable categories, a combination that does not seem to be studied a lot. The genericity of our fibrational framework can be exploited for: binary relations (i.e. the logic of "binary predicates") for which a coinductive predicate is bisimilarity; constructive logics (where interests are growing in coinductive predicates); and logics for name-passing processes. ?? 2013 Elsevier B.V.},
author = {Hasuo, Ichiro and Cho, Kenta and Kataoka, Toshiki and Jacobs, Bart},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/j.entcs.2013.09.014},
issn = {15710661},
keywords = {(co)recursive predicate,coalgebra,fibration,locally presentable category,modal logic},
month = nov,
pages = {197--214},
publisher = {Elsevier B.V.},
title = {Coinductive predicates and final sequences in a fibration},
volume = {298},
year = {2013}
}
@article{Ellerman2017,
author = {Ellerman, David},
doi = {10.1093/jigpal/jzx022},
issn = {1367-0751},
journal = {Log. J. IGPL},
keywords = {logical entropy,partition logic,shannon entropy},
month = oct,
number = {5},
pages = {806--835},
title = {Logical information theory: new logical foundations for information theory},
volume = {25},
year = {2017}
}
@article{Bouyer2003,
abstract = {Algebra offers an elegant and powerful approach to understand regular languages and finite automata. Such framework has been notoriously lacking for timed languages and timed automata. We introduce the notion of monoid recognizability for data languages, which includes timed languages as special case, in a way that respects the spirit of the classical situation. We study closure properties and hierarchies in this model and prove that emptiness is decidable under natural hypotheses. Our class of recognizable languages properly includes many families of deterministic timed languages that have been proposed until now, and the same holds for non-deterministic versions. {\textcopyright} 2003 Elsevier Science (USA). All rights reserved.},
author = {Bouyer, Patricia and Petit, Antoine and Th{\'{e}}rien, Denis},
doi = {10.1016/S0890-5401(03)00038-5},
issn = {08905401},
journal = {Inf. Comput.},
month = may,
number = {2},
pages = {137--162},
title = {An algebraic approach to data languages and timed languages},
volume = {182},
year = {2003}
}
@incollection{Dwork2008b,
abstract = {We briefly survey several privacy compromises in published datasets, some historical and some on paper. An inspection of these suggests that the problem lies with the nature of the privacy-motivated promises in question. These are typically syntactic, rather than semantic. They are also ad hoc , with insufficient argument that fulfilling these syntactic and ad hoc conditions yields anything like what most people would regard as privacy. We examine two comprehensive, or ad omnia , guarantees for privacy in statistical databases discussed in the literature, note that one is unachievable, and describe implementations of the other.},
address = {Berlin, Heidelberg},
author = {Dwork, Cynthia},
booktitle = {Privacy, Secur. Trust KDD},
doi = {10.1007/978-3-540-78478-4_1},
isbn = {978-3-540-78477-7},
issn = {03029743},
keywords = {cryptography,differential,privacy},
pages = {1--13},
publisher = {Springer Berlin Heidelberg},
title = {An Ad Omnia Approach to Defining and Achieving Private Data Analysis},
volume = {4890},
year = {2008}
}
@incollection{Cox2014,
author = {Cox, Lawrence H},
booktitle = {Priv. Stat. Databases},
doi = {10.1007/978-3-319-11257-2_1},
editor = {Domingo-Ferrer, Josep},
isbn = {978-3-319-11256-5},
issn = {16113349},
keywords = {algebraic circuit,cell suppression,divergence},
pages = {1--10},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {Enabling Statistical Analysis of Suppressed Tabular Data},
volume = {8744},
year = {2014}
}
@article{Janelidze2001,
author = {Janelidze, George and Kelly, Gregory Maxwell},
journal = {Theory Appl. Categ.},
keywords = {2001,action,adjunction,and phrases,c g,enriched category,janelidze and g,kelly,m,monad,monoid,monoidal category,permission to copy for,private use granted},
number = {4},
pages = {61--91},
title = {A note on actions of a monoidal category},
volume = {9},
year = {2001}
}
@article{Jøsang2012,
author = {J{\o}sang, Audun and Pope, Simon},
doi = {10.1111/j.1467-8640.2012.00421.x},
issn = {08247935},
journal = {Comput. Intell.},
keywords = {averaging operator,belief theory,cumulative operator,fusion,subjective logic},
month = nov,
number = {4},
pages = {453--474},
title = {DEMPSTER'S RULE AS SEEN BY LITTLE COLORED BALLS},
volume = {28},
year = {2012}
}
@incollection{Street1974,
author = {Street, Ross},
booktitle = {Proc. Sydney Categ. Theory Semin. 1972/1973},
doi = {10.1007/BFb0063102},
editor = {Kelly, Gregory Maxwell},
pages = {104--133},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Fibrations and Yoneda's lemma in a 2-category},
year = {1974}
}
@article{Grandis2002,
abstract = {It is known that factorisation systems in categories can be viewed as unitary pseudo-algebras for the monad ??? = (-)2, in Cat. We show in this note that an analogous fact holds for proper (i.e., epi-mono) factorisation systems and a suitable quotient of the former monad, deriving from a construct introduced by Freyd for stable homotopy. Some similarities of ??? with the structure of the path endofunctor of topological spaces are considered. ?? 2002 Elsevier Science B.V. All rights reserved.},
archivePrefix = {arXiv},
arxivId = {math/0101154},
author = {Grandis, Marco},
doi = {10.1016/S0022-4049(01)00114-1},
eprint = {0101154},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {1},
pages = {17--26},
primaryClass = {math},
title = {On the monad of proper factorisation systems in categories},
volume = {171},
year = {2002}
}
@article{Adamek2007,
abstract = {Injectivity of objects with respect to a set $\ch$ of morphisms is an important concept of algebra, model theory and homotopy theory. Here we study the logic of injectivity consequences of $\ch$, by which we understand morphisms $h$ such that injectivity with respect to $\ch$ implies injectivity with respect to $h$. We formulate three simple deduction rules for the injectivity logic and for its finitary version where \mor s between finitely ranked objects are considered only, and prove that they are sound in all categories, and complete in all "reasonable" categories.},
archivePrefix = {arXiv},
arxivId = {0709.2461},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Hebert, M. and Sousa, Lurdes},
eprint = {0709.2461},
journal = {J. Homotopy Relat. Struct.},
number = {2},
pages = {13--47},
title = {A Logic of Injectivity},
volume = {2},
year = {2007}
}
@article{Davey2006,
author = {Davey, Brian A.},
journal = {Acta univ. M. Belii},
keywords = {natural duality,partial structure,topological partial structure},
number = {13},
pages = {3--28},
title = {Natural dualities for structures},
volume = {13},
year = {2006}
}
@article{Capretta2006,
abstract = {The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use of recursive coalgebras as a paradigm of structured recursion in programming semantics, list some basic facts about recursive coalgebras and, centrally, give new conditions for the recursiveness of a coalgebra based on comonads, comonad-coalgebras and distributive laws of functors over comonads. We also present an alternative construction using countable products instead of cofree comonads. {\textcopyright} 2006 Elsevier Inc. All rights reserved.},
author = {Capretta, Venanzio and Uustalu, Tarmo and Vene, Varmo},
doi = {10.1016/j.ic.2005.08.005},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Comonads,Distributive laws,Recursive coalgebras,Structured recursion,Wellfounded coalgebras},
month = apr,
number = {4},
pages = {437--468},
title = {Recursive coalgebras from comonads},
volume = {204},
year = {2006}
}
@techreport{Doberkat2012a,
abstract = {Bisimilarity is a key concept in the investigation of concurrent systems; it can be investigated coalgebraically, opening the road for the coalgebraic treatment of stochas- tic systems, which otherwise would be dicult to undertake. Markov transition systems model probabilistic systems in which the transition among states is represented by prob- abilistic laws. Stochastic relations lie at the mathematical heart of Markov transition systems. We show in this paper that a stochastic relation can be decomposed along a given congruence so that the parts are bisimilar (with the original relation as a mediat- ing component); this result is the bisimulation analogue to the classical decomposition of algebras through complementary congruences. We apply this technique also to Kripke models for modal logics.},
author = {Doberkat, Ernst-Erich},
institution = {Software Technology and Department of Mathematics Technische Universit{\"{a}}t Dortmund},
month = may,
pages = {18},
title = {Bisimulations For Structuring Markov Transition Systems},
year = {2012}
}
@book{Goldblatt2009a,
author = {Goldblatt, Robert},
edition = {Revised},
isbn = {0486450260},
publisher = {Dover Publications Inc.},
shorttitle = {Topoi},
title = {Topoi: The Categorial Analysis of Logic},
type = {Book},
year = {2009}
}
@phdthesis{Segala1995,
author = {Segala, Roberto},
school = {Massachusetts Institute of Technology},
title = {Modeling and Verification of Randomized Distributed Real-Time Systems},
year = {1995}
}
@article{Cirstea2011,
abstract = {This paper gives a general coalgebraic account of temporal logics whose semantics involves a notion of computation path. Examples of such logics include the logic CTL* for transition systems and the logic PCTL for probabilistic transition systems. Our path-based temporal logics are interpreted over coalgebras of endofunctors obtained as the composition of a computation type (e.g. non-deterministic or stochastic) with a general transition type. The semantics of such logics relies on the existence of execution maps similar to the trace maps introduced by Jacobs and co-authors as part of the coalgebraic theory of finite traces (Hasuo et al., 2007 [1]). We consider finite execution maps derived from the theory of finite traces, and a new notion of maximal execution map that accounts for maximal, possibly infinite executions. The latter is needed to recover the logics CTL* and PCTL as specific path-based logics. ?? 2011 Elsevier B.V. All rights reserved.},
author = {C{\^{i}}rstea, Corina},
doi = {10.1016/j.tcs.2011.04.025},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Coalgebra,Computation path,Non-determinism,Probability,Temporal logic,Trace semantics},
month = sep,
number = {38},
pages = {5025--5042},
publisher = {Elsevier B.V.},
title = {Maximal traces and path-based coalgebraic temporal logics},
volume = {412},
year = {2011}
}
@article{Goldreich1991a,
author = {Goldreich, Oded and Micali, Silvio and Wigderson, Avi},
doi = {10.1145/116825.116852},
editor = {Fischer-H{\"{u}}bner, Simone and Hopper, Nicholas},
issn = {00045411},
journal = {J. ACM},
month = jul,
number = {3},
pages = {690--728},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems},
volume = {38},
year = {1991}
}
@article{Isbell1968,
author = {Isbell, John R.},
doi = {10.1007/BF01691344},
issn = {0025-5661},
journal = {Math. Syst. Theory},
month = mar,
number = {1},
pages = {27--50},
title = {Small subcategories and completeness},
volume = {2},
year = {1968}
}
@article{Zhang2008,
abstract = {In order to describe approximate equivalence among processes, the notions of ??-bisimilarity and behavioural pseudometric have been introduced by Ying and van Breugel respectively. Van Breugel provides a distance function induced by ??-bisimilarity, and conjectures that his behavioural pseudometric coincides with this function. This paper is inspired by this conjecture. We give a negative answer for van Breugel's conjecture first. Moreover, we show that the distance function induced by ??-bisimilarity is a pseudometric on states, and provide a fixed point characterization of this pseudometric. ?? 2008 Elsevier B.V. All rights reserved.},
author = {Zhang, Jinjin and Zhu, Zhaohui},
doi = {10.1016/j.entcs.2008.11.022},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {??-bisimilarity,Process algebra,behavioural pseudometric,fixed point characterization},
month = dec,
number = {3},
pages = {115--127},
publisher = {Elsevier B.V.},
title = {A behavioural pseudometric based on $\lambda$–bisimilarity},
volume = {220},
year = {2008}
}
@book{Leinster2004,
abstract = {Higher-dimensional category theory is the study of n-categories, operads, braided monoidal categories, and other such exotic structures. It draws its inspiration from areas as diverse as topology, quantum algebra, mathematical physics, logic, and theoretical computer science. This is the first book on the subject and lays its foundations. The heart of this book is the language of generalized operads. This is as natural and transparent a language for higher category theory as the language of sheaves is for algebraic geometry, or vector spaces for linear algebra. It is introduced carefully, then used to give simple descriptions of a variety of higher categorical structures. In particular, one possible definition of n-category is discussed in detail, and some common aspects of other possible definitions are established. Many examples are given throughout. There is also an introductory chapter motivating the subject for topologists.},
archivePrefix = {arXiv},
arxivId = {arXiv:math/0305049v1},
author = {Leinster, Tom},
eprint = {0305049v1},
isbn = {0-521-53215-9},
primaryClass = {arXiv:math},
publisher = {Cambridge University Press},
series = {London Mathematical Society Lecture Note},
title = {Higher Operads , Higher Categories},
year = {2004}
}
@article{Cassidy1985,
author = {Cassidy, C. and H{\'{e}}bert, Michel and Kelly, Gregory Maxwell},
doi = {10.1017/S1446788700023624},
issn = {1446-7887},
journal = {J. Aust. Math. Soc.},
language = {English},
month = apr,
number = {03},
pages = {287},
title = {Reflective subcategories, localizations and factorization systems},
volume = {38},
year = {1985}
}
@book{Barr1985,
author = {Barr, Michael and Wells, Charles},
keywords = {and phrases,theories,toposes,triples},
number = {12},
pages = {1--288},
publisher = {Springer-Verlag},
title = {Toposes, triples and theories},
year = {1985}
}
@article{Adamek2005b,
author = {Ad{\'{a}}mek, Jiř{\'{i}}},
journal = {Comment. Math. Univ. Carolinae},
keywords = {classification,coequation},
number = {2},
pages = {197--215},
title = {Birkhoff's covariety theorem without limitations},
volume = {46},
year = {2005}
}
@article{Petricek2018,
abstract = {Computer science provides an in-depth understanding of technical aspects of programming concepts, but if we want to understand how programming concepts evolve, how programmers think and talk about them and how they are used in practice, we need to consider a broader perspective that includes historical, philosophical and cognitive aspects. In this paper, we develop such broader understanding of monads, a programming concept that has an infamous formal definition, syntactic support in several programming languages and a reputation for being elegant and powerful, but also intimidating and difficult to grasp. This paper is not a monad tutorial. It will not tell you what a monad is. Instead, it helps you understand how computer scientists and programmers talk about monads and why they do so. To answer these questions, we review the history of monads in the context of programming and study the development through the perspectives of philosophy of science, philosophy of mathematics and cognitive sciences. More generally, we present a framework for understanding programming concepts that considers them at three levels: formal, metaphorical and implementation. We base such observations on established results about the scientific method and mathematical entities -- cognitive sciences suggest that the metaphors used when thinking about monads are more important than widely accepted, while philosophy of science explains how the research paradigm from which monads originate influences and restricts their use. Finally, we provide evidence for why a broader philosophical, sociological look at programming concepts should be of interest for programmers. It lets us understand programming concepts better and, fundamentally, choose more appropriate abstractions as illustrated in number of case studies that conclude the paper.},
archivePrefix = {arXiv},
arxivId = {1803.10195},
author = {Petricek, Tomas},
doi = {10.22152/programming-journal.org/2018/2/12},
eprint = {1803.10195},
issn = {2473-7321},
journal = {Art, Sci. Eng. Program.},
keywords = {abstraction,and engineering of programming,metaphor,monad,philosophy of science,programming concept,science,the art},
month = mar,
number = {3},
pages = {1--27},
title = {What we talk about when we talk about monads},
volume = {2},
year = {2018}
}
@book{Lloyd1987,
address = {New York, NY, USA},
author = {Lloyd, John W.},
edition = {2},
isbn = {0387181997},
publisher = {Springer},
title = {Foundations of Logic Programming},
year = {1987}
}
@incollection{Lamport1985,
author = {Lamport, Leslie},
booktitle = {Distrib. Syst. Methods Tools Specif. An Adv. Course},
doi = {10.1007/3-540-15216-4_12},
editor = {Paul, M. and Siegert, H. J. and Alford, M. W. and Ansart, J. P. and Hommel, G. and Lamport, L. and Liskov, B. and Mullery, G. P. and Schneider, F. B.},
pages = {7--43},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Basic concepts},
volume = {190},
year = {1985}
}
@book{Kock2006,
author = {Kock, Anders},
edition = {2},
isbn = {9780521687386},
month = jul,
number = {March},
pages = {246},
publisher = {Cambridge University Press},
series = {London Mathematical Society Lecture Note Series},
title = {Synthetic Differential Geometry},
year = {2006}
}
@article{Jacobs2002,
author = {Jacobs, Bart},
doi = {10.1016/S1571-0661(04)80362-1},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {112--134},
title = {Comprehension for Coalgebras},
volume = {65},
year = {2002}
}
@article{Pin2003,
abstract = {This paper is a contribution to the algebraic study of the concatenation product. In the first part of the paper, we extend to the ordered case standard algebraic tools related to the concatenation product, like the Sch??tzenberger product and the relational morphisms. We show in a precise way how the ordered Sch??tzenberger product corresponds to polynomial operations on languages. In the second part of the paper, we apply these results to establish a bridge between the three standard concatenation hierarchies, namely the Straubing-Th??rien hierarchy, the Brzozowski's (or dot-depth) hierarchy and the group hierarchy. ?? 2002 Elsevier Science B.V. All rights reserved.},
author = {Pin, Jean-{\'{E}}ric},
doi = {10.1016/S0304-3975(01)00230-4},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {Concatenation,Finite automata,Recognizable languages},
number = {1},
pages = {317--342},
title = {Algebraic tools for the concatenation product},
volume = {292},
year = {2003}
}
@article{Velebil2011,
author = {Velebil, Jiř{\'{i}} and Kurz, Alexander},
doi = {10.1017/S0960129510000575},
isbn = {0960129510},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = mar,
number = {02},
pages = {363--381},
title = {Equational presentations of functors and monads},
type = {Journal article},
volume = {21},
year = {2011}
}
@book{Eckmann1969,
doi = {10.1007/BFb0083078},
editor = {Eckmann, Beno and Tierney, Myles},
isbn = {978-3-540-04601-1},
keywords = {Equational Categories,Homology,Triples},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Seminar on Triples and Categorical Homology Theory},
volume = {80},
year = {1969}
}
@phdthesis{Rivieccio2010,
author = {Rivieccio, Umberto},
month = mar,
pages = {191},
school = {Universit{\`{a}} di Genova},
title = {An Algebraic Study of Bilattice-based Logics},
year = {2010}
}
@incollection{Scott1970,
author = {Scott, Dana S.},
booktitle = {Philos. Probl. Log.},
doi = {10.1007/978-94-010-3272-8_7},
editor = {Lamber, Karel},
isbn = {978-94-010-3274-2},
pages = {143--173},
publisher = {Springer Netherlands},
series = {Synthese Library},
title = {Advice on Modal Logic},
volume = {29},
year = {1970}
}
@article{Mislove1991a,
abstract = {Motivated by ideas from the study of abstract data types, we show how to interpret non-well-founded sets as fixed points of continuous transformations of an initial continuous algebra. We conisder a preordered structure closely related to the set HF of well-founded, hereditarily finite sets. By taking its ideal completion, we obtain an initial continuous algebra in which we are able to solve all of the usual systems of equations that characterize hereditarily finite, non-well-founded sets. In this way, we are able to obtain a structure which is isomorphic to HF1, the non-well founded analog of HF.},
author = {Mislove, Michael W. and Moss, Lawrence S. and Oles, Frank J.},
doi = {10.1016/0890-5401(91)90051-3},
isbn = {0890-5401},
issn = {08905401},
journal = {Inf. Comput.},
month = jul,
number = {1},
pages = {16--54},
title = {Non-well-founded sets modeled as ideal fixed points},
type = {Journal article},
volume = {93},
year = {1991}
}
@inproceedings{Marti2015,
archivePrefix = {arXiv},
arxivId = {arXiv:1503.02319v1},
author = {Marti, Johannes and Seifan, Fatemeh and Venema, Yde},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.238},
editor = {Moss, Lawrence S. and Sobocinski, Pawel},
eprint = {arXiv:1503.02319v1},
isbn = {978-3-939897-84-2},
issn = {1868-8969},
keywords = {2015,236,4230,and phrases µ -calculus,automata,calco,coalgebra,digital object identifier 10,lipics,uniform interpolation},
pages = {238----252},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {Uniform Interpolation for Coalgebraic Fixpoint Logic},
volume = {35},
year = {2015}
}
@inproceedings{Hasuo2015,
abstract = {In the context of formal verification in general and model checking in particular, parity games serve as a mighty vehicle: many problems are encoded as parity games, which are then solved by the seminal algorithm by Jurdzinski. In this paper we identify the essence of this workflow to be the notion of progress measure, and formalize it in general, possibly infinitary, lattice-theoretic terms. Our view on progress measures is that they are to nested/alternating fixed points what invariants are to safety/greatest fixed points, and what ranking functions are to liveness/least fixed points. That is, progress measures are combination of the latter two notions (invariant and ranking function) that have been extensively studied in the context of (program) verification. We then apply our theory of progress measures to a general model-checking framework, where systems are categorically presented as coalgebras. The framework's theoretical robustness is witnessed by a smooth transfer from the branching-time setting to the linear-time one. Although the framework can be used to derive some decision procedures for finite settings, we also expect the proposed framework to form a basis for sound proof methods for some undecidable/infinitary problems.},
address = {New York, New York, USA},
archivePrefix = {arXiv},
arxivId = {1511.00346},
author = {Hasuo, Ichiro and Shimizu, Shunsuke and C{\^{i}}rstea, Corina},
booktitle = {Proc. 43rd Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang.},
doi = {10.1145/2837614.2837673},
eprint = {1511.00346},
isbn = {9781450335492},
issn = {07308566},
keywords = {coalgebra,fixed-point logic,model checking},
pages = {718--732},
publisher = {ACM Press},
title = {Lattice-theoretic progress measures and coalgebraic model checking},
year = {2016}
}
@article{Klein2014,
abstract = {Este art{\'{i}}culo presenta una cobertura detallada de la verificaci{\'{o}}n formal integral del microkernel SEL4, de su prueba de la correcci{\'{o}}n funcional inicial con los resultados m{\'{a}}s recientes, que se extienden el argumento de garant{\'{i}}a hasta las propiedades de seguridad de nivel superior y hacia abajo a nivel binario de su aplicaci{\'{o}}n. El objetivo de nuestra verificaci{\'{o}}n, el n{\'{u}}cleo, es la parte m{\'{a}}s cr{\'{i}}tica de un sistema, que es nuestra motivaci{\'{o}}n para iniciar la verificaci{\'{o}}n del sistema con este componente},
author = {Klein, Gerwin and Andronick, June and Elphinstone, Kevin and Murray, Toby and Sewell, Thomas and Kolanski, Rafal and Heiser, Gernot},
doi = {10.1145/2560537},
issn = {07342071},
journal = {ACM Trans. Comput. Syst.},
month = feb,
number = {1},
pages = {1--70},
title = {Comprehensive formal verification of an OS microkernel},
volume = {32},
year = {2014}
}
@article{Choe1977,
author = {Choe, Tae H.},
doi = {10.1007/BF02485423},
issn = {00025270},
journal = {Algebr. Universalis},
number = {1},
pages = {137--142},
title = {Injective and projective zero-dimensional compact universal algebras},
volume = {7},
year = {1977}
}
@article{Richardson2006,
abstract = {We propose a simple approach to combining first-order logic and probabilistic graphical models in a single representation. A Markov logic network (MLN) is a first-order knowledge base with a weight attached to each formula (or clause). Together with a set of constants representing objects in the domain, it specifies a ground Markov network containing one feature for each possible grounding of a first-order formula in the KB, with the corresponding weight. Inference in MLNs is performed by MCMC over the minimal subset of the ground network required for answering the query. Weights are efficiently learned from relational databases by iteratively optimizing a pseudo-likelihood measure. Optionally, additional clauses are learned using inductive logic programming techniques. Experiments with a real-world database and knowledge base in a university domain illustrate the promise of this approach.},
archivePrefix = {arXiv},
arxivId = {arXiv:1103.0398},
author = {Richardson, Matthew and Domingos, Pedro},
doi = {10.1007/s10994-006-5833-1},
eprint = {arXiv:1103.0398},
isbn = {0885-6125},
issn = {0885-6125},
journal = {Mach. Learn.},
keywords = {First-order logic,Graphical models,Inductive logic programming,Knowledge-based model construction,Log-linear models,Markov chain Monte Carlo,Markov networks,Markov random fields,Pseudo-likelihood,Satisfiability,Statistical relational learning},
month = feb,
number = {1-2},
pages = {107--136},
pmid = {20958249},
title = {Markov logic networks},
volume = {62},
year = {2006}
}
@article{Priestley1972,
author = {Priestley, Hilary A.},
journal = {Proc. London Math. Soc.},
number = {3},
pages = {507},
publisher = {Oxford University Press},
title = {Ordered topological spaces and the representation of distributive lattices},
type = {Journal article},
volume = {3},
year = {1972}
}
@article{Esik2015,
author = {{\'{E}}sik, Zolt{\'{a}}n},
doi = {10.1093/logcom/ext001},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {Least fixed points,equational theory,iteration theory,residuals},
month = apr,
number = {2},
pages = {453--471},
title = {Residuated Park theories},
volume = {25},
year = {2015}
}
@phdthesis{Jung1988,
author = {Jung, Achim},
number = {April},
school = {Technische Universit{\"{a}}t Darmstadt},
title = {Cartesian closed categories of domains},
year = {1988}
}
@article{Kelly1980a,
author = {Kelly, Gregory Maxwell and Laplaza, M.L.},
doi = {10.1016/0022-4049(80)90101-2},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
pages = {193--213},
title = {Coherence for compact closed categories},
volume = {19},
year = {1980}
}
@article{Stone1936a,
author = {Stone, Marshall H.},
doi = {10.2307/1989664},
issn = {00029947},
journal = {Trans. Am. Math. Soc.},
month = jul,
number = {1},
pages = {37--111},
title = {The theory of representation for Boolean algebras},
type = {Journal article},
volume = {40},
year = {1936}
}
@incollection{Barr1989,
address = {Providence, Rhode Island},
author = {Barr, Michael},
booktitle = {Categ. Comput. Sci. Log.},
doi = {10.1090/conm/092},
editor = {Gray, John W. and Scedrov, Andre},
isbn = {9780821851005},
pages = {1--7},
publisher = {American Mathematical Society},
series = {Contemporary Mathematics},
title = {Models of Horn theories},
year = {1989}
}
@incollection{Kelly1974a,
author = {Kelly, Gregory Maxwell},
booktitle = {Proc. Sydney Categ. Theory Semin. 1972/1973},
doi = {10.1007/BFb0063096},
editor = {Kelly, Gregory M.},
isbn = {978-3-540-06966-9},
pages = {257--280},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Doctrinal adjunction},
volume = {420},
year = {1974}
}
@article{Leinster2013,
abstract = {Even a functor without an adjoint induces a monad, namely, its codensity monad; this is subject only to the existence of certain limits. We clarify the sense in which codensity monads act as substitutes for monads induced by adjunctions. We also expand on an undeservedly ignored theorem of Kennison and Gildenhuys: that the codensity monad of the inclusion of (finite sets) into (sets) is the ultrafilter monad. This result is analogous to the correspondence between measures and integrals. So, for example, we can speak of integration against an ultrafilter. Using this language, we show that the codensity monad of the inclusion of (finite-dimensional vector spaces) into (vector spaces) is double dualization. From this it follows that compact Hausdorff spaces have a linear analogue: linearly compact vector spaces. Extension of this analogy to other theories is left as an open question.},
archivePrefix = {arXiv},
arxivId = {1209.3606},
author = {Leinster, Tom},
eprint = {1209.3606},
journal = {Theory Appl. Categ.},
month = sep,
number = {13},
pages = {26},
title = {Codensity and the ultrafilter monad},
volume = {28},
year = {2013}
}
@inproceedings{Kurz2007,
author = {Kurz, Alexander and Rosick{\'{y}}, Jiř{\'{i}}},
booktitle = {Proc. 2nd Int. Conf. Algebr. Coalgebra Comput. Sci.},
isbn = {978-3-540-73857-2},
month = aug,
pages = {342--355},
title = {The Goldblatt-Thomason theorem for coalgebras},
year = {2007}
}
@inproceedings{Matsikoudis2012,
author = {Matsikoudis, Eleftherios and Lee, Edward A.},
booktitle = {Proc. 11th Int. Work. Coalgebraic Methods Comput. Sci.},
title = {From transitions to executions},
volume = {0720882},
year = {2012}
}
@incollection{Linton1969a,
author = {Linton, F. E. J.},
booktitle = {Semin. Triples Categ. Homol. Theory},
doi = {10.1007/BFb0083080},
editor = {Eckmann, B.},
isbn = {978-3-540-04601-1},
pages = {7--52},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {An outline of functorial semantics},
year = {1969}
}
@article{Rosebrugh2004,
author = {Rosebrugh, Robert and Wood, R. J.},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Complete distributivity,Idempotent splitting completion,K-Z doctrine},
number = {12},
pages = {172--183},
title = {Split structures},
volume = {13},
year = {2004}
}
@article{Pitts2011,
abstract = {ABSTRACT This paper introduces a new recursion principle for inductively defined data modulo $\alpha$-equivalence of bound names that makes use of Odersky-style local names when recursing over bound names. It is formulated in simply typed $\lambda$-calculus extended with names that can be restricted to a lexical scope, tested for equality, explicitly swapped and abstracted. The new recursion principle is motivated by the nominal sets notion of ‘$\alpha$-structural recursion', whose use of names and associated freshness side-conditions in recursive definitions formalizes common practice with binders. The new calculus has a simple interpretation in nominal sets equipped with name-restriction operations. It is shown to adequately represent $\alpha$-structural recursion while avoiding the need to verify freshness side-conditions in definitions and computations. The paper is a revised and expanded version of Pitts (Nominal System T. In Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 2010 (Madrid, Spain). ACM Press, pp. 159–170, 2010).},
author = {Pitts, Andrew M.},
doi = {10.1017/S0956796811000116},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = may,
number = {03},
pages = {235--286},
title = {Structural recursion with locally scoped names},
volume = {21},
year = {2011}
}
@article{Shafer1979,
abstract = {This paper studies belief functions, set functions which are normalized and monotone of order ∞ ∞ . The concepts of continuity and condensability are defined for belief functions, and it is shown how to extend continuous or condensable belief functions from an algebra of subsets to the corresponding power set. The main tool used in this extension is the theorem that every belief function can be represented by an allocation of probability--i.e., by a ∩ ∩ -homomorphism into a positive and completely additive probability algebra. This representation can be deduced either from an integral representation due to Choquet or from more elementary work by Revuz and Honeycutt.},
author = {Shafer, Glenn},
journal = {Ann. Probab.},
number = {5},
pages = {827--839},
title = {Allocations of Probability},
volume = {7},
year = {1979}
}
@incollection{Abel1999,
abstract = {We present a new strong normalisation proof for a $\lambda$-calculus with interleaving strictly positive inductive types $\lambda$$\mu$ which avoids the use of impredicative reasoning, i.e., the theorem of Knaster-Tarski. Instead it only uses predicative, i.e., strictly positive inductive definitions on the metalevel. To achieve this we show that every strictly positive operator on types gives rise to an operator on saturated sets which is not only monotone but also (deterministically) set based - a concept introduced by Peter Aczel in the context of intuitionistic set theory. We also extend this to coinductive types using greatest fixpoints of strictly monotone operators on the metalevel. The use of the term interleaving for this situation is due to Ralph Matthes, e.g., see [Mat98]. An alternative would be mutually. Types for Proofs and ProgramsTypes for Proofs and Programs Look Inside Other actions Reprints and Permissions Export citation About this Book Add to Papers},
author = {Abel, Andreas M. and Altenkirch, Thorsten},
booktitle = {Types for Proofs and Programs,TYPES'99},
editor = {Coquand, Thierry and Dybjer, Peter and Nordstr{\"{o}}m, Bengt and Smith, Jan},
pages = {21--40},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {A predicative strong normalisation proof for a $\lambda$-calculus with interleaving inductive types},
year = {2000}
}
@article{Caliskan2017,
abstract = {Artificial intelligence and machine learning are in a period of astounding growth. However, there are concerns that these technologies may be used, either with or without intention, to perpetuate the prejudice and unfairness that unfortunately characterizes many human institutions. Here we show for the first time that human-like semantic biases result from the application of standard machine learning to ordinary language---the same sort of language humans are exposed to every day. We replicate a spectrum of standard human biases as exposed by the Implicit Association Test and other well-known psychological studies. We replicate these using a widely used, purely statistical machine-learning model---namely, the GloVe word embedding---trained on a corpus of text from the Web. Our results indicate that language itself contains recoverable and accurate imprints of our historic biases, whether these are morally neutral as towards insects or flowers, problematic as towards race or gender, or even simply veridical, reflecting the {\em status quo} for the distribution of gender with respect to careers or first names. These regularities are captured by machine learning along with the rest of semantics. In addition to our empirical findings concerning language, we also contribute new methods for evaluating bias in text, the Word Embedding Association Test (WEAT) and the Word Embedding Factual Association Test (WEFAT). Our results have implications not only for AI and machine learning, but also for the fields of psychology, sociology, and human ethics, since they raise the possibility that mere exposure to everyday language can account for the biases we replicate here.},
archivePrefix = {arXiv},
arxivId = {1608.07187},
author = {Caliskan, Aylin and Bryson, Joanna J. and Narayanan, Arvind},
doi = {10.1126/science.aal4230},
eprint = {1608.07187},
issn = {10959203},
journal = {Science (80-. ).},
keywords = {results even with,we replicated the iat},
number = {6334},
pages = {183--186},
pmid = {28408601},
title = {Semantics derived automatically from language corpora contain human-like biases},
volume = {356},
year = {2017}
}
@article{Capretta2005,
author = {Capretta, Venanzio},
doi = {10.2168/LMCS-1(2:1)2005},
editor = {Barendregt, Henk},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = jul,
number = {2},
pages = {1--28},
title = {General recursion via coinductive types},
volume = {1},
year = {2005}
}
@incollection{Chang2012,
abstract = {The existing call-by-need lambda calculi describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the existing calculi models evaluation in a way that matches lazy implementations. Both calculi suffer from the same two problems. First, the calculi never discard function calls, even after they are completely resolved. Second, the calculi include re-association axioms even though these axioms are merely administrative steps with no counterpart in any implementation. In this paper, we present an alternative axiomatization of lazy evaluation using a single axiom. It eliminates both the function call retention problem and the extraneous re-association axioms. Our axiom uses a grammar of contexts to describe the exact notion of a needed computation. Like its predecessors, our new calculus satisfies consistency and standardization properties and is thus suitable for reasoning about behavioral equivalence. In addition, we establish a correspondence between our semantics and Launchbury's natural semantics.},
archivePrefix = {arXiv},
arxivId = {1201.3907},
author = {Chang, Stephen and Felleisen, Matthias},
booktitle = {Proc. 21st Eur. Symp. Program.},
doi = {10.1007/978-3-642-28869-2_7},
editor = {Seidl, Helmut},
eprint = {1201.3907},
keywords = {call-by-need,lambda calculus,laziness},
pages = {128--147},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Note in Computer Science},
title = {The call-by-need lambda calculus, revisited},
volume = {7211},
year = {2012}
}
@article{Petkovic2006,
abstract = {In this paper, we give correspondences between unary algebras, semigroups and congruences on free semigroups. We establish isomorphisms between the complete lattice of varieties of semigroups and the complete lattices of families of varieties of unary algebras, and families of filters of congruences on free semigroups. Similar correspondences between generalized varieties and pseudovarieties of semigroups and corresponding families of algebras and congruences are also established.},
author = {Petkovi{\'{c}}, Tatjana and {\'{C}}iri{\'{c}}, M. and Bogdanovi{\'{c}}, S.},
doi = {10.1142/S1005386706000447},
journal = {Algebr. Colloq.},
keywords = {automata,pseudovarieties,regular identities,unary algebras,varieties},
number = {3},
pages = {495--506},
title = {On Correspondences Between Unary Algebras , Automata , Semigroups and Congruences},
volume = {13},
year = {2006}
}
@inproceedings{Bonsangue2007,
abstract = {Abramsky's logical formulation of domain theory is extended to encompass the domain theoretic model for pi-calculus processes of Stark and of Fiore, Moggi and Sangiorgi. This is done by defining a logical counterpart of categorical constructions including dynamic name allocation and name exponentiation, and showing that they are dual to standard constructs in functor categories. We show that initial algebras of functors defined in terms of these constructs give rise to a logic that is sound, complete, and characterises bisimilarity. The approach is modular, and we apply it to derive a logical formulation of pi-calculus. The resulting logic is a modal calculus with primitives for input, free output and bound output.},
author = {Bonsangue, Marcello M. and Kurz, Alexander},
booktitle = {22nd Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2007.36},
isbn = {0-7695-2908-9},
pages = {303--312},
publisher = {IEEE},
title = {Pi-calculus in logical Form},
year = {2007}
}
@article{Rosicky2002,
author = {Rosick{\'{y}}, Jiř{\'{i}} and Tholen, Walter},
doi = {10.1016/S0022-4049(02)00141-X},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1-3},
pages = {355--382},
title = {Lax factorization algebras},
volume = {175},
year = {2002}
}
@incollection{Mislove2004,
abstract = {Labelled Markov processes (LMPs) are automata whose transitions are given by probability distributions. In this paper we present a ‘universal' LMP as the spectrum of a commutative C *-algebra consisting of formal linear combinations of labelled trees. We characterize the state space of the universal LMP as the set of homomorphims from an ordered commutative monoid of labelled trees into the multiplicative unit interval. This yields a simple semantics for LMPs which is fully abstract with respect to probabilistic bisimilarity. We also consider LMPs with entry points and exit points in the setting of iteration theories. We define an iteration theory of LMPs by specifying its categorical dual: a certain category of C *-algebras. We find that the basic operations for composing LMPs have simple definitions in the dual category.},
author = {Mislove, Michael W. and Ouaknine, Jo{\"{e}}l and Pavlovi{\'{c}}, Dusko},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Walukiewicz, Igor},
pages = {393--707},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Duality for labelled Markov processes},
volume = {2987},
year = {2004}
}
@article{Venema2006,
author = {Venema, Yde},
doi = {10.1016/j.ic.2005.06.003},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {04,106,2004,355,375,a significantly revised and,appeared under,automata,automata and fixed point,bisimulation,coalgebra,computer science,electronic notes in theoretical,expanded version of a,fixed point operators,game semantics,in proceedings cmcs,logics for coalgebras,modal logic,parity games,pp,preliminary conference paper which,the title,vol,ୋ this paper is},
month = apr,
number = {4},
pages = {637--678},
title = {Automata and fixed point logic: A coalgebraic perspective},
volume = {204},
year = {2006}
}
@article{Crolard2001,
abstract = {This paper is the first part of a work whose purpose is to investigate duality in some related frameworks (cartesian closed categories, lambda-calculi, intuitionistic and classical logics) from syntactic, semantical and computational viewpoints. We start with category theory and we show that any bicartesian closed category with coexponents is degenerated (i.e. there is at most one arrow between two objects). The remainder of the paper is devoted to logical issues. We examine the propositional calculus underlying the type system of bicartesian closed categories with coexponents and we show that this calculus corresponds to subtractive logic: a conservative extension of intuitionistic logic with a new connector (subtraction) dual to implication. Eventually, we consider first-order subtractive logic and we present an embedding of classical logic into subtractive logic. {\textcopyright} 2001 Published by Elsevier Science B.V.},
author = {Crolard, Tristan},
doi = {10.1016/S0304-3975(99)00124-3},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = mar,
number = {1-2},
pages = {151--185},
title = {Subtractive logic},
volume = {254},
year = {2001}
}
@book{Cortier2014,
author = {Cortier, V{\'{e}}ronique and Kremer, Steve},
booktitle = {Found. Trends{\textregistered} Program. Lang.},
doi = {10.1561/2500000001},
isbn = {2500000001},
issn = {2325-1107},
number = {3},
pages = {151--167},
title = {Formal Models and Techniques for Analyzing Security Protocols: A Tutorial},
volume = {1},
year = {2014}
}
@inproceedings{Danielsson2012,
abstract = {The operational semantics of a partial, functional language is often given as a relation rather than as a function. The latter approach is arguably more natural: if the language is functional, why not take advantage of this when defining the semantics},
address = {New York, New York, USA},
author = {Danielsson, Nils Anders},
booktitle = {Proc. 17th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '12},
doi = {10.1145/2364527.2364546},
isbn = {9781450310543},
issn = {15232867},
keywords = {dependent types,mixed induction and coinduction},
pages = {127},
publisher = {ACM Press},
title = {Operational semantics using the partiality monad},
year = {2012}
}
@article{Tholen2017,
abstract = {The paper proposes the notions of topological platform and quantalic topological theory for the presentation and investigation of categories of interest beyond the realm of algebra. These notions are nevertheless grounded in algebra, through the notions of monad and distributive law. The paper shows how they entail previously proposed concepts with similar goals.},
author = {Tholen, Walter},
doi = {10.1515/tmj-2017-0110},
issn = {1512-0139},
journal = {Tbilisi Math. J.},
month = nov,
number = {3},
pages = {91--104},
title = {Quantalic topological theories},
volume = {10},
year = {2017}
}
@incollection{Vardi2001a,
abstract = {The discussion of the relative merits of linear- versus branching-time frameworks goes back to early 1980s. One of the beliefs dominating this discussion has been that "while specifying is easier in LTL (linear-temporal logic), verification is easier for CTL (branching-temporal logic)". Indeed, the restricted syntax of CTL limits its expressive power and many important behaviors (e.g., strong fairness) can not be specified in CTL. On the other hand, while model checking for CTL can be done in time that is linear in the size of the specification, it takes time that is exponential in the specification for LTL. Because of these arguments, and for historical reasons, the dominant temporal specification language in industrial use is CTL.},
author = {Vardi, Moshe Y},
booktitle = {Proc. 7th Int. Conf. Tools Algorithms Constr. Anal. Syst.},
doi = {10.1007/3-540-45319-9_1},
editor = {Margaria, Tiziana and Yi, Wang},
isbn = {3540418652},
issn = {16113349},
pages = {1--22},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Branching vs. linear time: final showdown},
volume = {2031},
year = {2001}
}
@article{Hofmann2016,
abstract = {Motivated by the need to reason about hybrid systems, we study limits in categories of coalgebras whose underlying functor is a Vietoris polynomial one - intuitively, the topological analogue of a Kripke polynomial functor. Among other results, we prove that every Vietoris polynomial functor admits a final coalgebra if it respects certain conditions concerning separation axioms and compactness. When the functor is restricted to some of the categories induced by these conditions the resulting categories of coalgebras are even complete. As a practical application, we use these developments in the specification and analysis of non-deterministic hybrid systems, in particular to obtain suitable notions of stability, and behaviour.},
archivePrefix = {arXiv},
arxivId = {1612.03318},
author = {Hofmann, Dirk and Neves, Renato and Nora, Pedro},
eprint = {1612.03318},
month = dec,
pages = {1--28},
title = {Limits in categories of Vietoris coalgebras},
year = {2016}
}
@article{Kohlas2012,
abstract = {Many problems of artificial intelligence, or more generally, many problems of information processing, have a generic solution based on local computation on join trees or acyclic hypertrees. There are several variants of this method all based on the algebraic structure of valuation algebras. A strong requirement underlying this approach is that the elements of a problem decomposition form a join tree. Although it is always possible to construct covering join trees, if the requirement is originally not satisfied, it is not always possible or not efficient to extend the elements of the decomposition to the covering join tree. Therefore in this paper different variants of an axiomatic framework of valuation algebras are introduced which prove sufficient for local computation without the need of an extension of the factors of a decomposition. This framework covers the axiomatic system proposed by Shenoy and Shafer (1990) [1]. A particular emphasis is laid on the important special cases of idempotent algebras and algebras with some notion of division. It is shown that all well-known architectures for local computation like the Shenoy-Shafer architecture, Lauritzen-Spiegelhalter and HUGIN architectures may be adapted to this new framework. Further a new architecture for idempotent algebras is presented. As examples, in addition to the classical instances of valuation algebras, semiring-based valuation algebras, Gaussian potentials and the relational algebra are presented. {\textcopyright} 2011 Elsevier Inc. All rights reserved.},
author = {Kohlas, J{\"{u}}rg and Pouly, Marc and Schneuwly, Cesar},
doi = {10.1016/j.jcss.2011.05.012},
isbn = {9782879710341},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
keywords = {Generic computation,Hypertree decomposition,Join trees,Local computation,Valuation algebras},
month = jan,
number = {1},
pages = {348--369},
publisher = {Elsevier Inc.},
title = {Generic local computation},
volume = {78},
year = {2012}
}
@article{Johann2008,
abstract = {GADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools - analogous to the well-known and widely-used ones for algebraic and nested data types - for reasoning about, programming with, and improving the performance of programs involving, GADTs; we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can be derived. Copyright {\textcopyright} 2008 ACM.},
author = {Johann, Patricia and Ghani, Neil},
doi = {10.1145/1328897.1328475},
isbn = {9781595936899},
issn = {03621340},
journal = {ACM SIGPLAN Not.},
pages = {297},
title = {Foundations for structured programming with GADTs},
volume = {43},
year = {2008}
}
@article{Morris2009a,
author = {Morris, Peter and Altenkirch, Thorsten and Ghani, Neil},
doi = {10.1142/S0129054109006462},
isbn = {1920682465},
issn = {14451336},
journal = {Int. J. Found. Comput. Sci.},
keywords = {Advanced Data Types,Dependently Typed Programming,Epigram,Generic Programming},
number = {01},
title = {A universe of strictly positive families},
volume = {20},
year = {2009}
}
@inproceedings{Renyi1961,
abstract = {We shall investigate the relationships between the thermodynamic entropy and information theory and the implications that can be drawn for the arrow of time. This demands a careful study of classical thermodynamics and a review of its fundamental concepts. The statistical mechanical properties of time-dependent systems will be carefully studied, and the point at which the arrow of time appears will be described.},
archivePrefix = {arXiv},
arxivId = {1101.3070},
author = {R{\'{e}}nyi, Alfr{\'{e}}d},
booktitle = {Proc. Fourth Berkeley Symp. Math. Stat. Probab.},
doi = {10.1021/jp106846b},
eprint = {1101.3070},
isbn = {0097-0433},
issn = {15205207},
pages = {547--561},
pmid = {20961075},
title = {On measures of entropy and information},
volume = {1},
year = {1961}
}
@book{Lau2006,
abstract = {"This book gives a broad introduction to the theory of function algebras and leads to the cutting edge of research. To familiarize the reader from the very beginning on with the algebraic side of function algebras the more general concepts of the Universal Algebra is given in the first part of the book. The second part on function algebras covers the following topics: Galois-connection between function algebras and relation algebras, completeness criterions, clone theory."--Jacket.},
author = {Lau, Dietlinde.},
doi = {10.1007/3-540-36023-9},
isbn = {978-3-540-36022-3},
issn = {1439-7382},
publisher = {Springer Berlin Heidelberg},
series = {Springer Monographs in Mathematics},
title = {Function Algebras on Finite Sets},
year = {2006}
}
@inproceedings{Jeffrey2012,
author = {Jeffrey, Alan},
booktitle = {Proc. 6th ACM Work. Program. Lang. meets Progr. Verif.},
title = {LTL types FRP},
type = {Conference proceedings (article)},
year = {2012}
}
@article{Moss1997,
author = {Moss, Lawrence S.},
doi = {10.1093/jigpal/5.2.231},
issn = {1367-0751},
journal = {Log. J. IGPL},
keywords = {coalgebra,corecursion,operator on sets},
month = mar,
number = {2},
pages = {231--257},
title = {On the Foundations of Corecursion},
volume = {5},
year = {1997}
}
@article{Gambino2009,
abstract = {We study polynomial functors over locally cartesian closed categories. After setting up the basic theory, we show how polynomial functors assemble into a double category, in fact a framed bicategory. We show that the free monad on a polynomial endofunctor is polynomial. The relationship with operads and other related notions is explored.},
archivePrefix = {arXiv},
arxivId = {0906.4931},
author = {Gambino, Nicola and Kock, Joachim},
eprint = {0906.4931},
journal = {ArXiv e-prints},
month = jun,
pages = {41},
title = {Polynomial functors and polynomial monads},
year = {2009}
}
@article{Porst2011,
abstract = {We show that subobjects and quotients respectively of any object K in a locally finitely presentable category form an algebraic lattice. The same holds for the internal equivalence relations on K. In fact, these results turn out to be—at least in the case of subobjects—nothing but simple consequences of well known closure properties of the classes of locally finitely presentable categories and accessible categories, respectively. We thus get a completely categorical explanation of the well known fact that the subobject- and congruence lattices of algebras in finitary varieties are algebraic. Moreover we also obtain new natural examples: in particular, for any (not necessarily finitary) polynomial set-functor F, the subcoalgebras of an F-coalgebra form an algebraic lattice; the same holds for the lattices of regular congruences and quotients of these F-coalgebras.},
author = {Porst, Hans-E.},
doi = {10.1007/s00012-011-0129-0},
issn = {0002-5240},
journal = {Algebr. universalis},
keywords = {algebraic lattice,and phrases,congruence,hospitality of tshwane university,internal equivalence relation,is gratefully acknowledged,locally finitely presentable category,of technology,pretoria,quo-,subobject,tient},
month = apr,
number = {3},
pages = {285--298},
title = {Algebraic lattices and locally finitely presentable categories},
volume = {65},
year = {2011}
}
@unpublished{Gumm1999,
author = {Gumm, H. Peter},
keywords = {Coalgebra,coalgebra},
mendeley-tags = {coalgebra},
title = {Elements of the general theory of coalgebras},
type = {Unpublished work},
url = {http://www.mathematik.uni-marburg.de/$\sim$gumm/Papers/Luatcs.ps},
year = {1999}
}
@article{Worrell2005,
abstract = {A standard construction of the final coalgebra of an endofunctor involves defining a chain of iterates, starting at the final object of the underlying category and successively applying the functor. In this paper we show that, for a finitary set functor, this construction always yields a final coalgebra in $\omega$2=$\omega$+$\omega$ steps.},
author = {Worrell, James},
doi = {10.1016/j.tcs.2004.12.009},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = jun,
number = {1-3},
pages = {184--199},
title = {On the final sequence of a finitary set functor},
volume = {338},
year = {2005}
}
@book{Gabriel1971,
author = {Gabriel, Peter and Ulmer, Friedrich},
doi = {10.1007/BFb0059396},
isbn = {978-3-540-05578-5},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Lokal pr{\"{a}}sentierbare Kategorien},
volume = {221},
year = {1971}
}
@article{Coumans2012,
author = {Coumans, D. C. S. and van Gool, Sam J.},
doi = {10.1093/logcom/exs016},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {free algebras,partial algebras,quasi-equations,rank 0-1},
month = may,
number = {3},
pages = {645--672},
title = {On generalizing free algebras for a functor},
volume = {23},
year = {2012}
}
@article{SLack2004,
abstract = {We introduce adhesive categories, which are categories with structure ensuring that pushouts along monomorphisms are well- behaved, as well as quasiadhesive categories which restrict attention to regular monomorphisms. Many examples of graphical structures used in computer science are shown to be examples of adhesive and quasi- adhesive categories. Double-pushout graph rewriting generalizes well to rewriting on arbitrary adhesive and quasiadhesive categories. Mathematics},
author = {Uustalu, Tarmo},
doi = {10.1051/ita:2003022},
issn = {0988-3754},
journal = {Theor. Informatics Appl.},
keywords = {adhesive categories,and phrases,category theory,extensive categories,quasiadhesive categories},
month = oct,
number = {4},
pages = {315--336},
title = {Generalizing Substitution},
volume = {37},
year = {2003}
}
@article{Yeung1991,
abstract = {Let X(i), i = 1,...,n, be discrete random variables, and X \napproximately (i) be a set variable corresponding to X(i). Define the\nuniversal set OMEGA to be union i(n) = 1X approximately (i) and let \nthe sigma-field generated by {X approximately (i), i = 1,...,n}. It \nis shown that Shannon's information measures on the random vairables \nX(i), i = 1,...,n, constitute a unique measure mu* on F, which is \ncalled the I-Measure. In other words, the Shannon information measure\n(i.e., Shannon's information measures as a whole) is a measure on F, \nthus establishing the analogy between information theory and set \ntheory. Therefore each information theoretic operation can formally \nbe viewed as a set theoretic operation, and vice versa. This point of\nview, which we believe is of fundamental importance, has apparently \nbeen overlooked in the past by information theorists. As a \nconsequence the I-Diagram is introduced, which is a geometrical \nrepresentation of the relationship among the information measures. \nThe J-Diagram is analogous to the Venn Diagram in set theory. The use\nof the I-Diagram is discussed; some applications of which reveal \nresults that may otherwise be difficult to discover. A formula is \nalso derived for the value of the I-Measure of the atoms of F and its\nsub-sigma-fields generated by some subsets of the basic set \nvariables.},
author = {Yeung, R.W.},
doi = {10.1109/18.79902},
isbn = {978-3-642-56669-1},
issn = {0018-9448},
journal = {IEEE Trans. Inf. Theory},
month = may,
number = {3},
pages = {466--474},
title = {A new outlook on Shannon's information measures},
volume = {37},
year = {1991}
}
@article{Goncharov2014a,
archivePrefix = {arXiv},
arxivId = {1401.5277},
author = {Goncharov, Sergey and Milius, Stefan and Silva, Alexandra},
eprint = {1401.5277},
journal = {ArXiv e-prints},
month = jan,
pages = {1--48},
title = {Towards a Coalgebraic Chomsky Hierarchy},
year = {2014}
}
@inproceedings{Traytel2012,
author = {Traytel, Dmitry and Popescu, Andrei and Blanchette, Jasmin C.},
booktitle = {Proc. 2012 27th Annu. ACM/IEEE Symp. Log. Comput. Sci. LICS 2012},
doi = {10.1109/LICS.2012.75},
isbn = {9780769547695},
keywords = {(co)datatypes,Category theory,cardinals,higher-order logic,interactive theorem proving},
pages = {596--605},
title = {Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving},
year = {2012}
}
@incollection{Makinson2005,
address = {Berlin/Heidelberg},
author = {Makinson, David},
booktitle = {Handb. Philos. Log.},
doi = {10.1007/1-4020-3092-4_3},
pages = {175--278},
publisher = {Springer-Verlag},
title = {How to go nonmonotonic},
volume = {12},
year = {2005}
}
@article{Dwork2013,
abstract = {Private data analysis-the useful analysis of confidential data-requires a rigorous and practicable definition of privacy. Differential privacy, an emerging standard, is the subject of intensive investigation in several diverse research communities. We review the definition, explain its motivation, and discuss some of the challenges to bringing this concept to practice.},
author = {Dwork, Cynthia and Pottenger, Rebecca},
doi = {10.1136/amiajnl-2012-001047},
isbn = {1527-974X; 1067-5027},
issn = {1527-974X},
journal = {J. Am. Med. Informatics Assoc.},
month = jan,
number = {1},
pages = {102--108},
pmid = {23243088},
title = {Toward practicing privacy},
volume = {20},
year = {2013}
}
@phdthesis{Murray2010a,
abstract = {The object-capability model is an increasingly popular architecture\nfor building secure software systems. This model promotes the construction\nof reusable patterns for enforcing security properties within object-capability\nsystems. In this thesis, we apply the process algebra CSP, and its\nautomatic refinement-checker FDR, to analyse object-capability patterns\nand prove whether they uphold the security properties they are designed\nto enforce. We show how CSP can accurately model object capability\nsystems and patterns, and express their wide variety of features.\nWe show that complex safety properties of object-capability patterns\ncan be reasoned about by encoding them as CSP refinement checks for\nFDR. This enables one to detect vulnerabilities automatically in\npatterns due to concurrent and recursive invocation. We show that\nCSP's theory of data-independence can be applied to allow one to\ngeneralise the results obtained from analysing small fixed-sized\nsystems, to systems of arbitrary size. We show how to reason about\nthe information flow properties of object capability patterns. We\nargue that in order to do so sensibly, one must make the assumption\nthat objects can directly in uence each other only through their\novert interactions together. We show how traditional noninterference\nproperties can be adapted to take this assumption into account, and\nhow they can then be tested with FDR. We consider how to reason about\nliveness properties of object-capability patterns under necessary\nfairness assumptions. We prove that such properties cannot always\nbe expressed as CSP refinement checks for FDR, making them impossible\nfor FDR to test precisely, but how FDR can be applied to reason about\nthem by testing sufficient conditions for them instead. To reason\nabout authority, we develop a framework for expressing general non-causation\nproperties and show how it can capture various kinds of authority,\nas well as the notions of defensive correctness and defensive con-\nsistency. We show that, for deterministic systems, non-causation\nof safety effects can be expressed as refinement checks in CSP models\nthat FDR can support. However, for nondeterministic systems, we prove\nthat even certain simple non-causation properties cannot be precisely\ncaptured this way.},
author = {Murray, Toby},
school = {University of Oxford},
title = {Analysing the Security Properties of Object-Capability Patterns},
year = {2010}
}
@inproceedings{Brown2016,
abstract = {According to conventional wisdom, a self-interpreter for a strongly normalizing $\lambda$-calculus is impossible. We call this the normalization barrier. The normalization barrier stems from a theorem in computability theory that says that a to- tal universal function for the total computable functions is impossible. In this paper we break through the normaliza- tion barrier and define a self-interpreter for System F$\omega$, a strongly normalizing $\lambda$-calculus. After a careful analysis of the classical theorem, we show that static type checking in F$\omega$ can exclude the proof's diagonalization gadget, leaving open the possibility for a self-interpreter. Along with the self-interpreter, we program four other operations in F$\omega$, in- cluding a continuation-passing style transformation. Our op- erations rely on a new approach to program representation that may be useful in theorem provers and compilers.},
address = {New York, New York, USA},
author = {Brown, Matt and Palsberg, Jens},
booktitle = {Proc. 43rd Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang.},
doi = {10.1145/2837614.2837623},
isbn = {9781450335492},
issn = {07308566},
keywords = {2009,29,and hofer,f,lambda calculus,meta programming,ostermann,presented the first,rendel,self in-,self representation,self-interpreter for a typed,terpretation,$\lambda$ -calculus},
pages = {5--17},
publisher = {ACM Press},
title = {Breaking through the normalization barrier: a self-interpreter for f-omega},
year = {2016}
}
@book{Dubuc1970,
author = {Dubuc, Eduardo J.},
doi = {10.1007/BFb0060485},
isbn = {978-3-540-04934-0},
pmid = {13771357},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Kan extensions in Enriched Category Theory},
volume = {145},
year = {1970}
}
@inproceedings{Adamek2012a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Moss, Lawrence S.},
booktitle = {Proc. 11th Int. Work. Coalgebraic Methods Comput. Sci.},
doi = {10.1007/978-3-642-32784-1_4},
keywords = {finitary functors,hausdorff functor,presentation of func-},
title = {On finitary functors and their presentations},
year = {2012}
}
@book{Goodfellow2016,
abstract = {Deep learning draws upon many modeling formalisms that researchers can use to guide their design efforts and describe their algorithms. One of these formalisms is the idea of structured probabilistic models. We have already discussed structured probabilistic models briefly in Chapter 3.14. That brief presentation was sufficient to understand how to use structured probabilistic models as a language to describe some of the algorithms in part II of this book. Now, in part III, structured probabilistic models are a key ingredient of many of the most important research topics in deep learning. In order to prepare to discuss these research ideas, this chapter describes structured probabilistic models in much greater detail. This chapter is intended to be self-contained; the reader does not need to review the earlier introduction before continuing with this chapter. A structured probabilistic model is a way of describing a probability distribu-tion, using a graph to describe which random variables in the probability distri-bution interact with each other directly. Here we use " graph " in the graph theory sense–a set of vertices connected to one another by a set of edges. Because the structure of the model is defined by a graph, these models are often also referred to as graphical models. The graphical models research community is large and has developed many different models, training algorithms, and inference algorithms. In this chap-ter, we provide basic background on some of the most central ideas of graphical models, with an emphasis on the concepts that have proven most useful to the deep learning research community. If you already have a strong background in graphical models, you may wish to skip most of this chapter. However, even a graphical model expert may benefit from reading the final section of this chap-ter, section 13.6, in which we highlight some of the unique ways that graphical 412 CHAPTER 13. STRUCTURED PROBABILISTIC MODELS FOR DEEP LEARNING models are used for deep learning algorithms. Deep learning practitioners tend to use very different model structures, learning algorithms, and inference procedures than are commonly used by the rest of the graphical models research community. In this chapter, we identify these differences in preferences and explain the reasons for them. In this chapter we first describe the challenges of building large-scale proba-bilistic models in section 13.1. Next, we describe how to use a graph to describe the structure of a probability distribution in section 13.2. We then revisit the challenges we described in section 13.1 and show how the structured approach to probabilistic modeling can overcome these challenges in section 13.3. One of the major difficulties in graphical modeling is understanding which variables need to be able to interact directly, i.e., which graph structures are most suitable for a given problem. We outline two approaches to resolving this difficulty by learning about the dependencies in section 13.4. Finally, we close with a discussion of the unique emphasis that deep learning practitioners place on specific approaches to graphical modeling in section 13.6. 13.1 The Challenge of Unstructured Modeling},
author = {Goodfellow, Ian and Yoshua, Bengio and Aaron, Courville},
isbn = {978-0262035613},
keywords = {machine learning},
pages = {800},
publisher = {The MIT Press},
series = {Adaptive Computation and Machine Learning series},
title = {Deep Learning},
year = {2016}
}
@book{Borceux1994a,
author = {Borceux, Francis},
pages = {364},
publisher = {Cambridge University Press},
series = {Encyclopedia of Mathematics and its Applications},
title = {Handbook of Categorical Algebra 2: Categories and Structures},
year = {1994}
}
@book{Butz1998,
abstract = {Notes handed out to students attending the course on Category Theory at the Department of Computer Science in Aarhus, Spring 1998. These notes were supposed to give more detailed information about the relationship between regular categories and regular logic than is contained in Jaap van Oosten's script on

license_type: permissive

branch_name: refs/heads/master

extension: bib