text:
category theory (BRICS Lectures Series LS-95-1). Regular logic is there called coherent logic.},
author = {Butz, Carsten},
issn = {1395-2048},
number = {October},
pages = {46},
series = {BRICS Lecture Series},
title = {Regular Categories and Regular Logic},
year = {1998}
}
@book{Tennent1991a,
author = {Tennent, R. D.},
isbn = {0138055998},
month = jul,
publisher = {Prentice Hall},
title = {Semantics of Programming Languages},
type = {Book},
year = {1991}
}
@article{Majster-Cederbaum1996,
abstract = {Complete partial orders have been used for a long time for defining semantics of programming languages. In the context of concurrency de Bakker and Zucker (1982) proposed a metric setting for handling concurrency, recursion and nontermination, which has proved to be very successful in many applications. Starting with a semantic domain D for 'finite behaviour' we investigate the relation between the ideal completion Idl(D) and the metric completion which are both suitable to model recursion and infinite behaviour. We also consider the properties of semantic operators.},
author = {Majster-Cederbaum, Mila E. and Baier, Christel},
doi = {10.1016/0304-3975(95)00262-6},
issn = {03043975},
journal = {Theor. Comput. Sci.},
number = {1-2},
pages = {145--171},
title = {Metric completion versus ideal completion},
volume = {170},
year = {1996}
}
@incollection{AndrewM.Pitts1995,
author = {Pitts, Andrew M.},
booktitle = {Handb. Log. Comput. Sci.},
editor = {Abramsky, Samson and Gabbay, D. M. and Maibaum, Thomas S.E.},
publisher = {Oxford University Press},
title = {Categorical Logic},
year = {1995}
}
@incollection{Kelly1974,
author = {Kelly, Gregory Maxwell and Street, Ross},
booktitle = {Categ. Semin. Proc. Sydney Categ. Theory Semin. 1972/1973},
doi = {10.1007/BFb0063101},
editor = {Kelly, Gregory Maxwell},
isbn = {978-3-540-06966-9},
pages = {75--103},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Review of the elements of 2-categories},
year = {1974}
}
@inproceedings{Petricek2014,
abstract = {The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional resources or properties of the execution environment (rebindable resources; platform version in a cross-platform application). The recently introduced notion of coeffects captures the latter, whole-context properties, but it failed to capture fine-grained per-variable properties. We remedy this by developing a generalized coeffect system with annotations indexed by a coeffect shape. By instantiating a concrete shape, our system captures previously studied flat (whole-context) coeffects, but also structural (per-variable) coeffects, making coeffect analyses more useful. We show that the structural system enjoys desirable syntactic properties and we give a categorical semantics using extended notions of indexed comonad. The examples presented in this paper are based on analysis of established language features (liveness, linear logics, dataflow, dynamic scoping) and we argue that such context-aware properties will also be useful for future development of languages for increasingly heterogeneous and distributed platforms.},
address = {New York, New York, USA},
author = {Petricek, Tomas and Orchard, Dominic and Mycroft, Alan},
booktitle = {Proc. 19th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '14},
doi = {10.1145/2628136.2628160},
isbn = {9781450328739},
issn = {0362-1340},
keywords = {a key feature and,coeffects,context,contribution of,for capturing various no-,in this paper,indexed comonads,programming,tions of context in,types,we develop a calculus},
pages = {123--135},
publisher = {ACM Press},
title = {Coeffects},
year = {2014}
}
@inproceedings{Luu2016,
abstract = {Cryptocurrencies record transactions in a decentralized data structure called a blockchain. Two of the most popular cryptocurrencies, Bitcoin and Ethereum, support the fea-ture to encode rules or scripts for processing transactions. This feature has evolved to give practical shape to the ideas of smart contracts, or full-fledged programs that are run on blockchains. Recently, Ethereum's smart contract system has seen steady adoption, supporting tens of thousands of contracts, holding millions dollars worth of virtual coins. In this paper, we investigate the security of running smart contracts based on Ethereum in an open distributed network like those of cryptocurrencies. We introduce several new se-curity problems in which an adversary can manipulate smart contract execution to gain profit. These bugs suggest subtle gaps in the understanding of the distributed semantics of the underlying platform. As a refinement, we propose ways to enhance the operational semantics of Ethereum to make con-tracts less vulnerable. For developers writing contracts for the existing Ethereum system, we build a symbolic execution tool called Oyente to find potential security bugs. Among 19, 366 existing Ethereum contracts, Oyente flags 8, 833 of them as vulnerable, including the TheDAO bug which led to a 60 million US dollar loss in June 2016. We also discuss the severity of other attacks for several case studies which have source code available and confirm the attacks (which target only our accounts) in the main Ethereum network.},
address = {New York, New York, USA},
author = {Luu, Loi and Chu, Duc-Hiep and Olickel, Hrishi and Saxena, Prateek and Hobor, Aquinas},
booktitle = {Proc. 2016 ACM SIGSAC Conf. Comput. Commun. Secur. - CCS'16},
doi = {10.1145/2976749.2978309},
isbn = {9781450341394},
issn = {15437221},
pages = {254--269},
publisher = {ACM Press},
title = {Making Smart Contracts Smarter},
year = {2016}
}
@article{Freyd1973,
author = {Freyd, Peter},
doi = {10.1016/0022-4049(73)90031-5},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jun,
number = {2},
pages = {171--191},
title = {Concreteness},
volume = {3},
year = {1973}
}
@article{Gumm2001a,
abstract = {Functors preserving weak pullbacks provide the basis for a rich structure theory of coalgebras. We give an easy to use criterion to check whether a functor preserves weak pullbacks. We apply the characterization to the functor F which associates a set X with the set F(X) of all filters on X. It turns out that this functor preserves weak pullbacks, yet does not preserve weak generalized pullbacks. Since topological spaces can be considered as F-coalgebras, in fact they constitute a covariety, we find that the intersection of subcoalgebras need not be a coalgebra, and 1-generated F-coalgebras need not exist.},
author = {Gumm, H. Peter},
doi = {10.1007/s00012-001-8156-x},
journal = {Algebr. universalis},
number = {2-3},
pages = {135--147},
title = {Functors for Coalgebras},
volume = {45},
year = {2001}
}
@article{Dostal2014,
abstract = {Sifted colimits (those that commute with finite products in sets) play a major role in categorical universal algebra. For example, varieties of (many-sorted) algebras are precisely the free cocompletions under sifted colimits of (many-sorted) Lawvere theories. Such a characterisation does not depend on the existence of finite products in algebraic theories, but on the above fact that these products commute with sifted colimits and another condition: finite products form a sound class of limits. In this paper we study the notion of soundness for general classes of weights in enriched category theory. We show that soundness of a given class of weights is equivalent to having a `nice' characterisation of flat weights for that class. As an application, we give an elementary characterisation of sifted weights for the enrichment in categories and in preorders. We also provide a number of examples of sifted weights using our elementary criterion.},
archivePrefix = {arXiv},
arxivId = {1405.3090},
author = {Dost{\'{a}}l, Mat{\v{e}}j and Velebil, Jiř{\'{i}}},
eprint = {1405.3090},
month = may,
pages = {1--15},
title = {An elementary characterisation of sifted weights},
year = {2014}
}
@incollection{Jacobs2014,
author = {Jacobs, Bart and Silva, Alexandra},
booktitle = {Horizons Mind. A Tribut. to Prakash Panangaden},
doi = {10.1007/978-3-319-06880-0_20},
isbn = {9783319068794},
issn = {16113349},
pages = {384--406},
title = {Automata learning: a categorical perspective},
year = {2014}
}
@inproceedings{Governatori2005,
abstract = {This paper presents a formal system for reasoning about violations of obligations in contracts. The system is based on the formalism for the representation of contrary-to-duty obligations. These are the obligations that take place when other obligations are violated as typically applied to penalties in contracts. The paper shows how this formalism can be mapped onto the key policy concepts of a contract specification language. This language, called Business Contract Language (BCL) was previously developed to express contract conditions of relevance for run time contract monitoring. The aim of this mapping is to establish a formal underpinning for this key subset of BCL.},
author = {Governatori, Guido and Milosevic, Zoran},
booktitle = {Ninth IEEE Int. EDOC Enterp. Comput. Conf.},
doi = {10.1109/EDOC.2005.13},
isbn = {0-7695-2441-9},
issn = {15417719},
pages = {46--57},
publisher = {IEEE},
title = {Dealing with contract violations: formalism and domain specific language},
year = {2005}
}
@article{Milius2013,
author = {Milius, Stefan and Moss, Lawrence S. and Schwencke, Daniel},
doi = {10.2168/LMCS-9(3:28)2013},
editor = {unknown Anonymous},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
month = sep,
number = {3},
pages = {1--52},
title = {Abstract GSOS Rules and a Modular Treatment of Recursive Definitions},
volume = {9},
year = {2013}
}
@article{Craig2016,
abstract = {Linking clinical and phenotype variables across data sets will both power precision medicine studies and introduce new privacy risks},
author = {Craig, David W.},
doi = {10.1038/nmeth.3779},
isbn = {doi:10.1038/nmeth.3779},
issn = {1548-7091},
journal = {Nat. Methods},
month = feb,
number = {3},
pages = {211--212},
pmid = {26914204},
publisher = {Nature Publishing Group},
title = {Understanding the links between privacy and public data sharing},
volume = {13},
year = {2016}
}
@article{Carboni1998,
author = {Carboni, Aurelio and Kelly, Gregory Maxwell and Verity, Dominic and Wood, Richard J.},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Adjunction,Equipment,Span},
number = {5},
pages = {82--136},
title = {A 2-categorical approach to change of base and geometric morphisms II},
volume = {4},
year = {1998}
}
@article{Vidal2010,
author = {Vidal, J Climent and Tur, J Soliveres},
journal = {Extr. Math.},
keywords = {morphism of eilenberg-moore,morphism of kleisli,transformation of kleisli},
number = {1},
pages = {1--61},
title = {Kleisli and Eilenberg-Moore Constructions as Parts of Biadjoint Situations},
volume = {25},
year = {2010}
}
@incollection{Litak2012,
author = {Litak, Tadeusz and Pattinson, Dirk and Sano, Katsuhiko and Schr{\"{o}}der, Lutz},
booktitle = {Proc. 39th Int. Colloq. Autom. Lang. Program. ICALP 2012},
doi = {10.1007/978-3-642-31585-5_29},
editor = {Wattenhofer, Kurt Mehlhorn and Andrew Pitts and Roger},
pages = {299--311},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Coalgebraic predicate logic},
year = {2012}
}
@inproceedings{Kifer2009,
abstract = {In this paper we present a method for reasoning about privacy using the concepts of exchangeability and deFinetti's theorem. We illustrate the usefulness of this technique by using it to attack a popular data sanitization scheme known as Anatomy. We stress that Anatomy is not the only sanitization scheme that is vulnerable to this attack. In fact, any scheme that uses the random worlds model, i.i.d. model, or tuple-independent model needs to be re-evaluated. The difference between the attack presented here and others that have been proposedin the past is that we do not need extensive background knowledge. An attacker only needs to know the nonsensitive attributes of one individual in the data, and can carry out this attack just by building a machine learning model over the sanitized data. The reason this attack is successful is that it exploits a subtle flaw in the way prior work computed the probability of disclosure of a sensitive attribute. We demonstrate this theoretically, empirically, and with intuitive examples. We also discuss how this generalizes to many other privacy schemes.},
address = {New York, New York, USA},
author = {Kifer, Daniel},
booktitle = {Proc. 35th SIGMOD Int. Conf. Manag. data - SIGMOD '09},
doi = {10.1145/1559845.1559861},
isbn = {9781605585512},
keywords = {privacy,random worlds},
pages = {127},
publisher = {ACM Press},
title = {Attacks on privacy and deFinetti's theorem},
year = {2009}
}
@article{Mesablishvili2006,
author = {Mesablishvili, Bachuki},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {(co)monadicity,Coring,Descent data,Monad of effective descent type,Separable functor},
number = {1},
pages = {1--45},
title = {Monads of effective descent type and comonadicity},
volume = {16},
year = {2006}
}
@book{Barr1999,
abstract = {This book is a textbook in basic category theory, written specifically to be read by researchers and students in computing science. The authors expound the constructions basic to category theory in the context of examples and applications to computing science. Some categorical ideas and constructions are already used heavily in computing sciences and many of these use are described. Other ideas, in particular the concept of adjoint have not appeared as widely in the computing science literature. The authors give an elementary exposition of those ideas they believe to be basic categorical tools, with pointers to possible application. Michael Barr is Peter Redpath Professor in the Department of Mathematics and Statistics at McGill University in Montreal, Quebec. Charles Wells is Professor of Mathematics at Case Western Reserve University in Cleveland, Ohio. This new edition contains all the material from the first and second editions, including the four chapters excised from the second edition and the solutions to all the exercises, as well as added material on factorization systems, monoidal categories, and other topics. All errors known to the authors have been corrected.},
author = {Barr, Michael and Wells, Charles},
edition = {3},
isbn = {2-921120-31-3},
pages = {526},
publisher = {Centre de recherches math{\'{e}}matiques},
title = {Category Theory for Computing Science},
year = {1999}
}
@article{Almeida1990,
author = {Almeida, Jorge},
doi = {10.1007/BF01190713},
issn = {0002-5240},
journal = {Algebr. Universalis},
month = sep,
number = {3},
pages = {333--350},
title = {On pseudovarieties, varieties of languages, filters of congruences, pseudoidentities and related topics},
volume = {27},
year = {1990}
}
@book{Johnstone1982,
author = {Johnstone, Peter T.},
isbn = {0521337798, 9780521337793},
pages = {398},
publisher = {Cambridge University Press},
title = {Stone spaces},
type = {Book},
year = {1982}
}
@article{Kick2006,
abstract = {We give a coalgebraic formulation of timed processes and their operational semantics. We model time by a monoid called a “time domain”, and we model processes by “timed transition systems”, which amount to partial monoid actions of the time domain or, equivalently, coalgebras for an “evolution comonad” generated by the time domain. All our examples of time domains satisfy a partial closure property, yielding a distributive law of a monad for total monoid actions over the evolution comonad, and hence a distributive law of the evolution comonad over a dual comonad for total monoid actions. We show that the induced coalgebras are exactly timed transition systems with delay operators. We then integrate our coalgebraic formulation of time qua timed transition systems into Turi and Plotkin's formulation of structural operational semantics in terms of distributive laws. We combine timing with action via the more general study of the combination of two arbitrary sorts of behaviour whose operational semantics may interact. We give a modular account of the operational semantics for a combination induced by that of each of its components. Our study necessitates the investigation of products of comonads. In particular, we characterise when a monad lifts to the category of coalgebras for a product comonad, providing constructions with which one can readily calculate.},
author = {Kick, Marco and Power, A. John and Simpson, Alex},
doi = {10.1016/j.ic.2005.11.003},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {delay operators,distributive laws,evolution comonads,modularity,structural operational semantics,time domains,timed transition systems},
month = apr,
number = {4},
pages = {588--609},
title = {Coalgebraic semantics for timed processes},
volume = {204},
year = {2006}
}
@article{Plotkin2004a,
author = {Plotkin, Gordon D.},
doi = {10.1016/j.jlap.2004.03.009},
issn = {15678326},
journal = {J. Log. Algebr. Program.},
keywords = {59,abstract machines,big step semantics,concurrency,i am delighted to,induction,labelled,on sos,operational semantics,see my aarhus notes,semantics,semantics of programming languages,small-step,static semantics,structural,structural operational semantics,transition systems,$\lambda$ -calculus},
month = jul,
pages = {3--15},
title = {The origins of structural operational semantics},
volume = {60-61},
year = {2004}
}
@article{Rosebrugh2002,
author = {Rosebrugh, Robert and Wood, R. J.},
doi = {10.1016/S0022-4049(02)00140-8},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = nov,
number = {1-3},
pages = {327--353},
title = {Distributive laws and factorization},
volume = {175},
year = {2002}
}
@article{Jaziri2014,
author = {Jaziri, Samy and Larsen, Kim G. and Mardare, Radu and Xue, Bingtian},
doi = {10.1016/j.entcs.2014.10.011},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {complete axiomatization,non-compact modal logics,timed modal logic},
pages = {183--210},
publisher = {Elsevier B.V.},
title = {Adequacy and Complete Axiomatization for Timed Modal Logic},
volume = {308},
year = {2014}
}
@article{Heunen2009a,
abstract = {The aim of this paper is to relate algebraic quantum mechanics to topos theory, so as to construct new foundations for quantum logic and quantum spaces. Motivated by Bohr's idea that the empirical content of quantum physics is accessible only through classical physics, we show how a C*-algebra of observables A induces a topos T(A) in which the amalgamation of all of its commutative subalgebras comprises a single commutative C*-algebra. According to the constructive Gelfand duality theorem of Banaschewski and Mulvey, the latter has an internal spectrum S(A) in T(A), which in our approach plays the role of a quantum phase space of the system. Thus we associate a locale (which is the topos-theoretical notion of a space and which intrinsically carries the intuitionistic logical structure of a Heyting algebra) to a C*-algebra (which is the noncommutative notion of a space). In this setting, states on A become probability measures (more precisely, valuations) on S(A), and self-adjoint elements of A define continuous functions (more precisely, locale maps) from S(A) to Scott's interval domain. Noting that open subsets of S(A) correspond to propositions about the system, the pairing map that assigns a (generalized) truth value to a state and a proposition assumes an extremely simple categorical form. Formulated in this way, the quantum theory defined by A is essentially turned into a classical theory, internal to the topos T(A).},
archivePrefix = {arXiv},
arxivId = {0709.4364},
author = {Heunen, Chris and Landsman, Nicolaas P. and Spitters, Bas},
doi = {10.1007/s00220-009-0865-6},
eprint = {0709.4364},
issn = {0010-3616},
journal = {Commun. Math. Phys.},
month = oct,
number = {1},
pages = {63--110},
title = {A Topos for Algebraic Quantum Theory},
volume = {291},
year = {2009}
}
@incollection{Bonsangue1993a,
author = {Bonsangue, Marcello M. and Kok, Joost N.},
booktitle = {Math. Found. Comput. Sci.},
pages = {301--310},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Isomorphisms between Predicates and State Transformers},
type = {Conference proceedings (article)},
year = {1993}
}
@article{Makarov2006,
abstract = {It is well-known that a constructive proof of a $\Pi$20 formula F written as a $\lambda$-term via Curry-Howard isomorphism, computes a function that witnesses F. Murthy [Murthy, C.R., Classical proofs as programs: How, what and why, Technical Report TR 91-1215, Cornell University, Department of Computer Science (1991)] outlined an extension of this result to classical logic, with the double-negation rule mapped to Felleisen's control operator C [Felleisen, M., D. Friedman, E. Kohlbecker and B. Duba, A syntactic theory of sequential control, Theoretical Computer Science 52 (1987), pp. 205-237]. Since C is similar to call/cc operator in Scheme and SML/NJ, this opens a possibility of extracting programs in these languages from classical proofs. However, even though the basic idea has appeared in the literature, there appears to be little work that uses Griffin's extension of the Curry-Howard isomorphism to extract practical programs in real programming languages. In this article, we fill in missing steps in Murthy's argument and extend his method to encompass more interesting proofs by allowing additional ubiquitous inference rules: equality rules, rules for atomic formulas (such as transitivity of {less-than or slanted equal to}), and rules for pairs of dual decidable atoms (such as {less-than or slanted equal to} and >). We illustrate the usefulness of this extension with a complete example of program extraction. {\textcopyright} 2006 Elsevier B.V. All rights reserved.},
author = {Makarov, Yevgeniy},
doi = {10.1016/j.entcs.2005.11.071},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {Curry-Howard isomorphism,Program extraction,classical logic,control operators,functional programming,lambda calculus},
month = may,
number = {1 SPEC. ISS.},
pages = {521--542},
publisher = {Elsevier B.V.},
title = {Practical Program Extraction from Classical Proofs},
volume = {155},
year = {2006}
}
@incollection{Belnap1977,
address = {Dordrecht},
author = {Belnap, Nuel D.},
booktitle = {Mod. Uses Mult. Log.},
doi = {10.1007/978-94-010-1161-7_2},
pages = {5--37},
publisher = {Springer Netherlands},
series = {Episteme},
title = {A Useful Four-Valued Logic},
volume = {2},
year = {1977}
}
@article{Gischer1988,
abstract = {Pomsets have been introduced as a model of concurrency. Since a pomset is a string in which the total order has been relaxed to be a partial order, in this paper we view them as a generalization of strings, and investigate their algebraic properties. In particular, we investigate the axiomatic properties of pomsets, sets of pomsets and ideals of pomsets, under such operations as concatenation, parallel composition, union and their associated closure operations. We find that the equational theory of sets, pomsets under concatenation, parallel composition and union is finitely axiomatizable, whereas the theory of languages under the analogous operations is not. A similar result is obtained for ideals of pomsets, which incorporate the notion of subsumption which is also known as augmentation. Finally, we show that the addition of any closure operation (parallel or serial) leads to nonfinite axiomatizability of the resulting equational theory. {\textcopyright} 1988.},
author = {Gischer, Jay L.},
doi = {10.1016/0304-3975(88)90124-7},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = nov,
number = {2-3},
pages = {199--224},
title = {The equational theory of pomsets},
volume = {61},
year = {1988}
}
@article{Gunter1992,
abstract = {This paper introduces an operator M called the mixed powerdomain which generalizes the convex (Plotkin) powerdomain. The construction is based on the idea of representing partial information about a set of data items using a pair of sets, one representing partial information in the manner of the upper (Smyth) powerdomain and the other in the manner of the lower (Hoare) powerdomain where the components of such pairs are required to satisfy a consistency condition. This provides a richer family of meaningful partial descriptions than are available in the convex powerdomain and also makes it possible to include the empty set in a satisfactory way. The new construct is given a rigorous mathematical treatment like that which has been applied to the known powerdomains. It is proved that M is a continuous functor on bifinite domains which is left adjoint to the forgetful functor from a category of continuous structures called mix algebras. For a domain D with a coherent Scott topology, elements of MD can be represented as pairs (U, V) where U ⊆ D is a compact upper set, V ⊆ D is a closed set and the downward closure of U {frown} V is equal to V. A Stone dual characterization of M is also provided. {\textcopyright} 1992.},
author = {Gunter, Carl A.},
doi = {10.1016/0304-3975(92)90017-A},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = sep,
number = {2},
pages = {311--334},
title = {The mixed powerdomain},
volume = {103},
year = {1992}
}
@article{Uustalu2008,
abstract = {We argue that symmetric (semi)monoidal comonads provide a means to structure context-dependent notions of computation such as notions of dataflow computation (computation on streams) and of tree relabelling as in attribute evaluation. We propose a generic semantics for extensions of simply typed lambda calculus with context-dependent operations analogous to the Moggi-style semantics for effectful languages based on strong monads. This continues the work in the early 90s by Brookes, Geva and Van Stone on the use of computational comonads in intensional semantics. ?? 2008 Elsevier B.V. All rights reserved.},
author = {Uustalu, Tarmo and Vene, Varmo},
doi = {10.1016/j.entcs.2008.05.029},
isbn = {15710661},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {coKleisli semantics,context-dependent computation,dataflow computation,symmetric monoidal comonads,tree transformations},
number = {5},
pages = {263--284},
publisher = {Elsevier B.V.},
title = {Comonadic notions of computation},
volume = {203},
year = {2008}
}
@inproceedings{Machanavajjhala2008,
abstract = {In this paper, we propose the first formal privacy analysis of a data anonymization process known as the synthetic data generation, a technique becoming popular in the statistics community. The target application for this work is a mapping program that shows the commuting patterns of the population of the United States. The source data for this application were collected by the U.S. Census Bureau, but due to privacy constraints, they cannot be used directly by the mapping program. Instead, we generate synthetic data that statistically mimic the original data while providing privacy guarantees. We use these synthetic data as a surrogate for the original data. We find that while some existing definitions of privacy are inapplicable to our target application, others are too conservative and render the synthetic data useless since they guard against privacy breaches that are very unlikely. Moreover, the data in our target application is sparse, and none of the existing solutions are tailored to anonymize sparse data. In this paper, we propose solutions to address the above issues.},
author = {Machanavajjhala, Ashwin and Kifer, Daniel and Abowd, John and Gehrke, Johannes and Vilhuber, Lars},
booktitle = {2008 IEEE 24th Int. Conf. Data Eng.},
doi = {10.1109/ICDE.2008.4497436},
isbn = {978-1-4244-1836-7},
issn = {10844627},
month = apr,
pages = {277--286},
publisher = {IEEE},
title = {Privacy: Theory meets Practice on the Map},
year = {2008}
}
@incollection{Bilkova2008,
author = {B{\'{i}}lkov{\'{a}}, Marta and Palmigiano, Alessandra and Venema, Yde},
booktitle = {Adv. Modal Log.},
editor = {Areces, Carlos and Goldblatt, Robert},
isbn = {978-1904987680},
keywords = {coalgebra,coalgebraic modal-,completeness,derivation system,gentzen calculus,ity,modal logic},
number = {2},
pages = {1--21},
publisher = {College Publications},
title = {Proof systems for the coalgebraic cover modality},
volume = {7},
year = {2008}
}
@article{Jacobs2012a,
abstract = {Traditionally in categorical logic predicates on an object/type X are represented as subobjects of X. Here we break with that tradition and use maps of the form p : X --> X + X with [id, id] o p = id as predicates. This new view gives a more dynamic, measurement-oriented view on predicates, that works well especially in a quantitative setting. In classical logic (in the category of sets) these new predicates coincide with the traditional ones (subsets, or characteristic maps X --> {0,1}); in probabilistic logic (in the category of sets and stochastic matrices), the new predicates correspond to fuzzy predicates X --> [0,1]; and in quantum logic (in Hilbert spaces) they correspond to effects (positive endomaps below the identity), which may be understood as fuzzy predicates on a changed basis. It is shown that, under certain conditions about coproducts +, predicates p : X --> X + X form effect algebras and carry a scalar multiplication (with probabilities). Suitable substitution functors give rise to indexed/fibred categories. In the quantum case the famous Born rule - describing the probability of observation outcomes - follows directly from the form of these substitution functors: probability calculation becomes substitution in predicate logic. Moreover, the characteristic maps associated with predicates provide tests in a dynamic logic, and turn out to capture measurement in a form that uniformly covers the classical, probabilistic and quantum case. The probabilities incorporated in predicates (as eigenvalues) serves as weights for the possible measurement outcomes.},
archivePrefix = {arXiv},
arxivId = {1205.3940},
author = {Jacobs, Bart},
eprint = {1205.3940},
journal = {ArXiv e-prints},
month = may,
title = {New Directions in Categorical Logic, for Classical, Probabilistic and Quantum Logic},
year = {2012}
}
@article{Benthem2012,
author = {van Benthem, Johan and Bezhanishvili, Nick and Hodkinson, Ian},
doi = {10.1007/s11225-012-9388-9},
issn = {0039-3215},
journal = {Stud. Log.},
month = feb,
pages = {31--60},
publisher = {Springer Netherlands},
title = {Sahlqvist correspondence for modal mu-calculus},
volume = {100},
year = {2012}
}
@inproceedings{Cirstea2015,
address = {Dagstuhl, Germany},
author = {C{\^{i}}rstea, Corina},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci. (CALCO 2015)},
doi = {http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.66},
editor = {Moss, Lawrence S and Sobocinski, Pawel},
isbn = {978-3-939897-84-2},
issn = {1868-8969},
pages = {66--85},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Canonical coalgebraic linear time logics},
volume = {35},
year = {2015}
}
@inproceedings{Losch2013,
address = {New York, New York, USA},
author = {L{\"{o}}sch, Steffen and Pitts, Andrew M.},
booktitle = {Proc. 40th Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '13},
doi = {10.1145/2429069.2429073},
isbn = {9781450318327},
keywords = {denotational semantics,domain theory,full ab-,nominal sets,straction,symmetry},
number = {Theorem 8},
pages = {3},
publisher = {ACM Press},
title = {Full abstraction for nominal Scott domains},
year = {2013}
}
@article{Diers1976,
author = {Diers, Yves},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {4},
pages = {363--396},
title = {Compl{\'{e}}tion monadique},
volume = {17},
year = {1976}
}
@article{Ginsberg1988,
author = {Ginsberg, Matthew L.},
doi = {10.1111/j.1467-8640.1988.tb00280.x},
issn = {0824-7935},
journal = {Comput. Intell.},
keywords = {circumscription,commonsense,defaults,knowledge representation,nonmonotonic reasoning,reasoning,theorem proving,truth maintenance},
month = sep,
number = {3},
pages = {265--316},
title = {Multivalued logics: a uniform approach to reasoning in artificial intelligence},
volume = {4},
year = {1988}
}
@article{Carboni1991,
author = {Carboni, Aurelio and Kelly, Gregory Maxwell and Wood, Richard J.},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {1},
pages = {47--95},
title = {A 2-categorical approach to change of base and geometric morphisms I},
volume = {32},
year = {1991}
}
@inproceedings{Kifer2010,
address = {New York, New York, USA},
author = {Kifer, Daniel and Lin, Bing-rong},
booktitle = {Proc. twenty-ninth ACM SIGMOD-SIGACT-SIGART Symp. Princ. database Syst. data - Pod. '10},
doi = {10.1145/1807085.1807106},
isbn = {9781450300339},
keywords = {axioms,privacy,utility},
pages = {147},
publisher = {ACM Press},
title = {Towards an axiomatization of statistical privacy and utility},
year = {2010}
}
@book{Baier2008,
author = {Baier, Christel and Katoen, Joost-Pieter},
isbn = {9780262026499},
pages = {984},
publisher = {MIT Press},
series = {Computer Science and Intelligent Systems},
title = {Principles of Model Checking},
year = {2008}
}
@inproceedings{Kobayashi2009,
abstract = {The model checking of higher-order recursion schemes has important applications in the verification of higher-order programs. Ong has previously shown that the modal mu-calculus model checking of trees generated by order-n recursion scheme is n-EXPTIME complete, but his algorithm and its correctness proof were rather complex. We give an alternative, type-based verification method: Given a modal mu-calculus formula, we can construct a type system in which a recursion scheme is typable if, and only if, the (possibly infinite, ranked) tree generated by the scheme satisfies the formula. The model checking problem is thus reduced to a type checking problem. Our type-based approach yields a simple verification algorithm, and its correctness proof (constructed without recourse to game semantics) is comparatively easy to understand. Furthermore, the algorithm is polynomial-time in the size of the recursion scheme, assuming that the formula and the largest order and arity of non-terminals of the recursion scheme are fixed.},
archivePrefix = {arXiv},
arxivId = {1012.1255},
author = {Kobayashi, Naoki and Ong, C.-H. Luke},
booktitle = {Proc. 24th Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2009.29},
eprint = {1012.1255},
isbn = {978-0-7695-3746-7},
issn = {10436871},
month = aug,
pages = {179--188},
publisher = {IEEE},
title = {A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes},
year = {2009}
}
@article{Adamek2012e,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Trnkov{\'{a}}, V{\v{e}}ra},
doi = {10.1016/j.jpaa.2012.02.026},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = mar,
publisher = {Elsevier B.V.},
title = {Relatively terminal coalgebras},
year = {2012}
}
@inproceedings{Barth2006,
abstract = {Contextual integrity is a conceptual framework for un- derstanding privacy expectations and their implications de- veloped in the literature on law, public policy, and political philosophy. We formalize some aspects of contextual in- tegrity in a logical framework for expressing and reasoning about norms of transmission of personal information. In comparison with access control and privacy policy frame- works such as RBAC, EPAL, and P3P, these norms focus on who personal information is about, how it is transmit- ted, and past and future actions by both the subject and the users of the information. Norms can be positive or neg- ative depending on whether they refer to actions that are allowed or disallowed. Our model is expressive enough to capture naturally many notions of privacy found in legisla- tion, including those found in HIPAA, COPPA, and GLBA. A number of important problems regarding compliance with privacy norms, future requirements associated with specific actions, and relations between policies and legal standards reduce to standard decision procedures for temporal logic.},
archivePrefix = {arXiv},
arxivId = {arXiv:1011.1669v3},
author = {Barth, Adam and Datta, Anupam and Mitchell, J.C. and Nissenbaum, Helen},
booktitle = {2006 IEEE Symp. Secur. Priv.},
doi = {10.1109/SP.2006.32},
eprint = {arXiv:1011.1669v3},
isbn = {0-7695-2574-1},
issn = {10816011},
pages = {15 pp.--198},
pmid = {25246403},
publisher = {IEEE},
title = {Privacy and contextual integrity: framework and applications},
volume = {2006},
year = {2006}
}
@article{Cecaj2016,
abstract = {The analysis of multiple datasets on users' behaviors opens interesting information fusion possibilities and, at the same time, creates a potential for re-identification and de-anonymization of users' data. On the one hand, this kind of approaches can breach users' privacy despite anonymization. On the other hand, combining different datasets is a key enabler for advanced context-awareness in that information from multiple sources can complement and enrich each other. In this work we analyze different anonymized mobility datasets in the direction of highlighting re-identification and information fusion possibilities. In particular we focus on call detail record (CDR) datasets released by mobile telecom operators and datasets comprising geo-localized messages released by social network sites. Results shows that: (1) in line with previous findings, few (about 4) data points are enough to uniquely pin point the majority (90 %) of the users, (2) more than 20 % of CDR users have a single social network user exhibiting a number of matching data points. We speculate that these two users might be the same person. (3) We derive an estimate of the probability of two users begin the same person given the number of data points they have in common, and estimate that for 3 % of the social network users we can find a CDR user very likely (>90 % probability) to be the same person.},
author = {Cecaj, Alket and Mamei, Marco and Zambonelli, Franco},
doi = {10.1007/s12652-015-0303-x},
issn = {1868-5137},
journal = {J. Ambient Intell. Humaniz. Comput.},
keywords = {De-anonymization,Information fusion,Mobility patterns},
month = feb,
number = {1},
pages = {83--96},
publisher = {Springer Berlin Heidelberg},
title = {Re-identification and information fusion between anonymized CDR and social network data},
volume = {7},
year = {2016}
}
@incollection{Venema2013,
author = {Venema, Yde and Vosmaer, Jacob},
booktitle = {Leo Esakia Duality Modal Intuitionistic Logics},
doi = {10.1007/978-94-017-8860-1_6},
editor = {Bezhanishvili, Guram},
pages = {119--153},
publisher = {Springer Netherlands},
series = {Outstanding Contributions to Logic},
title = {Modal logic and the Vietoris functor},
volume = {4},
year = {2014}
}
@article{Dong2015,
abstract = {The task of {\em data fusion} is to identify the true values of data items (eg, the true date of birth for {\em Tom Cruise}) among multiple observed values drawn from different sources (eg, Web sites) of varying (and unknown) reliability. A recent survey\cite{LDL+12} has provided a detailed comparison of various fusion methods on Deep Web data. In this paper, we study the applicability and limitations of different fusion techniques on a more challenging problem: {\em knowledge fusion}. Knowledge fusion identifies true subject-predicate-object triples extracted by multiple information extractors from multiple information sources. These extractors perform the tasks of entity linkage and schema alignment, thus introducing an additional source of noise that is quite different from that traditionally considered in the data fusion literature, which only focuses on factual errors in the original sources. We adapt state-of-the-art data fusion techniques and apply them to a knowledge base with 1.6B unique knowledge triples extracted by 12 extractors from over 1B Web pages, which is three orders of magnitude larger than the data sets used in previous data fusion papers. We show great promise of the data fusion approaches in solving the knowledge fusion problem, and suggest interesting research directions through a detailed error analysis of the methods.},
archivePrefix = {arXiv},
arxivId = {1503.00302},
author = {Dong, Xin Luna and Gabrilovich, Evgeniy and Heitz, Geremy and Horn, Wilko and Murphy, Kevin and Sun, Shaohua and Zhang, Wei},
doi = {10.14778/2732951.2732962},
eprint = {1503.00302},
issn = {21508097},
journal = {Proc. VLDB Endow.},
month = jun,
number = {10},
pages = {881--892},
title = {From data fusion to knowledge fusion},
volume = {7},
year = {2014}
}
@article{Hyland2006,
author = {Hyland, Martin and Plotkin, Gordon D. and Power, A. John},
doi = {10.1016/j.tcs.2006.03.013},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {computational effect,lawvere theory,modularity,monad},
month = jul,
number = {1-3},
pages = {70--99},
title = {Combining effects: Sum and tensor},
volume = {357},
year = {2006}
}
@article{Athorne2012,
abstract = {The relative cell complexes with respect to a generating set of cofibrations are an important class of morphisms in any model structure. In the particular case of the standard (algebraic) model structure on $\textbf{Top}$, we give a new expression of these morphisms by defining a category of relative cell complexes, which has a forgetful functor to the arrow category. This allows us to prove a conjecture of Richard Garner: considering the algebraic weak factorisation system given in that algebraic model structure between cofibrations and trivial fibrations, we show that the category of relative cell complexes is equivalent to the category of coalgebras.},
archivePrefix = {arXiv},
arxivId = {1202.6034},
author = {Athorne, Thomas},
eprint = {1202.6034},
journal = {ArXiv e-prints},
month = feb,
pages = {28},
title = {The coalgebraic structure of cell complexes},
year = {2012}
}
@article{Church2008,
author = {Church, a},
doi = {10.2307/2269030},
issn = {00324728},
journal = {J. Symb. Log.},
number = {1},
pages = {40--41},
title = {A Note on the Entscheidungsproblem},
volume = {1},
year = {2008}
}
@article{Staton2008,
author = {Staton, Sam},
doi = {10.1109/LICS.2008.43},
isbn = {978-0-7695-3183-0},
issn = {1043-6871},
journal = {2008 23rd Annu. IEEE Symp. Log. Comput. Sci.},
month = jun,
pages = {166--177},
publisher = {Ieee},
title = {General Structural Operational Semantics through Categorical Logic},
year = {2008}
}
@article{Isbell1972,
author = {Isbell, John R.},
journal = {Am. J. Math.},
number = {2},
pages = {535--596},
title = {General Functorial Semantics, I},
volume = {94},
year = {1972}
}
@book{Adamek1989,
address = {Dordrecht},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Trnkov{\'{a}}, V{\v{e}}ra},
isbn = {978-0792300106},
pages = {492},
publisher = {Kluwer Academic Publishers},
series = {Mathematics and Its Applications},
title = {Automata and algebras in categories},
year = {1989}
}
@article{Barr1994,
author = {Barr, Michael},
doi = {10.1016/0304-3975(94)90060-4},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = feb,
number = {1},
pages = {189--192},
title = {Additions and corrections to “Terminal coalgebras in well-founded set theory”},
volume = {124},
year = {1994}
}
@inproceedings{Urabe2015,
address = {Dagstuhl, Germany},
author = {Urabe, Natsuki and Hasuo, Ichiro},
booktitle = {Proc. 6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.320},
editor = {Moss, Lawrence S and Sobocinski, Pawel},
isbn = {978-3-939897-84-2},
issn = {1868-8969},
pages = {320--335},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Coalgebraic infinite traces and Kleisli simulations},
volume = {35},
year = {2015}
}
@incollection{Preugschat2012,
abstract = {We present a framework for obtaining effective characterizations of simple fragments of future temporal logic (LTL) with the natural numbers as time domain. The framework is based on prophetic automata (also known as complete unambiguous B{\"{u}}chi automata), which enjoy strong structural properties, in particular, they separate the “finitary fraction” of a regular language of infinite words from its “infinitary fraction” in a natural fashion. Within our framework, we provide characterizations of all natural fragments of temporal logic, where, in some cases, no effective characterization had been known previously, and give lower and upper bounds for their computational complexity.},
author = {Preugschat, Sebastian and Wilke, Thomas},
booktitle = {Found. Softw. Sci. Comput. Struct.},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {135--149},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Effective characterizations of simple fragments of temporal logic using prophetic automata},
volume = {7213},
year = {2012}
}
@article{Bilkova2012a,
abstract = {The category Rel(Set) of sets and relations can be described as a category of spans and as the Kleisli category for the powerset monad. A set-functor can be lifted to a functor on Rel(Set) iff it preserves weak pullbacks. We show that these results extend to the enriched setting, if we replace sets by posets or preorders. Preservation of weak pullbacks becomes preservation of exact lax squares. As an application we present Moss's coalgebraic over posets.},
archivePrefix = {arXiv},
arxivId = {1210.1433},
author = {B{\'{i}}lkov{\'{a}}, Marta and Kurz, Alexander and Petrişan, Daniela and Velebil, Jiř{\'{i}}},
eprint = {1210.1433},
journal = {ArXiv e-prints},
month = oct,
pages = {1--28},
title = {Relation liftings on preorders and posets},
year = {2012}
}
@incollection{Dwork2008,
abstract = {Over the past five years a new approach to privacy-preserving data analysis has born fruit 13, 18, 7, 19, 5, 37, 35, 8, 32. This approach differs from much (but not all!) of the related literature in the statistics, databases, theory, and cryptography communities, in that a formal and ad omnia privacy guarantee is defined, and the data analysis techniques presented are rigorously proved to satisfy the guarantee. The key privacy guarantee that has emerged is differential privacy. Roughly speaking, this ensures that (almost, and quantifiably) no risk is incurred by joining a statistical database. In this survey, we recall the definition of differential privacy and two basic techniques for achieving it. We then show some interesting applications of these techniques, presenting algorithms for three specific tasks and three general results on differentially private learning.},
address = {Berlin, Heidelberg},
archivePrefix = {arXiv},
arxivId = {arXiv:cond-mat/9912410v1},
author = {Dwork, Cynthia},
booktitle = {Theory Appl. Model. Comput.},
doi = {10.1007/978-3-540-79228-4_1},
eprint = {9912410v1},
isbn = {9783540792277},
issn = {03029743},
pages = {1--19},
primaryClass = {arXiv:cond-mat},
publisher = {Springer Berlin Heidelberg},
title = {Differential Privacy: A Survey of Results},
volume = {4978},
year = {2008}
}
@article{Hutton1998,
abstract = {This paper is a tutorial on defining recursive descent parsers in Haskell. In the spirit of one-stop shopping, the paper combines material from three areas into a single source. The three areas are functional parsers (Burge, 1975; Wadler, 1985; Hutton, 1992; Fokker, 1995), the use of monads to structure functional programs (Wadler, 1990, 1992a, 1992b), and the use of special syntax for monadic programs in Haskell (Jones, 1995; Peterson et al., 1996). More specifically, the paper shows how to define monadic parsers using do notation in Haskell. Of course, recursive descent parsers defined by hand lack the efficiency of bottom-up parsers generated by machine (Aho et al., 1986; Mogensen, 1993; Gill and Marlow, 1995). However, for many research applications, a simple recursive descent parser is perfectly sufficient. Moreover, while parser generators typically offer a fixed set of combinators for describing grammars, the method described here is completely extensible: parsers are first-class values, and we have the full power of Haskell available to define new combinators for special applications. The method is also an excellent illustration of the elegance of functional programming.},
author = {Hutton, Graham and Meijer, Erik},
journal = {J. Funct. Program.},
number = {04},
pages = {437--444},
publisher = {Cambridge University Press},
title = {Monadic Parsing in Haskell},
volume = {8},
year = {1998}
}
@article{Floridi2011,
author = {Floridi, Luciano},
doi = {10.1023/B:MIND.0000021684.50925.c9},
isbn = {9780199232383},
issn = {0924-6495},
journal = {Minds Mach.},
keywords = {bar-hillel,carnap paradox,data,either it is raining,how,how the information has,i know,information,is another,one is inclined to,or it isn,probability distributions,reached me,say,semantic information,t,theory of strongly semantic,theory of weakly semantic,truth-values},
month = may,
number = {2},
pages = {197--221},
title = {Outline of a Theory of Strongly Semantic Information},
volume = {14},
year = {2004}
}
@incollection{Kupke2005,
abstract = {This paper studies finitary modal logics as specification languages for Set-coalgebras (coalgebras on the category of sets) using Stone duality. It is well-known that Set-coalgebras are not semantically adequate for finitary modal logics in the sense that bisimilarity does not in general coincide with logical equivalence. Stone-coalgebras (coalgebras over the category of Stone spaces), on the other hand, do provide an adequate semantics for finitary modal logics. This leads us to study the relationship of finitary modal logics and Set-coalgebras by uncovering the relationship between Set-coalgebras and Stone-coalgebras. This builds on a long tradition in modal logic, where one studies canonical extensions of modal algebras and ultrafilter extensions of Kripke frames to account for finitary logics. Our main contributions are the generalisations of two classical theorems in modal logic to coalgebras, namely the J{\'{o}}nsson-Tarski theorem giving a set-theoretic representation for each modal algebra and the bisimulation-somewhere-else theorem stating that two states of a coalgebra have the same (finitary modal) theory iff they are bisimilar (or behaviourally equivalent) in the ultrafilter extension of the coalgebra.},
author = {Kupke, Clemens and Kurz, Alexander and Pattinson, Dirk},
booktitle = {Algebr. Coalgebra Comput. Sci.},
doi = {10.1007/11548133_17},
editor = {Fiadeiro, Jos{\'{e}} and Harman, Neil and Roggenbach, Markus and Rutten, Jan},
isbn = {978-3-540-28620-2},
pages = {263--277},
publisher = {Springer Berlin / Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Ultrafilter extensions for coalgebras},
type = {Book part (with own title)},
volume = {3629},
year = {2005}
}
@incollection{Abramsky1994a,
author = {Abramsky, Samson and Jung, Achim},
booktitle = {Handb. Log. Comput. Sci.},
editor = {Abramsky, Samson and Gabby, Dov M. and Maibaum, Thomas S. E.},
isbn = {978-0198537625},
pages = {1--168},
publisher = {Oxford University Press},
title = {Domain theory},
type = {Book part (with own title)},
volume = {3},
year = {1994}
}
@phdthesis{Green2009,
abstract = {In 2006 America Online's research division leaked the web search histories of more than 600,000 of their customers. While this data had been stripped of customer names and identifying information, it nevertheless revealed deeply private information about these individuals' identities and interests. Access to information is becoming fundamental to our society, whether it is a web search or a look at one's health records. While much research has considered the problem of securing data within the database, there exist applications where the content of the users' queries is more sensitive. For example, a doctor who queries a medical records database may inadvertently reveal information that can harm his patient's interests (e.g., queries by a disease specialist might indicate a potential infection, and thus impact insurance coverage decisions). In this work we propose privacy-preserving databases in which a central database serves a pool of users without learning their query pattern. These systems will have several competing requirements. First, we require that the database operator learn nothing about which items the user is asking for, or even the user's identity. This guarantee must hold according to a strong security definition that takes into account the possibility of a malicious operator who tampers with the protocol. Secondly, we require that the database operator retain the ability to control access to items within the database. This seems quite challenging, however, since access control appears to be fundamentally incompatible with our desired privacy requirements. A promising technology for constructing oblivious databases is Oblivious Transfer (OT). In a k -out-of-N OT protocol, a Sender with a collection of N messages interacts with a Receiver such that the Receiver obtains any k of the messages, and no information about the rest of the database. For its part, the Sender learns nothing about which messages the Receiver requested. Unfortunately, while a k -items-out-of- N policy can be considered a basic form access control, it is not powerful enough for many practical applications. Furthermore, many existing OT constructions are vulnerable to selective-failure attacks that may effectively compromise user privacy if undertaken by a malicious database operator. In this work we propose several methods that address these problems efficiently and under strong definitions of security. We will then show how these techniques may be combined in order to produce a complete solution. Specifically, we propose: (1) Two new protocols for k -out-of- N Oblivious Transfer (OT) based on techniques from the field of Identity Based Encryption (IBE). Proposed by Shamir [Sha84] and realized by Boneh-Franklin [BF01], IBE is a powerful technology that greatly simplifies key distribution. We formalize the notion of using this system to blindly extract keys, and show how the primitive can be used to construct efficient fully-simulatable OT protocols (previous OT constructions are either inefficient, are proven according to unrealistic security definitions, or require strong complexity assumptions). (2) A third OT protocol that is secure in the strong Universal Composability (UC) model of Canetti [Can01]. Not only does this protocol meet a strong definition of security, but it can be generically composed with any other UC-secure protocol (including itself). This is important in the case of databases where many users may concurrently access the same database. To our knowledge, this is the first efficient adaptive OT construction to meet this definition. (3) A technique for providing strong and history-dependent access control for an oblivious database. In this model, the user is prevented from requesting items that are not permitted by her policy, while the database operator learns nothing more about the content of her requests. Our constructions are based on a new form of stateful anonymous credentials. Finally, we show how these technologies can be combined to produce a practical oblivious database. The contributions of this work are both theoretical and practical. In particular, we believe that the notion of constructing Oblivious Transfer from Identity-Based Encryption may ultimately help to expand our understanding of both primitives. Simultaneously, the constructions we propose achieve high efficiency under strong security definitions. Ultimately, we believe that this is the first work to thoroughly consider the practical tradeoffs of constructing privacy-preserving databases.},
author = {Green, Matthew Daniel},
booktitle = {ProQuest Diss. Theses},
isbn = {9781109128697},
keywords = {0984:Computer science,Applied sciences,Computer science,Computer security,Cryptography,Databases,Privacy,Secure databases},
pages = {170},
school = {Johns Hopkins University},
title = {Cryptography for secure and private databases: Enabling practical data access without compromising privacy},
year = {2009}
}
@article{Clarkson2010,
abstract = {Trace properties, which have long been used for reasoning about systems, are sets of execution traces. Hyperproperties, introduced here, are sets of trace properties. Hyperproperties can express security policies, such as secure information flow and service level agreements, that trace properties cannot. Safety and liveness are generalized to hyperproperties, and every hyperproperty is shown to be the intersection of a safety hyperproperty and a liveness hyperproperty. A verification technique for safety hyperproperties is given and is shown to generalize prior techniques for verifying secure information flow. Refinement is shown to be applicable with safety hyperproperties. A topological characterization of hyperproperties is given. [ABSTRACT FROM AUTHOR]\nCopyright of Journal of Computer Security is the property of IOS Press and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)},
author = {Clarkson, Michael R. and Schneider, Fred B.},
doi = {10.3233/JCS-2009-0393},
editor = {Sabelfeld, Andrei},
issn = {18758924},
journal = {J. Comput. Secur.},
keywords = {Security policies,information flow,liveness,safety},
month = sep,
number = {6},
pages = {1157--1210},
title = {Hyperproperties},
volume = {18},
year = {2010}
}
@inproceedings{Banaschewski1972,
author = {Banaschewski, Bernhard},
booktitle = {Gen. Topol. its Relations to Mod. Anal. Algebr. Proc. Third Prague Topol. Symp. 1971},
pages = {51--62},
publisher = {Academia Publishing House of the Czechoslovak Academy of Sciences},
title = {On profinite universal algebras},
year = {1972}
}
@article{Gabbay1998,
author = {Gabbay, Dov and Shehtman, Valentin},
doi = {10.1093/jigpal/6.1.73},
issn = {1367-0751},
journal = {Log. J. IGPL},
month = jan,
number = {1},
pages = {73--146},
title = {Products of modal logics, part 1},
volume = {6},
year = {1998}
}
@article{Enqvist2014,
author = {Enqvist, Sebastian},
doi = {10.1093/logcom/exu045},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {abstract model theory,coalgebra,lindstr{\"{o}}m,modal logic,s theorem},
month = jul,
title = {A new coalgebraic Lindstrom theorem},
year = {2014}
}
@article{Wand1979,
abstract = {We consider the problem of data type extensions. Guttag, Horowitz, and Musser have pointed out that in this situation the naive initial algebra approach requires the data type to save too much information. We formulate a category of implementations of such an extension, and we show that such a category has a final object. The resulting semantics is closer to that of Hoare, since it can be argued that an abstract data type in the sense of Hoare is a final object in the category of representations of that type. We consider as an example the specification of integer arrays, and we show that our specification yields arrays as its abstract data type. The connection with initial algebra semantics is discussed. {\textcopyright} 1979.},
author = {Wand, Mitchell},
doi = {10.1016/0022-0000(79)90011-4},
issn = {00220000},
journal = {J. Comput. Syst. Sci.},
month = aug,
number = {1},
pages = {27--44},
title = {Final algebra semantics and data type extensions},
volume = {19},
year = {1979}
}
@article{Worrell2002,
author = {Worrell, James},
doi = {10.1016/S1571-0661(04)80373-6},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = oct,
number = {1},
pages = {358--364},
title = {A Note on Coalgebras and Presheaves},
volume = {65},
year = {2002}
}
@article{Sulzmann2007,
author = {Sulzmann, Martin and Stuckey, Peter J.},
doi = {10.1017/S0956796807006569},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = sep,
number = {02},
title = {HM(X) type inference is CLP(X) solving},
volume = {18},
year = {2007}
}
@article{Bousfield1977,
author = {Bousfield, A.K.},
doi = {10.1016/0022-4049(77)90067-6},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jan,
number = {2-3},
pages = {207--220},
title = {Constructions of factorization systems in categories},
volume = {9},
year = {1977}
}
@incollection{Droste2009,
abstract = {Weighted finite automata are classical nondeterministic finite automata in which the transitions carry weights. These weights may model, for example, the cost involved when executing a transition, the resources or time needed for this, or the probability or reliability of its successful execution. Weights can also be added to classical automata with infinite state sets like pushdown automata, and this extension constitutes the general concept of weighted automata. Since their introduction in the 1960s they have stimulated research in related areas of theoretical computer science, including formal language theory, algebra, logic, and discrete structures. Moreover, weighted automata and weighted context-free grammars have found application in natural-language processing, speech recognition, and digital image compression.This book covers all the main aspects of weighted automata and formal power series methods, ranging from theory to applications. The contributors are the leading experts in their respective areas, and each chapter presents a detailed survey of the state of the art and pointers to future research. The chapters in Part I cover the foundations of the theory of weighted automata, specifically addressing semirings, power series, and fixed point theory. Part II investigates different concepts of weighted recognizability. Part III examines alternative types of weighted automata and various discrete structures other than words. Finally, Part IV deals with applications of weighted automata, including digital image compression, fuzzy languages, model checking, and natural-language processing.Computer scientists and mathematicians will find this book an excellent survey and reference volume, and it will also be a valuable resource for students exploring this exciting research area.},
archivePrefix = {arXiv},
arxivId = {arXiv:1011.1669v3},
author = {{\'{E}}sik, Zolt{\'{a}}n},
booktitle = {Handb. Weight. Autom.},
doi = {10.1007/978-3-642-01492-5 2},
editor = {Droste, Manfred and Kuich, Werner and Vogler, Heiko},
eprint = {arXiv:1011.1669v3},
isbn = {9783642014918},
issn = {1098-6596},
pages = {608},
pmid = {25246403},
publisher = {Springer Berlin Heidelberg},
series = {Monographs in Theoretical Computer Science. An EATCS Series},
title = {Fixed point theory},
year = {2009}
}
@incollection{Alvim2011,
author = {Alvim, M{\'{a}}rio S. and Andr{\'{e}}s, Miguel E. and Chatzikokolakis, Konstantinos and Palamidessi, Catuscia},
booktitle = {Found. Secur. Anal. Des. VI. FOSAD 2011},
doi = {10.1007/978-3-642-23082-0_8},
editor = {Aldini, Alessandro and Gorrieri, Roberto},
isbn = {978-3-642-23081-3},
pages = {211--230},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Quantitative Information Flow and Applications to Differential Privacy},
volume = {6858},
year = {2011}
}
@article{Day2007,
abstract = {For a small category K enriched over a suitable monoidal category V, the free completion of K under colimits is the presheaf category [K op, V]. If K is large, its free completion under colimits is the V-category P K of small presheaves on K, where a presheaf is small if it is a left Kan extension of some presheaf with small domain. We study the existence of limits and of monoidal closed structures on P K. ?? 2006 Elsevier Ltd. All rights reserved.},
archivePrefix = {arXiv},
arxivId = {math/0610439},
author = {Day, Brian J. and Lack, Stephen},
doi = {10.1016/j.jpaa.2006.10.019},
eprint = {0610439},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {3},
pages = {651--663},
primaryClass = {math},
title = {Limits of small functors},
volume = {210},
year = {2007}
}
@inproceedings{Wang2014,
abstract = {— The concept of differential privacy stems from the study of private query of datasets. In this work, we apply this concept to metric spaces to study a mechanism that randomizes a deterministic query by adding mean-zero noise to keep differential privacy. For one-shot queries, we show that privacy of an n-dimensional input implies a lower bound n − n ln(on the entropy of the randomized output, and this lower bound is achieved by adding Laplacian noise. We then consider the privacy of a discrete-time linear feedback system in which noise is added to the system output at each time. The adversary estimates the system states from the output history. We show that, to keep the system differentially private, the output entropy is bounded below, and this lower bound is achieves by an explicit mechanism.},
author = {Wang, Yu and Huang, Zhenqi and Mitra, Sayan and Dullerud, Geir E},
booktitle = {53rd IEEE Conf. Decis. Control},
doi = {10.1109/CDC.2014.7039713},
isbn = {978-1-4673-6090-6},
month = dec,
pages = {2130--2135},
publisher = {IEEE},
title = {Entropy-minimizing mechanism for differential privacy of discrete-time linear feedback systems},
year = {2014}
}
@inproceedings{Peri2016,
author = {Peri, Joseph S. J.},
booktitle = {Signal Process. Sensor/Information Fusion, Target Recognit. XXV},
doi = {10.1117/12.2228471},
editor = {Kadar, Ivan},
isbn = {9781510600836},
issn = {1996756X},
month = may,
pages = {98420W},
title = {Dempster-Shafer information measures in category theory},
volume = {9842},
year = {2016}
}
@article{Kingdom2015,
author = {Bonsangue, Marcello and Hansen, Helle Hvid and Kurz, Alexander and Rot, Jurriaan},
doi = {10.2168/LMCS-11(3:2)2015},
editor = {Milius, Stefan},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {algebraic techniques in automata,and phrases,probabilistic automata,value 1 problem},
month = aug,
number = {3},
pages = {1--50},
title = {Presenting distributive laws},
volume = {11},
year = {2015}
}
@inproceedings{Abel2013a,
address = {New York, New York, USA},
author = {Abel, Andreas M. and Pientka, Brigitte},
booktitle = {Proc. 18th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '13},
doi = {10.1145/2500365.2500591},
isbn = {9781450323260},
keywords = {coinduction,ity,pattern matching,productiv-,recursion,strong normalization,type-based termination},
pages = {185},
publisher = {ACM Press},
title = {Wellfounded recursion with copatterns},
year = {2013}
}
@article{Josang2002,
abstract = {The consensus operator provides a method for combining possibly conflicting beliefs within the Dempster-Shafer belief theory, and represents an alternative to the traditional Dempster's rule. This paper describes how the consensus operator can be applied to dogmatic conflicting opinions, i.e., when the degree of conflict is very high. It overcomes shortcomings of Dempster's rule and other operators that have been proposed for combining possibly conflicting beliefs. {\textcopyright} 2002 Elsevier Science B.V. All rights reserved.},
author = {Josang, Audun},
doi = {10.1016/S0004-3702(02)00259-X},
issn = {00043702},
journal = {Artif. Intell.},
keywords = {Belief,Conflict,Consensus operator,Dempster's rule,Subjective logic},
number = {1-2},
pages = {157--170},
title = {The consensus operator for combining beliefs},
volume = {141},
year = {2002}
}
@article{Ghani2004,
author = {Ghani, Neil and Uustalu, Tarmo},
doi = {10.1051/ita:2004016},
issn = {0988-3754},
journal = {RAIRO - Theor. Informatics Appl.},
month = oct,
number = {4},
pages = {321--342},
title = {Coproducts of Ideal Monads},
volume = {38},
year = {2004}
}
@article{Kupke2008,
abstract = {We generalize some of the central results in automata theory to the abstraction level of coalgebras and thus lay out the foundations of a universal theory of automata operating on infinite objects. Let F be any set functor that preserves weak pullbacks. We show that the class of recognizable languages of F-coalgebras is closed under taking unions, intersections, and projections. We also prove that if a nondeterministic F-automaton accepts some coalgebra it accepts a finite one of the size of the automaton. Our main technical result concerns an explicit construction which transforms a given alternating F-automaton into an equivalent nondeterministic one, whose size is exponentially bound by the size of the original automaton.},
author = {Kupke, Clemens and Venema, Yde},
doi = {10.2168/LMCS-4(4:10)2008},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,automata,coalgebra,fixed-point logics,parity games},
number = {4:10},
pages = {1--43},
title = {Coalgebraic Automata Theory: Basic Results},
volume = {4},
year = {2008}
}
@article{Furber2015,
abstract = {This paper presents a categorical account of conditional probability, covering both the classical and the quantum case. Classical conditional probabilities are expressed as a certain "triangle-fill-in" condition, connecting marginal and joint probabilities, in the Kleisli category of the distribution monad. The conditional probabilities are induced by a map together with a predicate (the condition). The latter is a predicate in the logic of effect modules on this Kleisli category. This same approach can be transferred to the category of C*-algebras (with positive unital maps), whose predicate logic is also expressed in terms of effect modules. Conditional probabilities can again be expressed via a triangle-fill-in property. In the literature, there are several proposals for what quantum conditional probability should be, and also there are extra difficulties not present in the classical case. At this stage, we only describe quantum systems with classical parameterization.},
archivePrefix = {arXiv},
arxivId = {1306.0831},
author = {Furber, Robert and Jacobs, Bart},
doi = {10.4204/EPTCS.195.14},
eprint = {1306.0831},
issn = {20752180},
journal = {Quantum Phys. Log.},
number = {Qpl 2015},
pages = {179--195},
title = {Towards a Categorical Account of Conditional Probability},
year = {2015}
}
@article{Porst2008,
author = {Porst, Hans-E.},
doi = {10.2989/QM.2008.31.2.2.474},
issn = {1607-3606},
journal = {Quaest. Math.},
keywords = {bimonoids,comonoids,free and cofree construc-,monoidally closed categories,monoids,tions},
month = jun,
number = {2},
pages = {127--139},
title = {On Categories of Monoids, Comonoids, and Bimonoids},
volume = {31},
year = {2008}
}
@inproceedings{Turi,
abstract = {We present a categorical theory of `well-behaved' operational semantics which aims at complementing the established theory of domains and denotational semantics to form a coherent whole. It is shown that, if the operational rules of a programming language can be modelled as a natural transformation of a suitable general form, depending on functorial notions of syntax and behaviour, then one gets the following for free: an operational model satisfying the rules and a canonical, internally fully abstract denotational model which satisfies the operational rules. The theory is based on distributive laws and bialgebras; it specialises to the known classes of well-behaved rules for structural operational semantics, such as GSOS.},
author = {Turi, Daniele and Plotkin, Gordon D.},
booktitle = {Proc. Twelfth Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.1997.614955},
isbn = {0-8186-7925-5},
pages = {280--291},
publisher = {IEEE Comput. Soc},
title = {Towards a mathematical operational semantics},
year = {1997}
}
@article{Matthes2007,
author = {Kunc, Michal},
doi = {10.1051/ita:2003018},
issn = {0988-3754},
journal = {RAIRO - Theor. Informatics Appl.},
keywords = {and phrases,implicit operation,languages,pseudoidentity,pseudovariety,syntactic homomorphism,variety of regular},
number = {3},
pages = {243--254},
title = {Equational description of pseudovarieties of homomorphisms},
volume = {37},
year = {2003}
}
@article{Keuchel2013,
abstract = {Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory {\`{a}} la Carte (MTC) framework in the context of programming language meta-theory. However, MTC's use of extensible Church-encodings is unsatisfactory. This paper takes a better approach to the problem with datatype-generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.},
author = {Keuchel, Steven and Schrijvers, Tom},
doi = {10.1145/2502488.2502491},
isbn = {9781450323895},
journal = {Proc. 9th ACM SIGPLAN Work. Generic Program. - WGP '13},
keywords = {Datatype-generic programming,Fixed points,Mechanized meta-theory,Modularity},
pages = {13},
title = {Generic datatypes {\`{a}} la carte},
year = {2013}
}
@article{Lambek1970,
author = {Lambek, Joachim},
doi = {http://10.4153/CMB-1970-065-6},
journal = {Can. Math. Bull.},
number = {3},
pages = {337--349},
title = {Subequalizers},
volume = {13},
year = {1970}
}
@article{Halmos1981,
author = {Halmos, Paul R.},
journal = {Math. Tomorrow},
pages = {9--20},
title = {Applied Mathematics is Bad Mathematics},
year = {1981}
}
@book{Bishop2003,
author = {Bishop, Matt},
isbn = {0-201-44099-7},
pages = {1136},
publisher = {Addison Wesley Professional},
title = {Computer Security: Art and Science},
year = {2003}
}
@article{Szawiel2012,
abstract = {We characterize the equational theories and Lawvere theories that correspond to the categories of analytic and polynomial monads on Set, and hence also the categories of the symmetric and rigid operads in Set. We show that the category of analytic monads is equivalent to the category of regular-linear theories. The category of polynomial monads is equivalent to the category of rigid theories, i.e. regular-linear theories satisfying an additional global condition. This solves a problem A. Carboni and P. T. Johnstone. The Lawvere theories corresponding to these monads are identified via some factorization systems.},
archivePrefix = {arXiv},
arxivId = {1204.2703},
author = {Szawiel, Stanislaw and Zawadowski, Marek},
eprint = {1204.2703},
journal = {ArXiv e-prints},
keywords = {distributive law,equational theory,factor-,interpretation,ization system,lawvere theory,monad,operad},
month = apr,
pages = {29},
title = {Theories of analytic monads},
year = {2012}
}
@phdthesis{Fontaine2010,
author = {Fontaine, Ga{\"{e}}lle M.M.},
isbn = {9789057762154},
pages = {246},
publisher = {Institute for Logic, Language and Computation},
title = {Modal fixpoint logic: some model theoretic questions},
year = {2010}
}
@inproceedings{Coecke2010,
author = {Coecke, Bob and Lal, Raymond},
booktitle = {Proc. 7th Int. QPL Work. Quantum Phys. Log.},
pages = {17----26},
title = {Causal categories: a backbone for a quantum-relativistic universe of interacting processes},
year = {2010}
}
@article{Moss1999,
author = {Moss, Lawrence S.},
doi = {10.1016/S0168-0072(98)00042-6},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
number = {1-3},
pages = {277--317},
title = {Coalgebraic logic},
type = {Journal article},
volume = {96},
year = {1999}
}
@article{Mich2005,
abstract = {A fully abstract and universal domain model for modal transition systems and refinement is shown to be a maximal-points space model for the bisimulation quotient of labelled transition systems over a finite set of events. In this domain model we prove that this quotient is a Stone space whose compact, zero-dimensional, and ultra-metrizable Hausdorff topology measures the degree of bisimilarity such that image-finite labelled transition systems are dense. Using this compactness we show that the set of labelled transition systems that refine a modal transition system, its ''set of implementations'', is compact and derive a compactness theorem for Hennessy-Milner logic on such implementation sets. These results extend to systems that also have partially specified state propositions, unify existing denotational, operational, and metric semantics on partial processes, render robust consistency measures for modal transition systems, and yield an abstract interpretation of compact sets of labelled transition systems as Scott-closed sets of modal transition systems.},
author = {Huth, Michael},
doi = {10.2168/LMCS-1(1:1)2005},
editor = {Escard{\'{o}}, Mart{\'{i}}n},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
language = {en},
month = jan,
number = {1},
publisher = {Institut f{\"{u}}r Theoretische Informatik, TU Braunschweig / Department of Theoretical Computer Science, Technical University Braunschweig, Germany},
title = {Labelled transition systems as a Stone space},
volume = {1},
year = {2005}
}
@article{Sarathy2011,
abstract = {Laplace noise addition is often advanced as an approach for satisfying differ-ential privacy. There have been several illustrations of the application of Laplace noise addition for count data, but no evaluation of its performance for numeric data. In this study we evaluate the privacy and utility performance of Laplace noise addition for numeric data. Our results indicate that Laplace noise addition delivers the promised level of privacy only by adding a large quantity of noise for even relatively large sub-sets. Because of this, even for simple mean queries, the responses for a masking mecha-nism that uses Laplace noise addition is of little value. We also show that Laplace noise addition may be vulnerable to a tracker attack. In order to avoid this, it may be neces-sary to increase the variance of the noise added as a function of the number of queries issued. This implies that the utility of the responses would be further reduced. These results raise serious questions regarding the viability of Laplace based noise addition for masking numeric data.},
author = {Sarathy, Rathindra and Muralidhar, Krishnamurty},
isbn = {1888-5063},
issn = {18885063},
journal = {Trans. Data Priv.},
number = {1},
pages = {1--17},
title = {Evaluating laplace noise addition to satisfy differential privacy for numeric data},
volume = {4},
year = {2011}
}
@inproceedings{Schroder2010,
author = {Schr{\"{o}}der, Lutz and Pattinson, Dirk},
booktitle = {Proc. Found. Softw. Sci. Comput. Struct.},
pages = {328--342},
publisher = {Springer},
title = {Coalgebraic correspondence theory},
year = {2010}
}
@article{Pattinson2003,
abstract = {This paper studies finitary modal logics, interpreted over coalgebras for an endofunctor, and establishes soundness, completeness and decidability results. The logics are studied within the abstract framework of coalgebraic modal logic, which can be instantiated with arbitrary endofunctors on the category of sets. This is achieved through the use of predicate liftings, which generalise atomic propositions and modal operators from Kripke models to arbitrary coalgebras. Predicate liftings also allow us to use induction along the terminal sequence of the underlying endofunctor as a proof principle. This induction principle is systematically exploited to establish soundness, completeness and decidability of the logics. We believe that this induction principle also opens new ways for reasoning about modal logics: Our proof of completeness does not rely on a canonical model construction, and the proof of the finite model property does not use filtrations.},
author = {Pattinson, Dirk},
doi = {10.1016/S0304-3975(03)00201-9},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = dec,
number = {1-3},
pages = {177--193},
title = {Coalgebraic modal logic: soundness, completeness and decidability of local consequence},
volume = {309},
year = {2003}
}
@article{Fric2010,
abstract = {First, we discuss basic probability notions from the viewpoint of category theory. Our approach is based on the following four “sine quibus non” conditions: 1. (elementary) category theory is efficient (and suffices); 2. random variables, observables, probability measures, and states are morphisms; 3. classical probability theory and fuzzy probability theory in the sense of S. Gudder and S. Bugajski are special cases of a more general model; 4. a good model allows natural modifications. Second, we show that the category ID of D-posets of fuzzy sets and sequentially continuous D-homomorphisms allows to characterize the passage from classical to fuzzy events as the minimal generalization having nontrivial quantum character: a degenerated state can be transported to a nondegenerated one. Third, we describe a general model of probability theory based on the category ID so that the classical and fuzzy probability theories become special cases and the model allows natural modifications. Finally, we present a modification in which the closed unit interval [0,1] as the domain of traditional states is replaced by a suitable simplex.},
author = {Fri{\v{c}}, Roman and Pap{\v{c}}o, Martin},
doi = {10.1007/s11225-010-9232-z},
issn = {0039-3215},
journal = {Stud. Log.},
month = feb,
number = {2},
pages = {215--230},
publisher = {Springer Netherlands},
title = {A Categorical Approach to Probability Theory},
volume = {94},
year = {2010}
}
@article{Johnstone1975,
author = {Johnstone, Peter T.},
doi = {10.1112/blms/7.3.294},
issn = {0024-6093},
journal = {Bull. London Math. Soc.},
month = nov,
number = {3},
pages = {294--297},
title = {Adjoint lifting theorems for categories of algebras},
volume = {7},
year = {1975}
}
@article{Sipos2015,
archivePrefix = {arXiv},
arxivId = {1409.1370},
author = {Sipos, Andrei},
eprint = {1409.1370},
journal = {ArXiv e-prints},
keywords = {codensity,frame,monad,sober space,stone space,ultrafilter},
pages = {1--18},
title = {Codensity and Stone spaces},
year = {2015}
}
@article{Kock1970a,
author = {Kock, Anders},
issn = {0025-5521},
journal = {Math. Scand.},
pages = {151--165},
title = {On double dualization monads},
volume = {27},
year = {1970}
}
@article{Pouly2013,
abstract = {This paper develops a new uncertainty measure for the theory of hints that complies with the established semantics of statistical information theory and further satisfies all classical requirements for such a measure imposed in the literature. The proposed functional decomposes into conversant uncertainty measures and therefore discloses a new interpretation of the latters as well. By abstracting to equivalence classes of hints we transport the new measure to mass functions in Dempster-Shafer theory and analyse its relationship with the aggregate uncertainty, which currently is the only known functional for the Dempster-Shafer theory of evidence that satisfies the same set of properties. Moreover, the perspective of hints reveals that the standard independence notion in Dempster-Shafer theory called non-interactivity corresponds to an amalgamation of probabilistic independence and qualitative independence between frames of discernment. All results in this paper are developed for arbitrary families of compatible frames generalizing the very specialized multi-variate systems that are usually studied in information theory. {\textcopyright} 2012 Elsevier Inc. All rights reserved.},
author = {Pouly, Marc and Kohlas, Juerg and Ryan, Peter Y A},
doi = {10.1016/j.ijar.2012.08.004},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Dempster-Shafer theory,Information theory,Theory of Hints},
month = jan,
number = {1},
pages = {228--251},
publisher = {Elsevier Inc.},
title = {Generalized information theory for hints},
volume = {54},
year = {2013}
}
@inproceedings{Colcombet2009,
author = {Colcombet, Thomas},
booktitle = {Proc. 36th Int. Collogquium Autom. Lang. Program. Part II},
doi = {10.1007/978-3-642-02930-1_12},
isbn = {3642029299},
issn = {03029743},
pages = {139--150},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {The theory of stabilisation monoids and regular cost functions},
volume = {5556},
year = {2009}
}
@incollection{Bradfield2005,
author = {Bradfield, Julian and Stirling, Colin},
booktitle = {Handb. Modal Log.},
doi = {10.1016/S1570-2464(07)80015-2},
editor = {Blackburn, Patrick and van Benthem, Johan and Wolter, Frank},
pages = {721--756},
publisher = {Elsevier B.V.},
series = {Studies in Logic and Practical Reasoning},
title = {Modal mu-calculi},
volume = {3},
year = {2007}
}
@book{Nachbin1965a,
author = {Nachbin, Leopoldo},
isbn = {978-0882753874},
publisher = {Van Nostrand, Princeton, N.J.},
series = {Van Nostrand Mathematical Studies},
title = {Topology and order},
type = {Book},
volume = {296},
year = {1965}
}
@inproceedings{Peri2015,
author = {Peri, Joseph S. J.},
booktitle = {Signal Process. Sensor/Information Fusion, Target Recognit. XXIV},
doi = {10.1117/12.2177200},
editor = {Kadar, Ivan},
month = may,
pages = {94740V},
title = {Categorification of the Dempster Shafer theory},
volume = {9474},
year = {2015}
}
@article{Adamek2003a,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Lawvere, F. William and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1007/s000120300002},
issn = {0002-5240},
journal = {Algebr. Universalis},
month = apr,
number = {1},
pages = {35--49},
title = {On the duality between varieties and algebraic theories},
volume = {49},
year = {2003}
}
@article{Gabbay2012,
author = {Gabbay, Murdoch J. and Ghica, Dan},
doi = {10.1016/j.entcs.2012.08.012},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {equivariance,game semantics,nominal abstraction and coabstraction,nominal sets},
month = sep,
pages = {173--189},
title = {Game semantics in the nominal model},
volume = {286},
year = {2012}
}
@article{Goncharov2016,
abstract = {Monads are extensively used nowadays to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. It turns out that equipping a monad with a (uniform) iteration operator satisfying a set of natural axioms allows for modelling iterative computations just as abstractly. The emerging monads are called complete Elgot monads. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of the relationship between abstract complete Elgot monads and those that capture coalgebraic resumptions, by comparing the corresponding categories of (Eilenberg-Moore) algebras. To this end we first provide a characterization of the latter category; even more generally, we formulate this characterization in terms of Uustalu's parametrized monads. This is further used for establishing a characterization of complete Elgot monads as precisely those monads whose algebras are coherently equipped with the structure of algebras of coalgebraic resumption monads.},
archivePrefix = {arXiv},
arxivId = {1603.02148},
author = {Goncharov, Sergey and Milius, Stefan and Rauch, Christoph},
eprint = {1603.02148},
journal = {ArXiv e-prints},
keywords = {Elgot Monads},
month = mar,
title = {Complete Elgot Monads and Coalgebraic Resumptions},
year = {2016}
}
@article{Gudder2006,
author = {Gudder, Stanley},
journal = {Math. Slovaca},
number = {5},
pages = {573----589},
publisher = {Mathematical Institute of the Slovak Academy of Sciences},
title = {An order for quantum observables},
volume = {56},
year = {2006}
}
@article{Ambler1995,
author = {Ambler, Simon},
doi = {10.1016/0304-3975(95)00045-X},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = nov,
number = {1},
pages = {3--27},
title = {Duality and the completeness of the modal $\mu$-calculus},
type = {Journal article},
volume = {151},
year = {1995}
}
@incollection{Plotkin2001,
abstract = {Moggi proposed a monadic account of computational effects. He also presented the computational $\lambda$-calculus, $\lambda$ c , a core call-by-value functional programming language for effects; the effects are obtained by adding appropriate operations. The question arises as to whether one can give a corresponding treatment of operational semantics. We do this in the case of algebraic effects where the operations are given by a single-sorted algebraic signature, and their semantics is supported by the monad, in a certain sense. We consider call-by-value PCF with— and without—recursion, an extension of $\lambda$ c with arithmetic. We prove general adequacy theorems, and illustrate these with two examples: non-determinism and probabilistic nondeterminism.},
author = {Plotkin, Gordon D. and Power, A. John},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/3-540-45315-6_1},
editor = {Honsell, Furio and Miculan, Marino},
pages = {1--24},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Adequacy for Algebraic Effects},
year = {2001}
}
@inproceedings{Anderson2014,
address = {New York, New York, USA},
author = {Anderson, Carolyn Jane and Foster, Nate and Guha, Arjun and Jeannin, Jean-Baptiste and Kozen, Dexter and Schlesinger, Cole and Walker, David},
booktitle = {Proc. 41st ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. - POPL '14},
doi = {10.1145/2535838.2535862},
isbn = {9781450325448},
keywords = {domain-specific languages,frenetic,gramming languages,kleene algebra,network pro-,software-defined networking},
pages = {113--126},
publisher = {ACM Press},
title = {NetKAT: Semantics foundations for networks},
year = {2014}
}
@article{Lescanne2012,
author = {Lescanne, Pierre and Perrinel, Matthieu},
doi = {10.1007/s00236-012-0153-3},
issn = {0001-5903},
journal = {Acta Inform.},
month = mar,
title = {“Backward” coinduction, Nash equilibrium and the rationality of escalation},
year = {2012}
}
@techreport{Abramsky2009,
abstract = {We revisit our earlier work on the representation of quantum systems as Chu spaces, and investigate the use of coalgebra as an alternative framework. On the one hand, coalgebras allow the dynamics of repeated measurement to be captured, and provide mathematical tools such as final coalgebras, bisimulation and coalgebraic logic. However, the standard coalgebraic framework does not accommodate contravariance, and is too rigid to allow physical symmetries to be represented. We introduce a fibrational structure on coalgebras in which contravariance is represented by indexing. We use this structure to give a universal semantics for quantum systems based on a final coalgebra construction. We characterize equality in this semantics as projective equivalence. We also define an analogous indexed structure for Chu spaces, and use this to obtain a novel categorical description of the category of Chu spaces. We use the indexed structures of Chu spaces and coalgebras over a common base to define a truncation functor from coalgebras to Chu spaces. This truncation functor is used to lift the full and faithful representation of the groupoid of physical symmetries on Hilbert spaces into Chu spaces, obtained in our previous work, to the coalgebraic semantics.},
author = {Abramsky, Samson},
institution = {OUCL},
month = oct,
number = {RR-09-11},
pages = {26},
title = {Coalgebras, Chu spaces, and representations of physical Systems},
year = {2009}
}
@article{Knuth2005,
author = {Knuth, Kevin H.},
doi = {10.1016/j.neucom.2004.11.039},
issn = {09252312},
journal = {Neurocomputing},
keywords = {bayesian inference,entropy,information theory,inquiry,lattice,probability},
month = aug,
pages = {245--274},
title = {Lattice duality: The origin of probability and entropy},
volume = {67},
year = {2005}
}
@incollection{Street1996,
abstract = {This chapter discusses category theory, with emphasis on categorical structures. Innovative categorical concepts in category theory include homological algebra, universal algebra, set theory, and enumerative combinatorics. The chapter emphasizes categories as vital mathematical structures. It also explores some fundamental interconnections involving rewrite systems, free higher-order categories, cubes and simplexes, and homotopy theory. A (directed) graph G consists of two sets G0, G1 and an ordered pair of functions. The elements of G0 are called “objects,” “vertices,” or “0-cells.” The elements of G1 are called “arrows,” “edges,” or “1-cells.” Repeated horizontal and vertical composition in a 2-category K determines a more general operation called “pasting.” Each free 2-category A has a length 2-functor ℓ: A →M induced by the unique computed morphism between the generating computads. The connection between categories and the Bazhanov–Stroganov d-simplex equations arisen in statistical and quantum mechanics are also presented.},
author = {Street, Ross},
booktitle = {Handb. Algebr.},
doi = {10.1016/S1570-7954(96)80019-2},
editor = {Hazewinkel, M.},
isbn = {978-0-444-82212-3},
issn = {15707954},
pages = {529--577},
publisher = {North-Holland},
title = {Categorical structures},
volume = {1},
year = {1996}
}
@inproceedings{Kupke2004a,
author = {Kupke, Clemens and Kurz, Alexander and Pattinson, Dirk},
booktitle = {Electron. Notes Theor. Comput. Sci.},
doi = {10.1016/j.entcs.2004.02.037},
issn = {15710661},
month = dec,
pages = {219--241},
title = {Algebraic Semantics for Coalgebraic Logics},
type = {Journal article},
volume = {106},
year = {2004}
}
@book{Dalen2004,
address = {Berlin, Heidelberg},
author = {van Dalen, Dirk},
doi = {10.1007/978-3-540-85108-0},
isbn = {978-3-540-20879-2},
publisher = {Springer Berlin Heidelberg},
series = {Universitext},
title = {Logic and Structure},
year = {2004}
}
@book{Hoare1985,
author = {Hoare, C.A.R.},
isbn = {0-13-153271-5},
keywords = {and phrases,concurrency,guarded commands,input,nondeterminacy,output,parallel programming,program structures,programming,programming languages,programming primitives},
pages = {256},
publisher = {Prentice Hall},
series = {Prentice Hall International Series in Computing Science},
title = {Communicating Sequential Processes},
year = {1985}
}
@article{Mulry1994,
abstract = {In this paper we consider two conceptually different categorical approaches to partiality namely partial map classifiers (pmcs) with total maps, and partial cartesian closed categories (pcccs) pC with partial maps, showing how these approaches are intimately related. While a topos setting generally provides a richer setting for defining possible pmcs and classes of partial maps, conditions are derived that determine when pmcs and partial maps can in fact restrict to pC. In this way semantic constructs can be interpreted consistently from both approaches. Various examples involving domains and cpos are examined as is the connection to Kleisli categories. Finally, it is observed that a general categorical framework involving monads arises naturally in this context. ?? 1994.},
author = {Mulry, Philip S.},
doi = {10.1016/0304-3975(94)00124-2},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = dec,
number = {1},
pages = {109--123},
title = {Partial map classifiers and partial cartesian closed categories},
volume = {136},
year = {1994}
}
@article{Company1931,
author = {Arbib, Michael A. and Manes, Ernest G.},
doi = {10.1016/0022-4049(80)90090-0},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = dec,
pages = {9--20},
title = {Machines in a category},
volume = {19},
year = {1980}
}
@inproceedings{McSherry2007,
abstract = {We study the role that privacy-preserving algorithms, which\nprevent the leakage of specific information about participants, can play in\nthe design of mechanisms for strategic agents, which must encourage players\nto honestly report information. Specifically, we show that the recent notion\nof differential privacv, in addition to its own intrinsic virtue, can ensure\nthat participants have limited effect on the outcome of the mechanism, and as\na consequence have limited incentive to lie. More precisely, mechanisms with\ndifferential privacy are approximate dominant strategy under arbitrary player\nutility functions, are automatically resilient to coalitions, and easily\nallow repeatability. We study several special cases of the unlimited supply\nauction problem, providing new results for digital goods auctions, attribute\nauctions, and auctions with arbitrary structural constraints on the prices.\nAs an important prelude to developing a privacy-preserving auction mechanism,\nwe introduce and study a generalization of previous privacy work that\naccommodates the high sensitivity of the auction setting, where a single\nparticipant may dramatically alter the optimal fixed price, and a slight\nchange in the offered price may take the revenue from optimal to zero.},
author = {McSherry, Frank and Talwar, Kunal},
booktitle = {48th Annu. IEEE Symp. Found. Comput. Sci.},
doi = {10.1109/FOCS.2007.66},
isbn = {0-7695-3010-9},
issn = {0272-5428},
month = oct,
pages = {94--103},
publisher = {IEEE},
title = {Mechanism Design via Differential Privacy},
year = {2007}
}
@inproceedings{Santocanale2010,
author = {Santocanale, Luigi and Venema, Yde},
booktitle = {Adv. Modal Log.},
editor = {And, Lev D. Beklemishev and Goranko, Valentin and Shehtman, Valentin},
isbn = {978-1-84890-013-4},
keywords = {coalgebra,monotone modal logic,neighborhood semantics,uniform interpolation},
pages = {350--370},
publisher = {College Publications},
title = {Uniform Interpolation for Monotone Modal Logic},
year = {2010}
}
@article{Aizpuru2006,
abstract = {In this paper we study how some classic properties in measure theory, valid on Boolean algebras, still hold in quantum logic, mainly, on quantum logic of sets. We obtain some results about the Vitali-Hahn-Saks property and the Nikodym property for sequences of real valued, $\sigma$-additive measures. {\textcopyright} 2006 Elsevier B.V. All rights reserved.},
author = {Aizpuru, A. and Tamayo, M.},
doi = {10.1016/j.fss.2006.03.010},
issn = {01650114},
journal = {Fuzzy Sets Syst.},
keywords = {Effect algebras,Measure},
month = aug,
number = {15},
pages = {2139--2143},
title = {Classical properties of measure theory on effect algebras},
volume = {157},
year = {2006}
}
@inproceedings{Adamek2014c,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Myers, Robert Samuel Ralph and Urbat, Henning},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-54830-7_24},
editor = {Muscholl, Anca},
pages = {366--380},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Generalized Eilenberg theorem I : Local varieties of languages},
year = {2014}
}
@article{Hofmann2012a,
abstract = {We combine two research directions of the past decade, namely the development of a lax-algebraic framework for categories of interest to topologists and analysts, and the exploration of key topological concepts, like separation and compactness, in an abstract category which comes equipped with an axiomatic notion of "closed" or "proper" map. Hence, we present various candidates for such notions in the context of the category of (T,V)-categories, with a Set-monad T=(T,e,m) laxly extended to the category of sets and V-valued relations, for a quantale V. Suitable categories of ordered sets, metric spaces, topological spaces, closure spaces, and approach spaces all fit into this framework and allow for applications of the the general theory. {\textcopyright} 2012 Elsevier B.V.},
author = {Hofmann, Dirk and Tholen, Walter},
doi = {10.1016/j.topol.2011.09.049},
issn = {01668641},
journal = {Topol. Appl.},
keywords = {Compact object,Lax algebra,Lax extension,Monad,Perfect morphism,Separated object},
month = jun,
number = {9},
pages = {2434--2452},
publisher = {Elsevier B.V.},
title = {Lax algebra meets topology},
volume = {159},
year = {2012}
}
@book{Halpern2003,
author = {Halpern, Joseph Y.},
edition = {1},
pages = {497},
publisher = {The MIT Press},
series = {Computer Science and Intelligent Systems},
title = {Reasoning about Uncertainty},
year = {2003}
}
@article{Makkai1996,
abstract = {The notion of anafunctor is introduced. An anafunctor is, roughly, a "functor defined up to isomorphism". Anafunctors have a general theory paralleling that of ordinary functors; they have natural transformations, they form categories, they can be composed, etc. Anafunctors can be saturated, to ensure that any object isomorphic to a possible value of the anafunctor is also a possible value at the same argument object. The existence of anafunctors in situations when ordinarily one would use choice is ensured without choice; e.g., for a category which has binary products, but not specified binary products, the anaversion of the product functor is canonically definable, unlike the ordinary product functor that needs the axiom of choice. When the composition functors in a bicategory are changed into anafunctors, one obtains anabicategories. In the standard definitions of bicategories such as the monoidal category of modules over a ring, or the bicategory of spans in a category with pullbacks, and many others, one uses choice; the anaversions of these bicategories have canonical definitions. The overall effect is an elimination of the axiom of choice, and of non-canonical choices, in large parts of general category theory. To ensure the Cartesian closed character of the bicategory of small categories, with anafunctors as 1-cells, one uses a weak version of the axiom of choice, which is related to A. Blass' axiom of Small Violations of Choice (1979).},
author = {Makkai, Michael},
doi = {10.1016/0022-4049(95)00029-1},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
number = {95},
pages = {109--173},
title = {Avoiding the axiom of choice in general category theory},
volume = {108},
year = {1996}
}
@book{Klir2006,
address = {Hoboken, NJ, USA},
author = {Klir, George J},
doi = {10.1002/0471755575},
isbn = {9780471755579},
month = nov,
pages = {511},
publisher = {John Wiley & Sons, Inc.},
title = {Uncertainty and Information},
year = {2005}
}
@incollection{Cleaveland1993,
address = {Berlin},
author = {Cleaveland, Ranee and Klein, Marion and Steffen, Bernhard},
booktitle = {Comput. Aided Verif. CAV 1992},
doi = {10.1007/3-540-56496-9_32},
editor = {von Bochmann, G. and Probst, D.K.},
pages = {410--422},
publisher = {Springer},
title = {Faster model checking for the modal Mu-Calculus},
year = {1993}
}
@incollection{Butler2017,
abstract = {Inspired by a number of different applications of rewriting logic, equational logic, and type theory that we present and further advance in this thesis, we study a unified formalism based on the key aspects of these quite different lines of research. The resulting formalism, that we call the open calculus of constructions, is intended as a step towards our long-term goal of developing a unified language for programming, specification and interactive theorem proving. \nWe begin our work by exploring the application of rewriting logic as a semantic framework for concurrency. To this end, we give a unified treatment of different classes of Petri nets, a typical and important representative of a class of formalisms that are used for the modeling and specification of concurrent and distributed systems based on a multiset representation of a distributed state space. Specifically, we continue the line of research initiated by Meseguer and Montanari under the motto "Petri nets are monoids" by giving a rewriting semantics for different Petri nets classes. In particular, we have covered important high-level Petri net models, namely algebraic net specifications and colored Petri nets, and we have proved that the models of our representations are naturally isomorphic to the well-known Best-Devillers process semantics. Apart from their contribution to a conceptual unification in this field, the main practical advantage of our representations in rewriting logic is their executability, which allows us to use a rewriting engine such as Maude for the efficient symbolic execution of system models and for their analysis. \nThe next application addressed in this thesis is the use of type theory, more precisely the calculus of inductive constructions, as a logical framework and for metalogical reasoning. Specifically, we have used the COQ proof assistant in a formally rigorous development of a UNITY-style temporal logic, which generalizes the original UNITY approach in important aspects. Since all inference rules of the temporal logic are proved as theorems in the metalogic, the result of the development is a verified temporal logic library, which due to the use of labeled transition systems as a semantic basis, can be employed for a wide range of system models, Petri nets and rewriting logic specifications being particular examples. The development also includes a new application of the proposition-as-types interpretation in the context of compositional reasoning. \nThe use of membership equational logic or rewriting logic as a semantic and logical framework for higher-order languages, or more generally languages with binding constructs, obviously requires a first-order treatment of names and relevant operations such as substitutions. To systematically address such applications, we develop CINNI, a new calculus of names and substitutions, that takes names seriously in the sense that it does not abstract from names, and is generic in the sense that it can be instantiated to arbitrary object languages. Our calculus unifies the standard named notation and a notation based on de Bruijn indices by employing a representation that was originally developed by Berkling for the lambda-calculus. It furthermore nicely generalizes the calculus lambda upsilon of explicit substitutions developed by Lescanne, and, as we show, most metatheoretic results can be generalized to the new calculus. We furthermore give a very general confluence result for the composition of CINNI with the equations or rules capturing the dynamics of the object language, and we in particular discuss how our approach can be applied to the representation of the untyped lambda-calculus, Abadi and Cardelli's object calculus, also called the sigma-calculus, and Milner's pi-calculus for communicating and mobile systems. As a real-world application of CINNI we briefly discuss a specification of an active network programming language in the rewriting-logic-based language Maude. \nWe more specifically address the use of membership equational logic and rewriting logic as a first-order logical framework by representing an important class of pure type systems. Pure type systems generalize a variety of different type theories, including the calculus of constructions and its well-known subsystems, and can be seen as higher-order logics via the propositions-as-types interpretation. Following a methodology based on Meseguer's general logics in combination with rewriting logic as a concrete logical framework, we have studied representations of pure type systems at different levels of abstractions, ranging from an abstract textbook representation to a more concrete executable representation of an important subclass, which can directly serve as a type inference and type checking algorithm. The latter representation is based on a new notion of uniform pure type systems, which take names seriously thanks to the CINNI calculus and simultaneously offer a possible solution to the known problem with alpha-closure pointed out by Pollack. Using an example, in which we validate proofs developed with the LEGO proof assistant in an extension of the calculus of constructions with universes, we have demonstrated how our approach directly leads to an executable prototype in a rewriting logic language such as Maude. \nAs an application of type theory in the context of classical reasoning we study Howe's HOL/Nuprl connection, which addresses the problem of formal interoperability between proof assistents, from the viewpoint of Meseguer's general logics. We supplement Howe's semantic justification by a proof-theoretic correctness argument, a piece of work which has lead to proof-translation as new interesting application (explored in joint work with Naumov) that goes beyond Howe's original HOL/Nuprl connection. From a theoretical perspective we found that the core idea of the HOL/Nuprl connection, namely the beneficial coexistence of an intensional and an extensional logic in the same formal system, does not rely on any of the advanced concepts of Nuprl, but can equally well be used in Martin-L{\"{o}}f's type theory and can further be easily adopted to type theories in the line of calculus of constructions. \nThe final and main contribution of this thesis is the development of a formalism that we call the open calculus of constructions (OCC). It is based on the surprisingly powerful interaction between its two key features, namely dependent types, in the spirit of Martin-L{\"{o}}f's type theory and the calculus of constructions, and the computational system of rewriting logic and its underlying membership equational logic, which is based on conditional rewriting modulo equations. The applications of membership equational logic, rewriting logic, and type theory, studied in this thesis have not only inspired the development of this unifying formalism, but they become applications of OCC itself and benefit from its use in an essential way. On the theoretical side, we introduce OCC by presenting a classical set-theoretic semantics and a formal system for which we prove soundness and consistency as a logic. The formal system is used to define derivable judgements together with their operational semantics, and is based on the ideas that we developed earlier in the context of uniform pure type systems. The model-theoretic semantics that we develop in this thesis is a very intuitive semantics with proof-irrelevance for impredicative universes, but unlike existing approaches it is more direct and can be given independently of the formal system. Using an experimental prototype of OCC, that we implemented in Maude following the approach to the specification of type theories mentioned before in combination with reflective techniques, we have developed a large collection of examples, many of which are closely related to the applications discussed earlier in this thesis. These examples do not only convey the pragmatics of OCC, but they simultaneously provide a proof-of-concept for our approach. Among the topics covered by our examples we find executable equational/behavioral specifications, programming with dependent types, symbolic execution of system models, formalization of algebraic and categorical concepts, inductive/coinductive theorem proving, and theorem proving modulo equational theories.},
author = {Butler, David and Aspinall, David and Gasc{\'{o}}n, Adri{\`{a}}},
booktitle = {Interact. Theorem Proving. ITP 2017},
doi = {10.1007/978-3-319-66107-0_8},
editor = {Ayala-Rinc{\'{o}}n, Mauricio and Mu{\~{n}}oz, C{\'{e}}sar A.},
isbn = {978-3-642-14051-8},
keywords = {formal verification,oblivious transfer,proof},
pages = {114--130},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {How to Simulate It in Isabelle: Towards Formal Proof for Secure Multi-Party Computation},
volume = {10499},
year = {2017}
}
@article{Vietoris1922a,
author = {Vietoris, Leopold},
doi = {10.1007/BF01696886},
issn = {0026-9255},
journal = {Monatshefte f{\"{u}}r Math. und

repository: anqurvanillapy/Type-Theory

repo_name: anqurvanillapy/Type-Theory