text:
by many examples. Entropy on MV-algebras is postponed to Part II.},
author = {{Di Nola}, Antonio and Dvure{\v{c}}enskij, Anatolij and Hy{\v{c}}ko, Marek and Manara, Corrado},
journal = {Kybernetika},
number = {2},
pages = {143--160},
title = {Entropy on effect algebras with the Riesz decomposition property I: Basic properties},
volume = {41},
year = {2005}
}
@article{Kifer2014,
abstract = {In this article, we introduce a new and general privacy framework called Pufferfish. The Pufferfish framework can be used to create new privacy definitions that are customized to the needs of a given application. The goal of Pufferfish is to allow experts in an application domain, who frequently do not have expertise in privacy, to develop rigorous privacy definitions for their data sharing needs. In addition to this, the Pufferfish framework can also be used to study existing privacy definitions. We illustrate the benefits with several applications of this privacy framework: we use it to analyze differ- ential privacy and formalize a connection to attackers who believe that the data records are independent; we use it to create a privacy definition called hedging privacy, which can be used to rule out attackers whose prior beliefs are inconsistent with the data; we use the framework to define and study the notion of composi- tion in a broader context than before; we show how to apply the framework to protect unbounded continuous attributes and aggregate information; and we show how to use the framework to rigorously account for prior data releases.},
author = {Kifer, Daniel and Machanavajjhala, Ashwin},
doi = {10.1145/2514689},
issn = {03625915},
journal = {ACM Trans. Database Syst.},
month = jan,
number = {1},
pages = {1--36},
title = {Pufferfish: A Framework for Mathematical Privacy Definitions},
volume = {39},
year = {2014}
}
@incollection{Chen2008,
address = {Berlin, Heidelberg},
author = {Chen, Qingfeng and Zhang, Chengqi and Zhang, Shichao},
booktitle = {Secur. Trans. Protoc. Anal.},
doi = {10.1007/978-3-540-85074-8_2},
pages = {17--72},
publisher = {Springer Berlin Heidelberg},
title = {Overview of security protocol analysis},
year = {2008}
}
@article{Sweeney1997,
author = {Sweeney, Latanya},
doi = {10.1111/j.1748-720X.1997.tb01885.x},
issn = {1073-1105},
journal = {J. Law, Med. \& Ethics},
keywords = {necting research},
month = jun,
number = {2-3},
pages = {98--110},
title = {Weaving Technology and Policy Together to Maintain Confidentiality},
volume = {25},
year = {1997}
}
@article{TenCate2009,
author = {ten Cate, Balder and Gabelaia, David and Sustretov, Dmitry},
doi = {10.1016/j.apal.2008.11.001},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {03b48,03c40,1991 msc,54a05,definability,expressivity,modal logic,topology},
month = may,
number = {1-2},
pages = {146--170},
title = {Modal languages for topology: Expressivity and definability},
volume = {159},
year = {2009}
}
@incollection{Gupta2007,
author = {Gupta, Gopal and Bansal, Ajay and Min, Richard and Simon, Luke and Mallya, Ajay},
booktitle = {Proc. 23rd Int. Conf. Log. Program.},
doi = {10.1007/978-3-540-74610-2_4},
editor = {Dahl, V{\'{e}}ronica and Niemel{\"{a}}, Ilkka},
issn = {0302-9743},
number = {ii},
pages = {27--44},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Coinductive Logic Programming and Its Applications},
year = {2007}
}
@article{Wang2016,
abstract = {This paper investigates the relation between three different notions of privacy: identifiability, differential privacy and mutual-information privacy. Under a unified privacy-distortion framework, where the distortion is defined to be the Hamming distance of the input and output databases, we establish some fundamental connections between these three privacy notions. Given a distortion level $D$, define $\epsilon_{\mathrm{i}}^*(D)$ to be the smallest (best) identifiability level, and $\epsilon_{\mathrm{d}}^*(D)$ to be the smallest differential privacy level. We characterize $\epsilon_{\mathrm{i}}^*(D)$ and $\epsilon_{\mathrm{d}}^*(D)$, and prove that $\epsilon_{\mathrm{i}}^*(D)-\epsilon_X\le\epsilon_{\mathrm{d}}^*(D)\le\epsilon_{\mathrm{i}}^*(D)$ for $D$ in some range, where $\epsilon_X$ is a constant depending on the distribution of the original database $X$, and diminishes to zero when the distribution of $X$ is uniform. Furthermore, we show that identifiability and mutual-information privacy are consistent in the sense that given distortion level $D$, the mechanism that optimizes the mutual-information privacy also minimizes the identifiability level.},
archivePrefix = {arXiv},
arxivId = {1402.3757},
author = {Wang, Weina and Ying, Lei and Zhang, Junshan},
doi = {10.1109/TIT.2016.2584610},
eprint = {1402.3757},
isbn = {9781479980093},
issn = {00189448},
journal = {IEEE Trans. Inf. Theory},
keywords = {Differential privacy,Hamming distance,identifiability,mutual information,rate-distortion},
number = {9},
pages = {5018--5029},
title = {On the relation between identifiability, differential privacy, and mutual-information privacy},
volume = {62},
year = {2016}
}
@book{Lurie2009,
archivePrefix = {arXiv},
arxivId = {arXiv:math/0608040v4},
author = {Lurie, Jacob},
eprint = {0608040v4},
isbn = {978-0691140490},
month = jul,
primaryClass = {arXiv:math},
publisher = {Princeton University Press},
title = {Higher topos theory},
year = {2009}
}
@incollection{Gibbons2015,
abstract = {A classic layout for complex software applications usually involves a set of fine-tuned performance-optimized routines that are combined and controlled from a higher layer in a lightweight fashion. As the application grows, reliable operation, portability, and maintainability gets to be a real concern. However, this can be tamed by abstracting away from the platform-dependent details by modelling the components and their relation on a higher level. Using a functional programming language combined with the technique of language embedding may be an answer when implementation of such solution comes in question [1][2]. In this design, the component descriptions may be captured by an adequate embedded domain-specific language that compiles to a lower-level language but there also has to be a way for composition and therefore getting a complete working application out of them. In this paper, we propose a method for extending compiled embedded domain-specific languages into a stand-alone system with minimal effort. {\textcopyright} 2012 Springer-Verlag.},
archivePrefix = {arXiv},
arxivId = {9780201398298},
author = {Gibbons, Jeremy},
booktitle = {Cent. Eur. Funct. Program. Sch. CEFP 2013},
doi = {10.1007/978-3-319-15940-9_1},
editor = {Zs{\'{o}}k, Vikt{\'{o}}ria and Horv{\'{a}}th, Zolt{\'{a}}n and Csat{\'{o}}, Lehel},
eprint = {9780201398298},
isbn = {978-3-319-15939-3},
issn = {03029743},
pages = {1--28},
pmid = {4520227},
publisher = {Springer, Cham},
series = {Lecture Notes in Computer Science},
title = {Functional Programming for Domain-Specific Languages},
volume = {8606},
year = {2015}
}
@article{Awodey2013,
abstract = {From a logical point of view, Stone duality for Boolean algebras relates theories in classical propositional logic and their collections of models. The theories can be seen as presentations of Boolean algebras, and the collections of models can be topologized in such a way that the theory can be recovered from its space of models. The situation can be cast as a formal duality relating two categories of syntax and semantics, mediated by homming into a common dualizing object, in this case 2.In the present work, we generalize the entire arrangement from propositional to first-order logic, using a representation result of Butz and Moerdijk. Boolean algebras are replaced by Boolean categories presented by theories in first-order logic, and spaces of models are replaced by topological groupoids of models and their isomorphisms. A duality between the resulting categories of syntax and semantics, expressed primarily in the form of a contravariant adjunction, is established by homming into a common dualizing object, now Sets, regarded once as a boolean category, and once as a groupoid equipped with an intrinsic topology.The overall framework of our investigation is provided by topos theory. Direct proofs of the main results are given, but the specialist will recognize toposophical ideas in the background. Indeed, the duality between syntax and semantics is really a manifestation of that between algebra and geometry in the two directions of the geometric morphisms that lurk behind our formal theory. Along the way, we give an elementary proof of Butz and Moerdijk's result in logical terms. ?? 2012 Elsevier B.V.},
archivePrefix = {arXiv},
arxivId = {1008.3145},
author = {Awodey, Steve and Forssell, Henrik},
doi = {10.1016/j.apal.2012.10.016},
eprint = {1008.3145},
issn = {01680072},
journal = {Ann. Pure Appl. Log.},
keywords = {Categorical logic,First-order logic,Topological semantics,Topos theory},
month = mar,
number = {3},
pages = {319--348},
publisher = {Elsevier B.V.},
title = {First-order logical duality},
volume = {164},
year = {2013}
}
@article{Klin2010,
author = {Klin, Bartek},
doi = {10.1016/j.entcs.2010.07.019},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {coalgebra,modal logic,structural operational semantics},
month = aug,
number = {2},
pages = {155--175},
publisher = {Elsevier B.V.},
title = {Structural Operational Semantics and Modal Logic, Revisited},
volume = {264},
year = {2010}
}
@article{Coquand2009,
abstract = {We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.},
author = {Coquand, Thierry and Spitters, Bas},
doi = {10.1017/S0305004109002515},
issn = {0305-0041},
journal = {Math. Proc. Cambridge Philos. Soc.},
language = {English},
month = may,
number = {02},
pages = {339},
publisher = {Cambridge University Press},
title = {Constructive Gelfand duality for C*-algebras},
volume = {147},
year = {2009}
}
@incollection{Bonsangue2008,
abstract = {We present a novel coalgebraic logic for deterministic Mealy machines that is sound, complete and expressive w.r.t. bisimulation. Every finite Mealy machine corresponds to a finite formula in the language. For the converse, we give a compositional synthesis algorithm which transforms every formula into a finite Mealy machine whose behaviour is exactly the set of causal functions satisfying the formula.},
author = {Bonsangue, Marcello M. and Rutten, Jan J.M.M. and Silva, Alexandra},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-540-78499-9_17},
editor = {Amadio, Roberto},
pages = {231--245},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Coalgebraic logic and synthesis of Mealy machines},
year = {2008}
}
@incollection{Porst1991,
author = {Porst, Hans-E. and Tholen, Walter},
booktitle = {Categ. Theory Work},
isbn = {3-88538-218-0},
pages = {111--136},
publisher = {Heldermann Verlag Berlin},
title = {Concrete dualities},
type = {Journal article},
year = {1991}
}
@incollection{Lack2010,
archivePrefix = {arXiv},
arxivId = {math/0702535},
author = {Lack, Stephen},
booktitle = {Towar. High. Categ.},
doi = {10.1007/978-1-4419-1524-5_4},
editor = {Baez, John C. and May, J. Peter},
eprint = {0702535},
month = feb,
pages = {1--73},
primaryClass = {math},
publisher = {Springer New York},
series = {The IMA Volumes in Mathematics and its Applications},
title = {A 2-categories companion},
year = {2010}
}
@article{Plotkin2008,
abstract = {We present a logic for algebraic effects, based on the algebraic representation of computational effects by operations and equations. We begin with the a-calculus, a minimal calculus which separates values, effects, and computations and thereby canonises the order of evaluation. This is extended to obtain the logic, which is a classical first-order multi-sorted logic with higher-order value and computation types, as in Levy's call-by-push-value, a principle of induction over computations, a free algebra principle, and predicate fixed points. This logic embraces Moggi's computational lambda-calculus, and also, via definable modalities, Hennessy-Milner logic, and evaluation logic, though Hoare logic presents difficulties.},
author = {Plotkin, Gordon D. and Pretnar, Matija},
doi = {10.1109/LICS.2008.45},
isbn = {9780769531830},
issn = {10436871},
journal = {Proc. - Symp. Log. Comput. Sci.},
pages = {118--129},
title = {A logic for algebraic effects},
year = {2008}
}
@incollection{Eilenberg1966,
abstract = {In the usual theory of categories, with any two objects A, B of a category A there is associated a set A (A B) of morphisms of A into B. Frequently the set A (A B) is endowed with an additional structure such as a privileged element or an abelian group structure. It has become clear that as the ramifications of the theory of categories increase, the structures that A (A B) will carry will be richer and more complex. The need for a general theory has been widely felt for some time, and beginnings have been made in various directions and often under restrictive hypotheses; e.g. by Mac Lane [15], Kelly [10], B{\'{e}}nabou [3], Linton [12]},
address = {Berlin, Heidelberg},
author = {Eilenberg, Samuel and Kelly, Gregory Maxwell},
booktitle = {Proc. Conf. Categ. Algebr.},
doi = {10.1007/978-3-642-99902-4_22},
isbn = {978-3-642-99904-8},
pages = {421--562},
publisher = {Springer Berlin Heidelberg},
title = {Closed Categories},
year = {1966}
}
@techreport{Necula1996,
author = {Necula, George C. and Lee, Peter},
booktitle = {Tech. Rep. C.},
institution = {School of Computer Science, Carnegie Mellon University},
keywords = {operating system security and,protection,safety of un-,system extensibility},
month = nov,
title = {Proof-Carrying Code},
year = {1996}
}
@article{NorbertFuhr;ThomasRolleke1997,
abstract = {We present a probabilistic data model which is based on relations in non-first-normal-form (NF2). Here, tuples are assigned probabilistic weights giving the probability that a tuple belongs to a relation. This way, imprecise attribute values are modelled as a probabilistic subrelation. For information retrieval, the set of weighted index terms of a document can be represented in the same way, thus supporting the integration of information retrieval and database systems. By redefining the relational operators for this type of relations, the result of each operator is again a probabilistic NF2 relation, where the weight of a tuple gives the probability that this tuple belongs to the result.},
author = {Fuhr, Norbert and R{\"{o}}lleke, Thomas},
doi = {10.1145/239041.239045},
issn = {10468188},
journal = {ACM Trans. Inf. Syst.},
month = jan,
number = {1},
pages = {32--66},
title = {A probabilistic relational algebra for the integration of information retrieval and database systems},
volume = {15},
year = {1997}
}
@inproceedings{Barak2007,
abstract = {The contingency table is a work horse of official statistics, the format of reported data for the US Census, Bureau of Labor Statistics, and the Internal Revenue Service. In many settings such as these privacy is not only ethically mandated, but frequently legally as well. Consequently there is an extensive and diverse literature dedicated to the problems of statistical disclosure control in contingency table release. However, all current techniques for reporting contingency tables fall short on at leas one of privacy, accuracy, and consistency (among multiple released tables). We propose a solution that provides strong guarantees for all three desiderata simultaneously. Our approach can be viewed as a special case of a more general approach for producing synthetic data: Any privacy-preserving mechanism for contingency table release begins with raw data and produces a (possibly inconsistent) privacy-preserving set of marginals. From these tables alone-and hence without weakening privacy--we will find and output the "nearest" consistent set of marginals. Interestingly, this set is no farther than the tables of the raw data, and consequently the additional error introduced by the imposition of consistency is no more than the error introduced by the privacy mechanism itself. The privacy mechanism of [20] gives the strongest known privacy guarantees, with very little error. Combined with the techniques of the current paper, we therefore obtain excellent privacy, accuracy, and consistency among the tables. Moreover, our techniques are surprisingly efficient. Our techniques apply equally well to the logical cousin of the contingency table, the OLAP cube.},
address = {New York, New York, USA},
author = {Barak, Boaz and Chaudhuri, Kamalika and Dwork, Cynthia and Kale, Satyen and McSherry, Frank and Talwar, Kunal},
booktitle = {Proc. twenty-sixth ACM SIGMOD-SIGACT-SIGART Symp. Princ. database Syst. - Pod. '07},
doi = {10.1145/1265530.1265569},
isbn = {9781595936851},
keywords = {OLAP,contingency table,privacy},
pages = {273},
publisher = {ACM Press},
title = {Privacy, accuracy, and consistency too},
year = {2007}
}
@article{Day1978a,
author = {Day, Brian J.},
doi = {10.1017/S0004972700008613},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
number = {01},
pages = {157},
title = {Duality in topological algebra: Addendum},
volume = {19},
year = {1978}
}
@inproceedings{Reynolds1983,
author = {Reynolds, John C.},
booktitle = {Inf. Process. 83},
editor = {Mason, R. E. A.},
pages = {513--513},
publisher = {Elsevier Science Publishers},
title = {Types, abstraction, and parametric Polymorphism},
year = {1983}
}
@book{Perrin2004,
author = {Perrin, Dominique and Pin, Jean-{\'{E}}ric},
doi = {10.1016/S0079-8169(04)80001-1},
editor = {Perrin, Dominique and Pin, Jean-{\'{E}}ric},
isbn = {978-0-12-532111-2},
pages = {1--3},
publisher = {Elsevier},
series = {Pure and Applied Mathematics},
title = {Infinite Words Automata, Semigroups, Logic and Games},
volume = {141},
year = {2004}
}
@article{Varacca2006,
author = {Varacca, Daniele and Winskel, Glynn},
doi = {10.1017/S0960129505005074},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = feb,
number = {01},
pages = {87},
title = {Distributing probability over non-determinism},
volume = {16},
year = {2006}
}
@incollection{Italiano2015,
address = {Berlin, Heidelberg},
author = {{\'{E}}sik, Zolt{\'{a}}n},
booktitle = {Proc. 40th Math. Found. Comput. Sci.},
doi = {10.1007/978-3-662-48057-1_2},
editor = {Italiano, Giuseppe F and Pighizzini, Giovanni and Sannella, Donald T.},
isbn = {978-3-662-48056-4},
issn = {16113349},
pages = {18--37},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Equational properties of fixed point operations in cartesian categories: An overview},
volume = {9234},
year = {2015}
}
@article{Kurz2010,
author = {Kurz, Alexander and Petrişan, Daniela},
doi = {10.1016/j.ic.2009.11.007},
issn = {08905401},
journal = {Inf. Comput.},
month = dec,
number = {12},
pages = {1421--1446},
title = {Presenting functors on many-sorted varieties and applications},
volume = {208},
year = {2010}
}
@article{Bauer2012,
abstract = {We prove that the category of left-handed skew distributive lattices with zero and proper homomorphisms is dually equivalent to a category of sheaves over local Priestley spaces. Our result thus provides a non-commutative version of classical Priestley duality for distributive lattices. The result also generalizes the recent development of Stone duality for skew Boolean algebras.},
archivePrefix = {arXiv},
arxivId = {1206.5848},
author = {Bauer, Andrej and Cvetko-Vah, Karin and Gehrke, Mai and van Gool, Sam J. and Kudryavtseva, Ganna},
eprint = {1206.5848},
month = jun,
pages = {19},
title = {A non-commutative Priestley duality},
year = {2012}
}
@article{Benthem1994,
author = {van Benthem, Johan and Bergstra, Jan},
doi = {10.1007/BF01160018},
issn = {0925-8531},
journal = {J. Logic, Lang. Inf.},
month = dec,
number = {4},
pages = {247--283},
title = {Logic of transition systems},
volume = {3},
year = {1994}
}
@incollection{Grillet1971,
author = {Grillet, Pierre Antoine},
booktitle = {Exact Categ. Categ. Sheaves},
doi = {10.1007/BFb0058581},
isbn = {978-3-540-05678-2},
pages = {121--222},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Regular categories},
volume = {i},
year = {1971}
}
@incollection{Elgot1975,
author = {Elgot, Calvin C.},
booktitle = {Proc. Log. Colloq. '73},
doi = {10.1016/S0049-237X(08)71949-9},
isbn = {9780444106421},
issn = {0049-237X},
pages = {175--230},
publisher = {Elsevier},
series = {Studies in Logic and the Foundations of Mathematics},
title = {Monadic computation and iterative algebraic theories},
year = {1975}
}
@incollection{Ancona2009,
author = {Ancona, Davide and Lagorio, Giovanni and Zucca, Elena},
booktitle = {Types for Proofs and Programs},
doi = {10.1007/978-3-642-02444-3_1},
editor = {Berardi, Stefano and Damiani, Ferruccio and De'Liguoro, Ugo},
keywords = {coinduction,nominal and structural typing,object-oriented languages,type inference},
pages = {1--18},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Type inference by coinductive logic programming},
year = {2009}
}
@misc{Ballester-Bolinches2012,
author = {Ballester-Bolinches, Adolfo and Pin, Jean-{\'{E}}ric and Soler-Escriv{\`{a}}, Xaro},
booktitle = {Forum Math.},
doi = {10.1515/forum-2012-0055},
issn = {0933-7741},
number = {6},
pages = {1737--1761},
title = {Formations of finite monoids and formal languages: Eilenberg's variety theorem revisited},
volume = {26},
year = {2012}
}
@article{Dalenius1986,
author = {Dalenius, Tore},
journal = {J. Off. Stat.},
number = {3},
pages = {329--336},
title = {Finding a Needle In a Haystack or Identifying Anonymous Census Records},
volume = {2},
year = {1986}
}
@article{Mcbride2008,
abstract = {In this paper, we introduce Applicative functors—an abstract characterisation of an ap- plicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this paper, introducing the applicative pattern by diverse exam- ples, then abstracting it to define the Applicative type class and introducing a bracket notation which interprets the normal application syntax in the idiom of an Applicative functor. Further, we develop the properties of applicative functors and the generic opera- tions they support.We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrows.},
author = {MCBRIDE, CONOR and PATERSON, ROSS},
doi = {10.1017/S0956796807006326},
isbn = {0956-7968},
issn = {0956-7968},
journal = {J. Funct. Program.},
month = jan,
number = {01},
pages = {1--13},
title = {Applicative programming with effects},
volume = {18},
year = {2008}
}
@inproceedings{Pirog2013,
abstract = {The monads used to model effectful computations traditionally concentrate on the 'destination' - the final results of the program. However, sometimes we are also interested in the 'journey' - the intermediate course of a computation - especially when reasoning about non-terminating interactive systems. In this article we claim that a necessary property of a monad for it to be able to describe the behaviour of a program is complete iterativity. We show how an ordinary monad can be modified to disclose more about its internal computational behaviour, by applying an associated transformer to a completely iterative monad. To illustrate this, we introduce two new constructions: a coinductive cousin of Cenciarelli and Moggi's generalised resumption transformer, and States - a State-like monad that accumulates the intermediate states. {\textcopyright} 2013 Elsevier B.V.},
author = {Pir{\'{o}}g, Maciej and Gibbons, Jeremy},
booktitle = {Proc. Twenty-ninth Conf. Math. Found. Program. Semant.},
doi = {10.1016/j.entcs.2013.09.019},
issn = {15710661},
keywords = {completely iterative monads,effects,resumptions,tracing},
pages = {309--324},
publisher = {Elsevier B.V.},
title = {Monads for Behaviour},
volume = {298},
year = {2013}
}
@article{Kock2012,
abstract = {The theory of commutative monads on cartesian closed categories provides a framework where aspects of the theory of distributions and other extensive quantities can be formulated and some results proved. We make explicit a link between our theory and the theory of Schwartz distributions of compact support. We also discuss probability distributions.},
archivePrefix = {arXiv},
arxivId = {1108.5952},
author = {Kock, Anders},
eprint = {1108.5952},
issn = {1201561X},
journal = {Theory Appl. Categ.},
keywords = {Distributions,Extensive quantities,Monads},
number = {4},
pages = {97--131},
title = {Commutative monads as a theory of distributions},
volume = {26},
year = {2012}
}
@article{Kroupa2012,
abstract = {We generalise belief functions to many-valued events which are represented by elements of Lindenbaum algebra of infinite-valued {\L}ukasiewicz propositional logic. Our approach is based on mass assignments used in the Dempster-Shafer theory of evidence. A generalised belief function is totally monotone and it has Choquet integral representation with respect to a unique belief measure on Boolean events. {\textcopyright} 2012 Springer-Verlag.},
author = {Kroupa, Tom{\'{a}}{\v{s}}},
doi = {10.1007/s00500-012-0836-2},
issn = {1432-7643},
journal = {Soft Comput.},
keywords = {Belief function,Choquet integral,MV-algebra,M{\"{o}}bius transform,{\L}ukasiewicz logic},
month = nov,
number = {11},
pages = {1851--1861},
title = {Extension of belief functions to infinite-valued events},
volume = {16},
year = {2012}
}
@incollection{Bove2012a,
abstract = {We propose a new approach to the computer-assisted verification of functional programs. We work in first order theories of functional programs which are obtained by extending Aczel's first order theory of combinatory formal arithmetic with positive inductive and coinductive predicates. Rather than building a special purpose system we implement our theories in Agda, a proof assistant for dependent type theory which can be used as a generic theorem prover. Agda provides support for interactive reasoning by encoding first order theories using the formulae-as-types principle. Further support is provided by off-the-shelf automatic theorem provers for first order logic which can be called by a program which translates Agda representations of first order formulae into the TPTP language understood by the provers. We show some examples where we combine interactive and automatic reasoning, covering both proof by induction and coinduction.},
author = {Bove, Ana and Dybjer, Peter and Sicard-Ram{\'{i}}rez, Andr{\'{e}}s and {Andr{\'{e}}s Sicard-Ram{\'{i}}rez}},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/978-3-642-28729-9_7},
editor = {Birkedal, Lars},
isbn = {978-3-642-28728-2},
pages = {104--118},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs},
volume = {7213},
year = {2012}
}
@article{Hyland2007,
author = {Hyland, Martin and Levy, Paul Blain and Plotkin, Gordon D. and Power, A. John},
doi = {10.1016/j.tcs.2006.12.026},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {computational effect,lawvere theory,modularity,monad},
month = may,
number = {1-3},
pages = {20--40},
title = {Combining algebraic effects with continuations},
volume = {375},
year = {2007}
}
@article{Buneman1991,
abstract = {Much of relational algebra and the underlying principles of relational database design have a simple representation in the theory of domains that is traditionally used in the denotational semantics of programming languages. By investigating the possible orderings on powerdomains that are well known in the study of nondeterminism and concurrency it is possible to show that many of the ideas in relational databases apply to structures that are much more general than relations. This also suggests a method of representing database objects as typed objects in programming languages. In this paper we show how operations such as natural join and projection-which are fundamental to relational database design-can be generalized, and we use this generalized framework to give characterizations of several relational database concepts including functional dependencies and universal relations. All of these have a simple-minded semantics in terms of the underlying domains, which can be thought of as domains of partial descriptions of "real-world" objects. We also discuss the applicability of relational database theory to nonrelational structures such as records with variants, higher-order relations, recursive structures and other ordered spaces. {\textcopyright} 1991.},
author = {Buneman, Peter and Jung, Achim and Ohori, Atsushi},
doi = {10.1016/0304-3975(91)90266-5},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = dec,
number = {1},
pages = {23--55},
title = {Using powerdomains to generalize relational databases},
volume = {91},
year = {1991}
}
@article{Kelly1997,
author = {Kelly, Gregory Maxwell and Lack, Stephen},
journal = {Theory Appl. Categ.},
keywords = {1997,2-category,and phrases,c g,kelly and stephen lack,m,monad,permission to copy for,private use granted,property,structure},
number = {9},
pages = {213--250},
title = {On property-like structures},
volume = {3},
year = {1997}
}
@article{Palamidessi2012,
abstract = {Differential privacy is a modern approach in privacy-preserving data analysis to control the amount of information that can be inferred about an individual by querying a database. The most common techniques are based on the introduction of probabilistic noise, often defined as a Laplacian parametric on the sensitivity of the query. In order to maximize the utility of the query, it is crucial to estimate the sensitivity as precisely as possible. In this paper we consider relational algebra, the classical language for queries in relational databases, and we propose a method for computing a bound on the sensitivity of queries in an intuitive and compositional way. We use constraint-based techniques to accumulate the information on the possible values for attributes provided by the various components of the query, thus making it possible to compute tight bounds on the sensitivity.},
archivePrefix = {arXiv},
arxivId = {1207.0872},
author = {Palamidessi, Catuscia and Stronati, Marco},
doi = {10.4204/EPTCS.85.7},
eprint = {1207.0872},
issn = {2075-2180},
journal = {Electron. Proc. Theor. Comput. Sci.},
month = jul,
number = {Qapl},
pages = {92--105},
title = {Differential Privacy for Relational Algebra: Improving the Sensitivity Bounds via Constraint Systems},
volume = {85},
year = {2012}
}
@incollection{Escardo2015,
author = {Escard{\'{o}}, Mart{\'{i}}n H{\"{o}}tzel and Xu, Chuangjie},
booktitle = {13th Int. Conf. Typed Lambda Calc. Appl.},
doi = {10.4230/LIPIcs.TLCA.2015.153},
editor = {Altenkirch, Thorsten},
keywords = {153,2015,4230,and phrases dependent type,anonymous existence,brouwerian continuity axioms,constructive mathematics,curry,digital object identifier 10,function extensionality,homotopy type theory,howard in-,intensional martin-l{\"{o}}f type theory,lipics,positional truncation,pro-,terpretation,tlca,topos theory},
pages = {153--164},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics},
title = {The Inconsistency of a Brouwerian Continuity Principle with the Curry – Howard Interpretation},
year = {2015}
}
@article{Bellin2006,
abstract = {We investigate semantics for classical proof based on the sequent calculus. We show that the propositional connectives are not quite well-behaved from a traditional categorical perspective, and give a more refined, but necessarily complex, analysis of how connectives may be characterised abstractly. Finally we explain the consequences of insisting on more familiar categorical behaviour.},
author = {Bellin, Gianluigi and Hyland, Martin and Robinson, Edmund P. and Urban, Christian},
doi = {10.1016/j.tcs.2006.08.002},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {category theory,classical logic,proof theory},
month = nov,
number = {2},
pages = {146--165},
title = {Categorical proof theory of classical propositional calculus},
volume = {364},
year = {2006}
}
@article{Gabbay2002a,
abstract = {The permutation model of set theory with atoms (FM-sets), devised by Fraenkel and Mostowski in the 1930s, supports notions of ‘name-abstraction' and ‘fresh name' that provide a new way to represent, compute with, and reason about the syntax of formal systems involving variable-binding operations. Inductively defined FM-sets involving the name-abstraction set former (together with Cartesian product and disjoint union) can correctly encode syntax modulo renaming of bound variables. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc.) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice in computer science.},
author = {Gabbay, Murdoch J. and Pitts, Andrew M.},
doi = {10.1007/s001650200016},
issn = {0934-5043},
journal = {Form. Asp. Comput.},
keywords = {abstract,abstract syntax,alpha-conversion,and,and reason about the,compute with,devised by fraenkel and,fm-sets,fresh name,in the 1930s,in-,involving variable-binding operations,mostowski,name-abstraction,permutation actions,set theory,set theory with atoms,structural induction,supports notions of,syntax of formal systems,that provide a new,the permutation model of,way to represent},
month = mar,
number = {3-5},
pages = {341--363},
title = {A New Approach to Abstract Syntax with Variable Binding},
volume = {13},
year = {2002}
}
@article{Turi1998a,
author = {Turi, Daniele and Rutten, Jan J.M.M.},
issn = {1469-8072},
journal = {Math. Struct. Comput. Sci.},
language = {English},
month = oct,
number = {5},
pages = {481--540},
title = {On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces},
type = {Journal article},
volume = {8},
year = {1998}
}
@article{Adamek1995,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1016/0022-4049(94)00152-9},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = dec,
number = {3},
pages = {225--232},
title = {On preaccessible categories},
volume = {105},
year = {1995}
}
@article{Urban2008,
author = {Urban, Christian},
doi = {10.1007/s10817-008-9097-2},
isbn = {1081700890},
issn = {0168-7433},
journal = {J. Autom. Reason.},
keywords = {lambda-calculus,nominal logic work,theorem provers},
month = mar,
number = {4},
pages = {327--356},
title = {Nominal techniques in Isabelle/HOL},
volume = {40},
year = {2008}
}
@incollection{Dwork2006a,
abstract = {We continue a line of research initiated in [10,11]on privacy-preserving statistical databases. Consider a trusted server that holds a database of sensitive information. Given a query function f mapping databases to reals, the so-called true answer is the result of applying f to the database. To protect privacy, the true answer is perturbed by the addition of random noise generated according to a carefully chosen distribution, and this response, the true answer plus noise, is returned to the user. Previous work focused on the case of noisy sums, in which f = ?i g(xi), where xi denotes the ith row of the database and g maps database rows to [0, 1]. We extend the study to general functions f, proving that privacy can be preserved by calibrating the standard devi- ation of the noise according to the sensitivity of the function f. Roughly speaking, this is the amount that any single argument to f can change its output. The new analysis shows that for several particular applications substantially less noise is needed than was previously understood to be the case. The first step is a very clean characterization of privacy in terms of indistinguishability of transcripts. Additionally, we obtain separation re- sults showing the increased value of interactive sanitization mechanisms over non-interactive.},
archivePrefix = {arXiv},
arxivId = {arXiv:1203.3453v5},
author = {Dwork, Cynthia and McSherry, Frank and Nissim, Kobbi and Smith, Adam},
booktitle = {Theory Cryptogr. TCC 2006.},
doi = {10.1007/11681878_14},
eprint = {arXiv:1203.3453v5},
isbn = {3-540-32731-2},
issn = {1520-6017},
number = {8},
pages = {265--284},
pmid = {21455981},
title = {Calibrating Noise to Sensitivity in Private Data Analysis},
volume = {3876},
year = {2006}
}
@incollection{Gehrke2008,
address = {Berlin, Heidelberg},
author = {Gehrke, Mai and Grigorieff, Serge and Pin, Jean-{\'{E}}ric},
booktitle = {ICALP 2008, Part II},
doi = {10.1007/978-3-540-70583-3_21},
editor = {Aceto, Luca and Damg{\aa}rd, Ivan and Goldberg, Leslie Ann and Halld{\'{o}}rsson, Magn{\'{u}}s M. and Ing{\'{o}}lfsd{\'{o}}ttir, Anna and Walukiewicz, Igor},
pages = {246--257},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Duality and Equational Theory of Regular Languages},
year = {2008}
}
@article{Kennison1968,
author = {Kennison, John F.},
journal = {Illinois J. Math.},
number = {3},
pages = {353--365},
title = {Full reflective subcategories and generalized covering spaces},
volume = {12},
year = {1968}
}
@inproceedings{Cirstea2013,
abstract = {We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that by suitably adapting the definition of coalgebraic bisimulation, one obtains a general and uniform account of the linear-time behaviour of a state in such a coalgebra. By moving away from a boolean universe of truth values, our approach can measure the extent to which a state in a system with branching is able to exhibit a particular linear-time behaviour. This instantiates to measuring the probability of a specific behaviour occurring in a probabilistic system, or measuring the minimal cost of exhibiting a specific behaviour in the case of weighted computations.},
author = {C{\^{i}}rstea, Corina},
booktitle = {Work. Fixed Points Comput. Sci.},
doi = {10.4204/EPTCS.126.2},
issn = {2075-2180},
month = aug,
pages = {11--27},
title = {From branching to linear time, coalgebraically},
volume = {126},
year = {2013}
}
@incollection{Kohlas2000,
address = {Dordrecht},
author = {Kohlas, J{\"{u}}rg and Shenoy, Prakash P},
booktitle = {Handb. Defeasible Reason. Uncertain. Manag. Syst.},
doi = {10.1007/978-94-017-1737-3_2},
number = {2100},
pages = {5--39},
publisher = {Springer Netherlands},
title = {Computation in Valuation Algebras},
volume = {5},
year = {2000}
}
@article{Kozen2013,
author = {Kozen, Dexter and Larsen, Kim G. and Mardare, Radu and Panangaden, Prakash},
doi = {10.1109/LICS.2013.38},
isbn = {978-1-4799-0413-6},
journal = {2013 28th Annu. ACM/IEEE Symp. Log. Comput. Sci.},
month = jun,
pages = {321--330},
publisher = {Ieee},
title = {Stone Duality for Markov Processes},
year = {2013}
}
@article{Hyland2014,
author = {Hyland, Martin},
doi = {10.1016/j.tcs.2014.03.005},
issn = {03043975},
journal = {Theor. Comput. Sci.},
pages = {132--144},
publisher = {Elsevier B.V.},
title = {Elements of a theory of algebraic theories},
volume = {546},
year = {2014}
}
@article{Adamek1997,
abstract = {For every sketch with countable limit specifications and countable colimit specifications we prove that there exists a finitary sketch (i.e., one with finite limit and colimit specifications) with the same category of finite models. The sketch is even coherent, i.e., describable by the finitary first-order logic. Assuming the non-existence of measurable cardinals, we also prove that for every geometric sketch there exists a coherent sketch with the same category of finite models. The latter result is, in fact, equivalent to the assumption of non-existence of measurable cardinals.},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Rosick{\'{y}}, Jiř{\'{i}}},
doi = {10.1016/S0022-4049(96)00159-4},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = mar,
number = {1-3},
pages = {3--23},
title = {Finite models of sketches},
volume = {116},
year = {1997}
}
@inproceedings{Jones,
author = {Jones, C. and Plotkin, Gordon D.},
booktitle = {Proceedings. Fourth Annu. Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.1989.39173},
isbn = {0-8186-1954-6},
pages = {186--195},
publisher = {IEEE Comput. Soc. Press},
title = {A probabilistic powerdomain of evaluations},
year = {1989}
}
@article{Goncharov2014,
abstract = {Strong bisimulation for labelled transition systems is one of the most fundamental equivalences in process algebra, and has been generalised to numerous classes of systems that exhibit richer transition behaviour. Nearly all of the ensuing notions are instances of the more general notion of coalgebraic bisimulation. Weak bisimulation, however, has so far been much less amenable to a coalgebraic treatment. Here we attempt to close this gap by giving a coalgebraic treatment of (parametrized) weak equivalences, including weak bisimulation. Our analysis requires that the functor defining the transition type of the system is based on a suitable order-enriched monad, which allows us to capture weak equivalences by least fixpoints of recursive equations. Our notion is in agreement with existing notions of weak bisimulations for labelled transition systems, probabilistic and weighted systems, and simple Segala systems.},
archivePrefix = {arXiv},
arxivId = {1404.1215},
author = {Goncharov, Sergey and Pattinson, Dirk},
eprint = {1404.1215},
journal = {ArXiv e-prints},
month = apr,
number = {1},
pages = {1--25},
title = {Coalgebraic Weak Bisimulation from Recursive Equations over Monads},
year = {2014}
}
@inproceedings{Cirstea2009,
abstract = {The coalgebraic approach to modal logic provides a uniform framework that captures the semantics of a large class of structurally different modal logics, including e.g. graded and probabilistic modal logics and coalition logic. In this paper, we introduce the coalgebraic mu-calculus, an extension of the general (coalgebraic) framework with fixpoint operators. Our main results are completeness of the associated tableau calculus and EXPTIME decidability. Technically, this is achieved by reducing satisfiability to the existence of non-wellfounded tableaux, which is in turn equivalent to the existence of winning strategies in parity games. Our results are parametric in the underlying class of models and yield, as concrete applications, previously unknown complexity bounds for the probabilistic mu-calculus and for an extension of coalition logic with fixpoints.},
address = {Berlin, Heidelberg},
author = {C{\^{i}}rstea, Corina and Kupke, Clemens and Pattinson, Dirk and Gr{\"{a}}del, Erich and Kahle, Reinhard},
booktitle = {Comput. Sci. Log.},
doi = {10.1007/978-3-642-04027-6},
editor = {Gr{\"{a}}del, Erich and Kahle, Reinhard},
isbn = {978-3-642-04026-9},
keywords = {Computer Science},
pages = {179--193},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {EXPTIME tableaux for the coalgebraic $\mu$-calculus},
volume = {5771},
year = {2009}
}
@incollection{Kurz2010b,
author = {Kurz, Alexander and Venema, Yde},
booktitle = {Adv. Modal Log.},
editor = {Beklemishev, Lev and Goranko, Valentin and Shehtman, Valentin},
isbn = {978-1-84890-013-4},
keywords = {Lindstr{\"{o}}m,coalgebra,modal logic},
pages = {292--309},
publisher = {College Publications},
title = {Coalgebraic Lindstr{\"{o}}m Theorems},
volume = {8},
year = {2010}
}
@phdthesis{Silva2010,
author = {Silva, Alexandra},
isbn = {9789064644337},
month = aug,
school = {Centrum Wiskunde & Informatica},
title = {Kleene Coalgebra},
year = {2010}
}
@inproceedings{Pirog2014,
abstract = {Resumptions appear in many forms as a convenient abstraction, such as in semantics of concurrency and as a programming pattern. In this paper we introduce generalised resumptions in a category-theoretic, coalgebraic context and show their basic properties: they form a monad, they come equipped with a corecursion scheme in the sense of Ad{\'{a}}mek et al.'s notion of completely iterative monads (cims), and they enjoy a certain universal property, which specialises to the coproduct with a free cim in the category of cims.},
author = {Pir{\'{o}}g, Maciej and Gibbons, Jeremy},
booktitle = {Proc. 30th Conf. Math. Found. Program. Semant.},
doi = {10.1016/j.entcs.2014.10.015},
issn = {15710661},
keywords = {coalgebra,completely iterative monads,resumptions},
pages = {273--288},
publisher = {Elsevier B.V.},
title = {The coinductive resumption monad},
volume = {308},
year = {2014}
}
@article{Lawvere1969,
author = {Lawvere, F. William},
journal = {Dialectica},
pages = {1--16},
title = {Adjointness in foundations},
volume = {23},
year = {1969}
}
@techreport{Motwani2007,
abstract = {A quasi-identifier refers to a subset of attributes that can uniquely identify most tuples in a table. Incautious pub-lication of quasi-identifiers will lead to privacy leakage. In this paper we consider the problems of finding and masking quasi-identifiers. Both problems are provably hard with se-vere time and space requirements. We focus on designing efficient approximation algorithms for large data sets. We first propose two natural measures for quantifying quasi-identifiers: distinct ratio and separation ratio. We develop efficient algorithms that find small quasi-identifiers with provable size and separation/distinct ratio guarantees, with space and time requirements sublinear in the number of tuples. We also design practical algorithms for finding all minimal quasi-identifiers. Finally we propose efficient algo-rithms for masking quasi-identifiers, where we use a random sampling technique to greatly reduce the space and time requirements, without much sacrifice in the quality of the results. Our algorithms for masking and finding minimum quasi-identifiers naturally apply to stream databases. Ex-tensive experimental results on real world data sets confirm efficiency and accuracy of our algorithms.},
author = {Motwani, Rajeev and Xu, Ying},
isbn = {9781595936493},
title = {Efficient Algorithms for Masking and Finding Quasi-Identifiers},
year = {2007}
}
@incollection{Casley1989,
author = {Casley, Ross and Crew, Roger F. and Meseguer, Jos{\'{e}} and Pratt, Vaughan},
booktitle = {Categ. Theory Comput. Sci.},
doi = {10.1007/BFb0018343},
editor = {Pitt, David H. and Rydeheard, David E. and Dybjer, Peter and Pitts, Andrew M. and Poign{\'{e}}, Axel},
isbn = {978-3-540-46740-3},
pages = {21--51},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Temporal structures},
year = {1989}
}
@article{Pippenger1997,
author = {Pippenger, Nicholas},
doi = {10.1007/BF02679444},
issn = {1432-4350},
journal = {Theory Comput. Syst.},
month = jul,
number = {2},
pages = {121--134},
title = {Regular languages and stone duality},
volume = {30},
year = {1997}
}
@article{Bezhanishvili1998a,
abstract = {This paper deals with the varieties of monadic Heyting algebras, algebraic models of intuitionistic modal logic MIPC. We investigate semisimple, locally finite, finitely approximated and splitting varieties of monadic Heyting algebras as well as varieties with the disjunction and the existence properties. The investigation of monadic Heyting algebras clarifies the correspondence between intuitionistic modal logics over MIPC and superintuitionistic predicate logics and provides us with the solutions of several problems raised by Ono [35].},
author = {Bezhanishvili, Guram},
doi = {10.1023/A:1005073905902},
journal = {Stud. Log.},
number = {3},
pages = {367--402},
title = {Varieties of Monadic Heyting Algebras. Part I},
volume = {61},
year = {1998}
}
@article{Ghani2001,
abstract = {Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad. {\textcopyright}2001 Published by Elsevier Science B. V.},
author = {Ghani, Neil and L{\"{u}}th, Christoph and {De Marchi}, Federico and Power, A. John},
doi = {10.1016/S1571-0661(04)80905-8},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
number = {1},
pages = {131--148},
title = {Algebras, coalgebras, monads and comonads},
volume = {44},
year = {2001}
}
@inproceedings{Adamek2015b,
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Milius, Stefan and Urbat, Henning},
booktitle = {6th Conf. Algebr. Coalgebra Comput. Sci.},
doi = {10.4230/LIPIcs.CALCO.2015.1},
keywords = {1,2015,4230,algebra,algebraic automata theory,and phrases syntactic monoid,calco,coalgebra,commutative variety,digital object identifier 10,duality,lipics,symmetric monoidal closed category,transition monoid},
title = {Syntactic Monoids in a Category},
year = {2015}
}
@article{Jirousek2018,
abstract = {We propose a new definition of entropy of basic probability assignments (BPAs) in the Dempster–Shafer (DS) theory of belief functions, which is interpreted as a measure of total uncertainty in the BPA. Our definition is different from those proposed by H{\"{o}}hle, Smets, Yager, Nguyen, Dubois–Prade, Lamata–Moral, Klir–Ramer, Klir–Parviz, Pal et al., Maeda–Ichihashi, Harmanec–Klir, Abell{\'{a}}n–Moral, Jousselme et al., Pouly et al., and Deng. We state a list of six desired properties of entropy for DS belief functions theory, four of which are motivated by Shannon's definition of entropy of probability functions, and the remaining two are requirements that adapt this measure to the philosophy of the DS theory. Three of our six desired properties are different from the five properties proposed by Klir and Wierman. We demonstrate that our definition satisfies all six properties in our list, whereas none of the existing definitions do. Our new definition has two components. The first component is Shannon's entropy of an equivalent probability mass function obtained using the plausibility transform, which constitutes the conflict measure of entropy. The second component is Dubois–Prade's definition of entropy of basic probability assignments in the DS theory, which constitutes the non-specificity measure of entropy. Our new definition is the sum of these two components. Our definition does not satisfy the subadditivity property. Whether there exists a definition that satisfies our six properties plus subadditivity remains an open question.},
author = {Jirou{\v{s}}ek, Radim and Shenoy, Prakash P.},
doi = {10.1016/j.ijar.2017.10.010},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Dempster's rule of combination,Dempster–Shafer theory of belief functions,Dempster–Shafer theory semantics,Maximum entropy property,Plausibility transform of a belief function},
month = jan,
pages = {49--65},
publisher = {Elsevier Inc.},
title = {A new definition of entropy of belief functions in the Dempster–Shafer theory},
volume = {92},
year = {2018}
}
@article{Rivieccio2017,
abstract = {We introduce a family of modal expansions of Belnap-Dunn four-valued logic and related systems, and interpret them in many-valued Kripke structures. Using algebraic logic techniques and topological duality for modal algebras, and generalizing the so-called twist-structure representation, we axiomatize by means of Hilbert-style calculi the least modal logic over the four-element Belnap lattice and some of its axiomatic extensions. We study the algebraic models of these systems, relating them to the algebraic semantics of classical multi-modal logic. This link allows us to prove that both local and global consequence of the least four-valued modal logic enjoy the finite model property and are therefore decidable.},
author = {Rivieccio, Umberto and Jung, Achim and Jansana, Ramon},
doi = {10.1093/logcom/exv038},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {Belnap logic,Bilattices,Many-valued modal logic,Paraconsistent Nelson logic},
month = feb,
number = {1},
pages = {155--199},
title = {Four-valued modal logic: Kripke semantics and duality},
volume = {27},
year = {2017}
}
@incollection{Urbat2017,
author = {Urbat, Henning and Ad{\'{a}}mek, Jiř{\'{i}} and Chen, Liang-ting and Milius, Stefan},
booktitle = {42nd Int. Symp. Math. Found. Comput. Sci. (MFCS 2017)},
doi = {10.4230/LIPIcs.MFCS.2017.43},
editor = {Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
keywords = {2017,4230,43,and phrases eilenberg,digital object identifier 10,duality,lipics,mfcs,monad,pseudovariety,s theorem,variety of languages},
pages = {43:1----43:15},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Eilenberg Theorems for Free},
volume = {83},
year = {2017}
}
@book{Barwise1996a,
author = {Barwise, Jon and Moss, Lawrence S.},
isbn = {1575860082},
publisher = {University of Chicago Press},
series = {CSLI Lecture Notes},
title = {Vicious Circles},
type = {Book},
year = {1996}
}
@article{Bezhanishvili1999,
abstract = {In this paper we continue the investigation of monadic Heyting algebras which we started in [2]. Here we present the representation theorem for monadic Heyting algebras and develop the duality theory for them. As a result we obtain an adequate topological semantics for intuitionistic modal logics over MIPC along with a Kripke-type semantics for them. It is also shown the importance and the effectiveness of the duality theory for further investigation of monadic Heyting algebras and logics over MIPC.},
author = {Bezhanishvili, Guram},
doi = {10.1023/A:1005173628262},
journal = {Stud. Log.},
number = {1},
pages = {21--48},
title = {Varieties of Monadic Heyting Algebras Part II. Duality Theory},
volume = {62},
year = {1999}
}
@book{Bird1996,
author = {Bird, Richard and de Moor, Oege},
isbn = {978-0135072455},
pages = {312},
publisher = {Prentice-Hall},
title = {The Algebra of Programming},
year = {1996}
}
@book{Milner1999a,
author = {Milner, Robin},
isbn = {0521658691},
publisher = {Cambridge Univ Pr},
title = {Communicating and mobile systems: the $\pi$-calculus},
type = {Book},
year = {1999}
}
@article{Hasuo2011b,
author = {Hasuo, Ichiro and Jacobs, Bart},
doi = {10.1017/S0960129510000551},
isbn = {0960129510},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = mar,
number = {02},
pages = {267--320},
title = {Traces for coalgebraic components},
volume = {21},
year = {2011}
}
@inproceedings{Bhat,
author = {Bhat, G. and Cleaveland, Rance},
booktitle = {Proc. 11th Annu. IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.1996.561358},
isbn = {0-8186-7463-6},
pages = {304--312},
publisher = {IEEE Comput. Soc. Press},
title = {Efficient model checking via the equational $\mu$-calculus},
year = {1996}
}
@article{Worrell1999,
abstract = {We consider the behaviour of the terminalsequence of an accessible endofunctor T on a locally presentable category K. The preservation of monics by T is sufficient to imply convergence, necessarily to a terminal coalgebra. We can say much more if K is Set, and $\kappa$ is $\omega$. In that case it is well known that we do not necessarily get convergence at $\omega$, however we show that to ensure convergence we don't need to go to a higher cardinal, just to the next limit ordinal, $\omega$ + $\omega$. For an $\omega$-accessible endofunctor T on Set the construction of the terminal coalgebra can thus be seen as a two stage construction, with each stage being finitary. The first stage obtains the Cauchy completion of the initial T-algebra as the $\omega$-th object in the terminalsequenceA$\omega$. In the second stage this object is pruned to get the final coalgebra A$\omega$+$\omega$. We give an example where A$\omega$ is the solution of the corresponding domain equation in the category of complete ultra-metric spaces.},
author = {Worrell, James},
doi = {10.1016/S1571-0661(05)80267-1},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
month = jan,
pages = {24--38},
title = {Terminal sequences for accessible endofunctors},
volume = {19},
year = {1999}
}
@article{Mislove2007,
abstract = {Labelled Markov processes (LMPs) are labelled transition systems in which each transition has an associated probability. In this paper we present a universal LMP as the spectrum of a commutative C*-algebra consisting of formal linear combinations of labelled trees. This yields a simple trace-tree semantics for LMPs that is fully abstract with respect to probabilistic bisimilarity. We also consider LMPs with distinguished entry and exit points as stateful stochastic relations. This allows us to define a category GSRel of generalized stochastic relations, which has measurable spaces as objects and LMPs as morphisms. Our main result in this context is to provide a predicate-transformer duality for GSRel that generalises Kozen's duality for the category SRel of stochastic relations.},
author = {Mislove, Michael W. and Pavlovi{\'{c}}, Dusko and Worrell, James},
doi = {10.1016/j.entcs.2007.02.015},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {(generalized) stochastic relation,c*-algebra,comonad,labelled markov process,probabilistic bisimulation,stone duality},
month = apr,
pages = {459--478},
title = {Labelled Markov Processes as Generalised Stochastic Relations},
volume = {172},
year = {2007}
}
@book{Bird1998,
author = {Bird, Richard},
edition = {2},
isbn = {9780134843469},
publisher = {Prentice Hall},
title = {Introduction to Functional Programming using Haskell},
year = {1998}
}
@inproceedings{Reed2010,
abstract = {We want assurances that sensitive information will not be disclosed when aggregate data derived from a database is published. Differential privacy offers a strong statistical guarantee that the effect of the presence of any individual in a database will be negligible, even when an adversary has auxiliary knowledge. Much of the prior work in this area consists of proving algorithms to be differentially private one at a time; we propose to streamline this process with a functional language whose type system automatically guarantees differential privacy, allowing the programmer to write complex privacy-safe query programs in a flexible and compositional way. The key novelty is the way our type system captures function sensitivity, a measure of how much a function can magnify the distance between similar inputs: well-typed programs not only can't go wrong, they can't go too far on nearby inputs. Moreover, by introducing a monad for random computations, we can show that the established definition of differential privacy falls out naturally as a special case of this soundness principle. We develop examples including known differentially private algorithms, privacy-aware variants of standard functional programming idioms, and compositionality principles for differential privacy.},
address = {New York, New York, USA},
author = {Reed, Jason and Pierce, Benjamin C.},
booktitle = {Proc. 15th ACM SIGPLAN Int. Conf. Funct. Program. - ICFP '10},
doi = {10.1145/1863543.1863568},
isbn = {9781605587943},
issn = {03621340},
month = sep,
number = {9},
pages = {157},
publisher = {ACM Press},
title = {Distance makes the types grow stronger},
volume = {45},
year = {2010}
}
@article{GrzegorzJarzembski1994,
author = {{Grzegorz Jarzembski}},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {3},
pages = {239--247},
title = {A new proof or Reiterman's theorem},
volume = {35},
year = {1994}
}
@article{Stoughton1988,
author = {Stoughton, Allen},
doi = {10.1016/0304-3975(88)90149-1},
issn = {03043975},
journal = {Theor. Comput. Sci.},
month = aug,
number = {3},
pages = {317--325},
title = {Substitution revisited},
volume = {59},
year = {1988}
}
@article{Plotkin2003,
author = {Plotkin, Gordon D. and Power, A. John},
doi = {10.1023/A:1023064908962},
journal = {Appl. Categ. Struct.},
keywords = {algebraic operation,computational effect,lawvere theory,monad},
number = {1},
pages = {69--94},
publisher = {Kluwer Academic Publishers},
title = {Algebraic Operations and Generic Effects},
volume = {11},
year = {2003}
}
@article{Foulis1994,
abstract = {The effects in a quantum-mechanical system form a partial algebra and a partially ordered set which is the prototypical example of the effect algebras discussed in this paper. The relationships among effect algebras and such structures as orthoalgebras and orthomodular posets are investigated, as are morphisms and group- valued measures (or charges) on effect algebras. It is proved that there is a universal group for every effect algebra, as well as a universal vector space over an arbitrary field.},
author = {Foulis, D. J. and Bennett, M. K.},
doi = {10.1007/BF02283036},
issn = {0015-9018},
journal = {Found. Phys.},
month = oct,
number = {10},
pages = {1331--1352},
title = {Effect algebras and unsharp quantum logics},
volume = {24},
year = {1994}
}
@article{Ohearn1995,
author = {O'Hearn, Peter W. and Riecke, Jon G.},
doi = {10.1006/inco.1995.1103},
issn = {08905401},
journal = {Inf. Comput.},
month = jul,
number = {1},
pages = {107--116},
title = {Kripke Logical Relations and PCF},
volume = {120},
year = {1995}
}
@article{Sano2011,
author = {Sano, Katsuhiko},
doi = {10.1016/j.entcs.2011.06.012},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {frames,hybrid logic,monotone neighborhood,product of neighborhood frames,product of topologies,pure completeness},
month = jul,
pages = {51--67},
publisher = {Elsevier B.V.},
title = {Axiomatizing Hybrid Products of Monotone Neighborhood Frames},
volume = {273},
year = {2011}
}
@inproceedings{Heunen2017,
abstract = {Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed. Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.},
archivePrefix = {arXiv},
arxivId = {1701.02547},
author = {Heunen, Chris and Kammar, Ohad and Staton, Sam and Yang, Hongseok},
booktitle = {2017 32nd Annu. ACM/IEEE Symp. Log. Comput. Sci.},
doi = {10.1109/LICS.2017.8005137},
eprint = {1701.02547},
isbn = {978-1-5090-3018-7},
issn = {10436871},
month = jun,
pages = {1--12},
publisher = {IEEE},
title = {A convenient category for higher-order probability theory},
year = {2017}
}
@article{Jung2001,
abstract = {Stably compact spaces are a natural generalization of compact Hausdorff spaces in the T0 setting. They have been studied intensively by a number of researchers and from a variety of standpoints. In this paper we let the morphisms between stably compact spaces be certain ``closed relations'' and study the resulting categorical properties. Apart from extending ordinary continuous maps, these morphisms have a number of pleasing properties, the most prominent, perhaps, being that they correspond to preframe homomorphisms on the localic side. We exploit this Stone-type duality to establish that the category of stably compact spaces and closed relations has bilimits.},
author = {Jung, Achim and Kegelmann, Mathias and Moshier, M. Andrew},
doi = {10.1016/S1571-0661(04)80964-2},
issn = {1571-0661},
journal = {Electron. Notes Theor. Comput. Sci.},
number = {0},
pages = {209--231},
title = {Stably compact spaces and closed relations},
type = {Journal article},
volume = {45},
year = {2001}
}
@article{Coecke2012,
abstract = {We introduce a graphical framework for Bayesian inference that is sufficiently general to accommodate not just the standard case but also recent proposals for a theory of quantum Bayesian inference wherein one considers density operators rather than probability distributions as representative of degrees of belief. The diagrammatic framework is stated in the graphical language of symmetric monoidal categories and of compact structures and Frobenius structures therein, in which Bayesian inversion boils down to transposition with respect to an appropriate compact structure. We characterize classical Bayesian inference in terms of a graphical property and demonstrate that our approach eliminates some purely conventional elements that appear in common representations thereof, such as whether degrees of belief are represented by probabilities or entropic quantities. We also introduce a quantum-like calculus wherein the Frobenius structure is noncommutative and show that it can accommodate Leifer's calculus of ‘conditional density operators'. The notion of conditional independence is also generalized to our graphical setting and we make some preliminary connections to the theory of Bayesian networks. Finally, we demonstrate how to construct a graphical Bayesian calculus within any dagger compact category.},
archivePrefix = {arXiv},
arxivId = {1102.2368},
author = {Coecke, Bob and Spekkens, Robert W.},
doi = {10.1007/s11229-011-9917-5},
eprint = {1102.2368},
issn = {00397857},
journal = {Synthese},
keywords = {Bayesian inference,Conditional density operator,Frobenius algebra,Graphical calculus,Symmetric monoidal category},
number = {3},
pages = {651--696},
title = {Picturing classical and quantum Bayesian inference},
volume = {186},
year = {2012}
}
@article{Weil2002,
author = {Weil, Pascal},
doi = {10.1142/S0218196702000912},
issn = {0218-1967},
journal = {Int. J. Algebra Comput.},
month = feb,
number = {01n02},
pages = {137--178},
title = {Profinite methods in semigroup theory},
volume = {12},
year = {2002}
}
@incollection{Schroder2007b,
author = {Schr{\"{o}}der, Lutz and Pattinson, Dirk},
booktitle = {Autom. Lang. Program.},
doi = {10.1007/978-3-540-73420-8_41},
editor = {Schr{\"{o}}der, Lutz and Pattinson, Dirk},
pages = {1--12},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Modular algorithms for heterogeneous modal logics},
year = {2007}
}
@article{Pearl1992,
abstract = {An earlier position paper has examined the applicability of belief-functions methodology in three reasoning tasks: (1) representation of incomplete knowledge, (2) belief-updating, and (3) evidence pooling. My conclusions were that the use of belief functions encounters basic difficulties along all three tasks, and that extensive experimental and theoretical studies should be undertaken before belief functions could be applied safely. This article responds to the discussion, in this issue, of my conclusions and the degree to which they affect the applicability of belief functions in automated reasoning tasks. {\textcopyright} 1992.},
author = {Pearl, Judea},
doi = {10.1016/0888-613X(90)90013-R},
isbn = {0888-613X},
issn = {0888613X},
journal = {Int. J. Approx. Reason.},
keywords = {Belief functions,Dempster-Shafer theory,conditional information,knowledge representation nonmonotonic reasoning},
month = sep,
number = {5-6},
pages = {363--389},
title = {Reasoning with belief functions: An analysis of compatibility},
volume = {4},
year = {1990}
}
@article{Adamek2013,
abstract = {Continuous lattices were characterised by Martin Escardo as precisely the objects that are Kan-injective w.r.t. a certain class of morphisms. We study Kan-injectivity in general categories enriched in posets. For every class H of morphisms we study the subcategory of all objects Kan-injective w.r.t. H and all morphisms preserving Kan-extensions. For categories such as Top_0 and Pos we prove that whenever H is a set of morphisms, the above subcategory is monadic, and the monad it creates is a Kock-Zoeberlein monad. However, this does not generalise to proper classes: we present a class of continuous mappings in Top_0 for which Kan-injectivity does not yield a monadic category.},
archivePrefix = {arXiv},
arxivId = {1311.1721},
author = {Ad{\'{a}}mek, Jiř{\'{i}} and Sousa, Lurdes and Velebil, Jiř{\'{i}}},
doi = {10.1017/S0960129514000024},
eprint = {1311.1721},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
number = {01},
pages = {6--45},
title = {Kan injectivity in order-enriched categories},
volume = {25},
year = {2015}
}
@phdthesis{Zanasi2015,
archivePrefix = {arXiv},
arxivId = {1403.7048},
author = {Zanasi, Fabio},
eprint = {1403.7048},
keywords = {distributive law,frobenius algebra,hopf algebra,linear algebra,prop,string diagram},
school = {Universit{\'{e}} de Lyon},
title = {Interacting Hopf Algebras},
year = {2015}
}
@article{Tanaka2006,
author = {Tanaka, Miki and Power, A. John},
doi = {10.1007/s10990-006-8750-x},
issn = {1388-3690},
journal = {Higher-Order Symb. Comput.},
keywords = {binding signatures,context,initial algebra semantics,pseudo-distributive law,pseudo-monad,substitution monoidal structure},
month = sep,
number = {2-3},
pages = {305--337},
title = {Pseudo-distributive laws and axiomatics for variable binding},
volume = {19},
year = {2006}
}
@article{Davey2015,
abstract = {We clarify what it means for two full dualities based on the same algebra to be different. Our main theorem gives conditions on two different alter egos of a finite algebra under which, if one yields a full duality, then the other does too. We use this theorem to obtain a better understanding of several important examples from the theory of natural dualities. Throughout the paper, a fundamental role is played by the universal Horn theory of the dual classes.},
archivePrefix = {arXiv},
arxivId = {1511.03001},
author = {Davey, Brian A. and Pitkethly, Jane G. and Willard, Ross},
eprint = {1511.03001},
pages = {1--25},
title = {New-from-old full dualities via axiomatisation},
year = {2015}
}
@article{Heunen2009,
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 = jul,
number = {1},
pages = {63--110},
title = {A topos for algebraic quantum theory},
volume = {291},
year = {2009}
}
@article{Danos2006,
author = {Danos, Vincent and Desharnais, Jos{\'{e}}e and Laviolette, Fran{\c{c}}ois and Panangaden, Prakash},
doi = {10.1016/j.ic.2005.02.004},
issn = {08905401},
journal = {Inf. Comput.},
month = apr,
number = {4},
pages = {503--523},
title = {Bisimulation and cocongruence for probabilistic systems},
volume = {204},
year = {2006}
}
@article{Cancila2004,
author = {Cancila, Daniela and Honsell, Furio and Lenisa, Marina},
doi = {10.1016/j.entcs.2004.08.019},
issn = {15710661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {categories of sets,constant functor,identity functor,partially defined endofunctors},
month = nov,
pages = {61--80},
title = {Properties of Set Functors},
volume = {104},
year = {2004}
}
@techreport{Preston2008,
abstract = {These notes give an elementary approach to parts of the theory of standard Borel and analytic spaces.},
archivePrefix = {arXiv},
arxivId = {0809.3066},
author = {Preston, Chris},
eprint = {0809.3066},
month = sep,
title = {Some Notes on Standard Borel and Related Spaces},
year = {2008}
}
@article{Sweeney2002,
author = {Sweeney, Latanya},
doi = {10.1142/S021848850200165X},
journal = {Int. J. Uncertainty, Fuzziness Knowledge-Based Syst.},
keywords = {data anonymity,data fusion,data privacy,privacy,re-identification},
month = oct,
number = {05},
pages = {571--588},
title = {Achieving $k$-anonymity privacy protection using generalization and suppression},
volume = {10},
year = {2002}
}
@book{Kelly1982,
author = {Kelly, Gregory Maxwell},
booktitle = {Theory Appl. Categ.},
number = {10},
publisher = {Cambridge Univ Pr},
series = {Lecture Notes in Mathematics},
title = {Basic Concepts of Enriched Category Theory},
volume = {64},
year = {1982}
}
@article{Chen2011,
author = {Chen, Rui and Mohammed, Noman and Fung, Benjamin Cm and Desai, Bipin C. and Xiong, Li},
issn = {21508097},
journal = {Proc. VLDB Endow.},
number = {11},
pages = {1087--1098},
title = {Publishing set-valued data via differential privacy},
volume = {4},
year = {2011}
}
@article{Narens2016,
abstract = {The focus of this article is on probability theories based on non-boolean event spaces that have potential for scientific and philosophical applications. Since the early 1930s, such an alternative probability theory has been systematically used to provide a mathematical foundation for quantum physics. This article investigates in a general way feasible alternatives to boolean event algebras as bases for probability theories. Such alternatives permit new kinds of logical relationships among events that are not expressible in boolean event algebras. In psychology, these relationships allow for kinds of modeling methods that help account for various puzzling phenomena found throughout psychology, particularly in cognitive decision theory. The alternative probability theories presented are investigated through algebraic characterizations of their event spaces and probability functions. This is done using results from a well-developed area of mathematics known as “lattice theory”. This article describes the basics of lattice theory and how the interpretation of a few of its results indicates that generalizations of boolean event spaces are severely limited for useful application in scientific modeling. The overall conclusion is that two types of event spaces appear especially promising for generalization: One that captures key concepts of the logic inherent in quantum mechanics, “quantum logic”, and another that captures key concepts inherent in a generalization of classical logic that is used in the foundations of mathematics, “intuitionistic logic”. Both of these types of logical structures are useful for constructing unorthodox models of troublesome findings in behavioral economics. One theme of this article is the use of intuitionistic logic to model probabilistic judgments and decision making.},
author = {Narens, Louis},
doi = {10.1016/j.jmp.2016.04.013},
issn = {00222496},
journal = {J. Math. Psychol.},
keywords = {Foundations of probability,Intuitionistic logic,Lattice theory,Quantum probability theory},
month = oct,
pages = {66--81},
publisher = {Elsevier Inc.},
title = {An introduction to lattice based probability theories},
volume = {74},
year = {2016}
}
@article{Speed1972,
author = {Speed, T.P.},
doi = {10.1017/S0004972700044415},
issn = {0004-9727},
journal = {Bull. Aust. Math. Soc.},
pages = {177},
title = {Profinite posets},
volume = {6},
year = {1972}
}
@unpublished{Altenkirch,
author = {Altenkirch, Thorsten and Anberr{\'{e}}e, Thomas and Li, Nuo},
title = {Definable Quotients in Type Theory},
year = {2012}
}
@article{Borceux1986,
author = {Borceux, Francis and Dejean, Dominique},
journal = {Cah. Topol. G{\'{e}}om{\'{e}}trie Diff{\'{e}}rentielle Cat{\'{e}}goriques},
number = {2},
pages = {133--146},
title = {Cauchy completion in category theory},
volume = {27},
year = {1986}
}
@inproceedings{Wilke1991,
author = {Wilke, Thomas},
booktitle = {Autom. Lang. Program. 18th Colloquium, Madrid, Spain, July 8–12, 1991 Proc.},
doi = {10.1007/3-540-54233-7_166},
editor = {Albert, Javier Leach and Monien, Burkhard and Artalejo, Mario Rodr{\'{i}}guez},
pages = {588--599},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {An EILENBERG theorem for ∞-languages},
year = {1991}
}
@article{Bartels2004,
author = {Bartels, Falk and Sokolova, Ana and de Vink, Erik P.},
doi = {10.1016/j.tcs.2004.07.019},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {bisimulation,coalgebra,cocongruence,preservation and reflection of,probabilistic bisimulation,probabilistic transition systems},
month = oct,
number = {1-2},
pages = {3--22},
title = {A hierarchy of probabilistic system types},
volume = {327},
year = {2004}
}
@incollection{Kelly1974b,
author = {Kelly, Gregory Maxwell},
booktitle = {Categ. Semin.},
doi = {10.1007/BFb0063106},
editor = {Kelly, Gregory Maxwell},
pages = {281--375},
publisher = {Springer, Berlin, Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Coherence theorems for lax algebras and for distributive laws},
volume = {420},
year = {1974}
}
@book{Gray1974,
author = {Gray, John W.},
doi = {10.1007/BFb0061280},
isbn = {978-3-540-06830-3},
issn = {0075-8434},
pages = {284},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Mathematics},
title = {Formal Category Theory: Adjointness for 2-Categories},
volume = {391},
year = {1974}
}
@article{Bou2008,
abstract = {This paper deals with many-valued modal logics, based only on the necessity operator, over a residuated lattice. We focus on three basic classes, according to the accessibility relation, of Kripke frames: the full class of frames evaluated in the residuated lattice (and so defining the minimum modal logic), the ones evaluated in the idempotent elements and the ones evaluated in 0 and 1. We show how to expand an axiomatization, with canonical constants in the language, of a finite residuated lattice into one of the modal logic, for each one of the three basic classes of Kripke frames, over the very lattice. And we also give axiomatizations for the case of a finite MV chain but this time without canonical constants.},
archivePrefix = {arXiv},
arxivId = {0811.2107},
author = {Bou, F{\'{e}}lix Felix and Esteva, Francesc and Godo, Llu{\'{i}}s Lluis and Rodriguez, Ricardo O.},
doi = {10.1093/logcom/exp062},
eprint = {0811.2107},
issn = {0955-792X},
journal = {J. Log. Comput.},
keywords = {fuzzy logic,many-valued logic,many-valued modal logic,modal logic,substructural logic},
month = nov,
number = {5},
pages = {1--53},
title = {On the Minimum Many-Valued Modal Logic over a Finite Residuated Lattice},
volume = {21},
year = {2008}
}
@article{Abadi1997,
address = {New York, New York, USA},
author = {Abadi, Martı́n and Gordon, Andrew D.},
doi = {10.1006/inco.1998.2740},
isbn = {0897919122},
issn = {08905401},
journal = {Inf. Comput.},
month = jan,
number = {1},
pages = {1--70},
publisher = {ACM Press},
title = {A calculus for cryptographic protocols: the Spi calculus},
volume = {148},
year = {1999}
}
@inproceedings{Ben-Sasson2014,
abstract = {We build a system that provides succinct non-interactive zero-knowledge proofs (zk-SNARKs) for program executions on a von Neumann RISC architecture. The system has two components: a cryptographic proof system for verifying satisfiability of arithmetic circuits, and a circuit generator to translate program executions to such circuits. Our design of both components improves in functionality and efficiency over prior work, as follows.Our circuit generator is the first to be universal: it does not need to know the program, but only a bound on its running time. Moreover, the size of the output circuit depends additively (rather than multiplicatively) on program size, allowing verification of larger programs.The cryptographic proof system improves proving and verification times, by leveraging new algorithms and a pairing library tailored to the protocol.We evaluated our system for programs with up to 10,000 instructions, running for up to 32,000 machine steps, each of which can arbitrarily access random-access memory; and also demonstrated it executing programs that use just-in-time compilation. Our proofs are 230 bytes long at 80 bits of security, or 288 bytes long at 128 bits of security. Typical verification time is 5 milliseconds, regardless of the original program's running time.},
author = {Ben-Sasson, Eli and Chiesa, Alessandro and Tromer, Eran and Virza, Madars},
booktitle = {Proc. 23rd {USENIX} Secur. Symp.},
isbn = {9781931971157},
keywords = {computationally-sound proofs,succinct arguments,zero-knowledge},
pages = {781--796},
publisher = {{USENIX} Association},
title = {Succinct Non-Interactive Zero Knowledge for a von Neumann Architecture},
year = {2014}
}
@article{Dwork2008c,
abstract = {In 1977 Tore Dalenius articulated a desideratum for statistical databases: nothing about an individual should be learnable from the database that cannot be learned without access to the database. We give a general impossibility result showing that a natural formalization of Dalenius goal cannot be achieved if the database is useful. The key obstacle is the side information that may be available to an adversary. Our results hold under very general conditions regarding the database, the notion of privacy violation, and the notion of utility. Contrary to intuition, a variant of the result threatens the privacy even of someone not in the database. This state of affairs motivated the notion of differential privacy 15, 16, a strong ad omnia privacy which, intuitively, captures the increased risk to ones privacy incurred by participating in a database. 1},
author = {Dwork, Cynthia and Naor, Moni},
journal = {J. Priv. Confidentiality},
number = {1},
pages = {93--107},
title = {On the difficulties of disclosure prevention in statistical databases or the case for differential privacy},
year = {2008}
}
@inproceedings{Zyskind2015b,
abstract = {—The recent increase in reported incidents of surveil-lance and security breaches compromising users' privacy call into question the current model, in which third-parties collect and con-trol massive amounts of personal data. Bitcoin has demonstrated in the financial space that trusted, auditable computing is possible using a decentralized network of peers accompanied by a public ledger. In this paper, we describe a decentralized personal data management system that ensures users own and control their data. We implement a protocol that turns a blockchain into an automated access-control manager that does not require trust in a third party. Unlike Bitcoin, transactions in our system are not strictly financial – they are used to carry instructions, such as storing, querying and sharing data. Finally, we discuss possible future extensions to blockchains that could harness them into a well-rounded solution for trusted computing problems in society.},
author = {Zyskind, Guy and Nathan, Oz and Pentland, Alex Sandy},
booktitle = {2015 IEEE Secur. Priv. Work.},
doi = {10.1109/SPW.2015.27},
keywords = {Bitcoin,Blockchain,Personal data,Privacy},
month = may,
pages = {180--184},
publisher = {IEEE},
title = {Decentralizing privacy: Using blockchain to protect personal data},
year = {2015}
}
@inproceedings{Kifer2011,
abstract = {Differential privacy is a powerful tool for providing privacy-preserving noisy query answers over statistical databases. It guarantees that the distribution of noisy query answers changes very little with the addition or deletion of any tuple. It is frequently accompanied by popularized claims that it provides privacy without any assumptions about the data and that it protects against attackers who know all but one record. In this paper we critically analyze the privacy protections offered by differential privacy. First, we use a no-free-lunch theorem, which defines non-privacy as a game, to argue that it is not possible to provide privacy and utility without making assumptions about how the data are generated. Then we explain where assumptions are needed. We argue that privacy of an individual is preserved when it is possible to limit the inference of an attacker about the participation of the individual in the data generating process. This is different from limiting the inference about the presence of a tuple (for example, Bob's participation in a social network may cause edges to form between pairs of his friends, so that it affects more than just the tuple labeled as "Bob"). The definition of evidence of participation, in turn, depends on how the data are generated -- this is how assumptions enter the picture. We explain these ideas using examples from social network research as well as tabular data for which deterministic statistics have been previously released. In both cases the notion of participation varies, the use of differential privacy can lead to privacy breaches, and differential privacy does not always adequately limit inference about participation.},
address = {New York, New York, USA},
author = {Kifer, Daniel and Machanavajjhala, Ashwin},
booktitle = {Proc. 2011 Int. Conf. Manag. data - SIGMOD '11},
doi = {10.1145/1989323.1989345},
isbn = {9781450306614},
issn = {07308078},
month = apr,
pages = {193},
pmid = {18450441},
publisher = {ACM Press},
title = {No free lunch in data privacy},
year = {2011}
}
@article{Bunge1974,
author = {Bunge, Marta C.},
doi = {10.1090/S0002-9947-1974-0344305-0},
issn = {0002-9947},
journal = {Trans. Am. Math. Soc.},
pages = {355--355},
title = {Coherent extensions and relational algebras},
volume = {197},
year = {1974}
}
@article{Mitchell1988,
abstract = {Abstract data type declarations appear in typed programming languages like Ada, Alphard, {CLU} and {ML.} This form of declaration binds a list of identifiers to a type with associated operations, a composite ``value'' we call a data algebra. We use a second-order typed lambda calculus {SOL} to show how data algebras may be given types, passed as parameters, and returned as results of function calls. In the process, we discuss the semantics of abstract data type declarations and review a connection between typed programming languages and constructive logic.},
author = {Mitchell, John C. and Plotkin, Gordon D.},
doi = {10.1145/44501.45065},
isbn = {0897911474},
issn = {01640925},
journal = {ACM Trans. Program. Lang. Syst.},
month = jul,
number = {3},
pages = {470--502},
title = {Abstract types have existential type},
volume = {10},
year = {1988}
}
@incollection{Bonsangue2006,
abstract = {We take the point of view that, if transition systems are coalgebras for a functor T, then an adequate logic for these transition systems should arise from the ‘Stone dual' L of T. We show that such a functor always gives rise to an ‘abstract' adequate logic for T-coalgebras and investigate under which circumstances it gives rise to a ‘concrete' such logic, that is, a logic with an inductively defined syntax and proof system. We obtain a result that allows us to prove adequateness of logics uniformly for a large number of different types of transition systems and give some examples of its usefulness.},
author = {Bonsangue, Marcello M. and Kurz, Alexander},
booktitle = {Found. Softw. Sci. Comput. Struct.},
doi = {10.1007/11690634_12},
editor = {Aceto, Luca and Ing{\'{o}}lfsd{\'{o}}ttir, Anna},
isbn = {978-3-540-33045-5},
pages = {172--186},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Presenting functors by operations and equations},
volume = {3921},
year = {2006}
}
@misc{Kock1995,
author = {Kock, Anders},
booktitle = {J. Pure Appl. Algebr.},
doi = {10.1016/0022-4049(94)00111-U},
issn = {00224049},
number = {1},
pages = {41--59},
title = {Monads for which structures are adjoint to units},
volume = {104},
year = {1995}
}
@inproceedings{Kiselyov2015,
abstract = {We present a rational reconstruction of extensible effects, the recently proposed alternative to monad transformers, as the confluence of efforts to make effectful computations compose. Free monads and then extensible effects emerge from the straightforward term representation of an effectful computation, as more and more boilerplate is abstracted away. The generalization process further leads to freer monads, constructed without the Functor constraint. The continuation exposed in freer monads can then be represented as an efficient type-aligned data structure. The end result is the algorithmically efficient extensible effects library, which is not only more comprehensible but also faster than earlier implementations. As an illustration of the new library, we show three surprisingly simple applications: non-determinism with committed choice (LogicT), catching IO exceptions in the presence of other effects, and the semi-automatic management of file handles and other resources through monadic regions. We extensively use and promote the new sort of `laziness', which underlies the left Kan extension: instead of performing an operation, keep its operands and pretend it is done.},
address = {New York, New York, USA},
author = {Kiselyov, Oleg and Ishii, Hiromi},
booktitle = {Proc. 8th ACM SIGPLAN Symp. Haskell - Haskell 2015},
doi = {10.1145/2804302.2804319},
isbn = {9781450338080},
issn = {03621340},
keywords = {coroutine,effect handler,effect interaction,free monad,kan extension,open union,type and effect system},
pages = {94--105},
publisher = {ACM Press},
title = {Freer monads, more extensible effects},
year = {2015}
}
@article{Carboni1993,
abstract = {In recent years, there has been considerable discussion as to the appropriate definition of distributive categories. Three definitions which have had some support are: (1) A category with finite sums and products such that the canonical map ??:A??B+ A??C???A??(B+C) is an isomorphism (Walters). (2) A category with finite sums and products such that the canonical functor +:A/A?? A/B???A/(A+B) is an equivalence (Monro). (3) A category with finite sums and finite limits such that the canonical functor + of (2) is an equivalence (Lawvere and Schanuel). There has been some confusion as to which of these was the natural notion to consider. This resulted from the fact that there are actually two elementary notions being combined in the above three definitions. The first, to which we give the name distributivity, is exactly that of (1). The second notion, which we shall call extensivity, is that of a category with finite sums for which the canonical functor + of definitions (2) and (3) is an equivalence. Extensivity, although it implies the existence of certain pullbacks, is essentially a property of having well-behaved sums. It is the existence of these pullbacks which has caused the confusion. The connections between definition (1) and definitions (2) and (3) are that any extensive category with products is distributive in the first sense, and that any category satisfying (3) satisfies (1) locally. The purpose of this paper is to present some basic facts about extensive and distributive categories, and to discuss the relationships between the two notions. ?? 1993.},
author = {Carboni, Aurelio and Lack, Stephen and Walters, R.F.C.},
doi = {10.1016/0022-4049(93)90035-R},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = feb,
number = {2},
pages = {145--158},
title = {Introduction to extensive and distributive categories},
volume = {84},
year = {1993}
}
@article{Kelly2004,
author = {Kelly, Gregory Maxwell and Lack, Stephen},
journal = {Fields Inst. Commun.},
pages = {319--340},
title = {Monoidal functors generated by adjunctions, with applications to transport of structure},
volume = {43},
year = {2004}
}
@incollection{Kurucz2007,
author = {Kurucz, Agi},
booktitle = {Handb. Modal Log.},
chapter = {15},
doi = {10.1016/S1570-2464(07)80018-8},
editor = {Blackburn, Patrick and Benthem, Johan Van and Wolter, Frank},
pages = {869--924},
publisher = {Elsevier},
series = {Studies in Logic and Practical Reasoning},
title = {Combining modal logics},
year = {2007}
}
@article{Myers2011,
author = {Myers, Robert Samuel Ralph},
institution = {Imperial College London},
month = oct,
pages = {287},
title = {Rational Coalgebraic Machines in Varieties : Languages, Completeness and Automatic Proofs.},
year = {2011}
}
@article{Lenisa2004,
author = {Lenisa, Marina and Power, A. John and Watanabe, Hiroshi},
doi = {10.1016/j.tcs.2004.07.024},
issn = {03043975},
journal = {Theor. Comput. Sci.},
keywords = {abstract operational semantics,distributive law,final semantics,gsos -rule,initial},
month = oct,
number = {1-2},
pages = {135--154},
title = {Category theory for operational semantics},
volume = {327},
year = {2004}
}
@article{VanBreugel2008,
abstract = {Desharnais, Gupta, Jagadeesan and Panangaden introduced a family of behavioural pseudometrics for probabilistic transition systems. These pseudometrics are a quantitative analogue of probabilistic bisimilarity. Distance zero captures probabilistic bisimilarity. Each pseudometric has a discount factor, a real number in the interval (0, 1]. The smaller the discount factor, the more the future is discounted. If the discount factor is one, then the future is not discounted at all. Desharnais et al. showed that the behavioural distances can be calculated up to any desired degree of accuracy if the discount factor is smaller than one. In this paper, we show that the distances can also be approximated if the future is not discounted. A key ingredient of our algorithm is Tarski's decision procedure for the first order theory over real closed fields. By exploiting the Kantorovich-Rubinstein duality theorem we can restrict to the existential fragment for which more efficient decision procedures exist.},
author = {van Breugel, Franck and Sharma, Babita and Worrell, James},
doi = {10.2168/LMCS-4(2:2)2008},
editor = {Seidl, Helmut},
issn = {18605974},
journal = {Log. Methods Comput. Sci.},
keywords = {and phrases,approximation algorithm,behavioural pseudometric,larity,probabilistic bisimi-,probabilistic transition system},
month = apr,
number = {2},
pages = {2},
title = {Approximating a behavioural pseudometric without discount for probabilistic systems},
volume = {4},
year = {2008}
}
@article{Pin1995,
author = {Pin, Jean-{\'{E}}ric},
journal = {Russ. Math. (Izvestija vuzov.Matematika)},
pages = {80--90},
title = {A variety theorem without complementation},
volume = {39},
year = {1995}
}
@article{Korostenski1993,
author = {Korostenski, Mareli and Tholen, Walter},
doi = {10.1016/0022-4049(93)90171-O},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = mar,
number = {1},
pages = {57--72},
title = {Factorization systems as Eilenberg-Moore algebras},
volume = {85},
year = {1993}
}
@incollection{Dwork2006,
abstract = {In 1977 Dalenius articulated a desideratum for statistical databases: nothing about an individual should be learnable from the database that cannot be learned without access to the database. We give a general impossibility result showing that a formalization of Dalenius' goal along the lines of semantic security cannot be achieved. Contrary to intuition, a variant of the result threatens the privacy even of someone not in the database. This state of affairs suggests a new measure, differential privacy, which, intuitively, captures the increased risk to one's privacy incurred by participating in a database. The techniques developed in a sequence of papers [8, 13, 3], culminating in those described in [12], can achieve any desired level of privacy under this measure. In many cases, extremely accurate information about the database can be provided while simultaneously ensuring very high levels of privacy.},
address = {Berlin, Heidelberg},
author = {Dwork, Cynthia},
booktitle = {Proc. Int. Colloq. Autom. Lang. Program. Part II},
doi = {10.1007/11787006_1},
editor = {Bugliesi, Michele and Preneel, Bart and Sassone, Vladimiro and Wegener, Ingo},
isbn = {978-3-540-35907-4},
pages = {1--12},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Differential Privacy},
volume = {4052},
year = {2006}
}
@article{Doberkat2011,
author = {Doberkat, Ernst-Erich and Schubert, Christoph},
doi = {10.1017/S0960129510000526},
issn = {0960-1295},
journal = {Math. Struct. Comput. Sci.},
month = mar,
number = {02},
pages = {175--234},
title = {Coalgebraic logic over general measurable spaces–--a survey},
volume = {21},
year = {2011}
}
@incollection{Gibbons2016,
author = {Gibbons, Jeremy},
booktitle = {A List Successes That Can Chang. World Essays Dedic. to Philip Wadler Occas. His 60th Birthd.},
doi = {10.1007/978-3-319-30936-1_7},
editor = {Lindley, Sam and McBride, Conor and Trinder, Phil and Sannella, Don},
pages = {132--151},
publisher = {Springer International Publishing},
series = {Lecture Notes in Computer Science},
title = {Comprehending Ringads},
year = {2016}
}
@article{Gehrke2014a,
abstract = {Our main result is that any topological algebra based on a Boolean space is the extended Stone dual space of a certain associated Boolean algebra with additional operations. A particular case of this result is that the profinite completion of any abstract algebra is the extended Stone dual space of the Boolean algebra of recognisable subsets of the abstract algebra endowed with certain residuation operations. These results identify a connection between topological algebra as applied in algebra and Stone duality as applied in logic, and show that the notion of recognition originating in computer science is intrinsic to profinite completion in mathematics in general. This connection underlies a number of recent results in automata theory including a generalisation of Eilenberg-Reiterman theory for regular languages and a new notion of compact recognition applicable beyond the setting of regular languages. The purpose of this paper is to give the underlying duality theoretic result in its general form. Further we illustrate the power of the result by providing a few applications in topological algebra and language theory. In particular, we give a simple proof of the fact that any topological algebra quotient of a profinite algebra which is again based on a Boolean space is again profinite and we derive the conditions dual to the ones of the original Eilenberg theorem in a fully modular manner. We cast our results in the setting of extended Priestley duality for distributive lattices with additional operations as some classes of languages of interest in automata theory fail to be closed under complementation.},
archivePrefix = {arXiv},
arxivId = {1309.2422},
author = {Gehrke, Mai},
doi = {10.1016/j.jpaa.2015.12.007},
eprint = {1309.2422},
issn = {00224049},
journal = {J. Pure Appl. Algebr.},
month = jul,
number = {7},
pages = {2711--2747},
publisher = {Elsevier B.V.},
title = {Stone duality, topological algebra, and recognition},
volume = {220},
year = {2016}
}
@phdthesis{Oliveira2014,
author = {de Oliveira, Henrique Roscoe},
number = {June},
school = {Northwestern University},
title = {Attention and Information Acquisition},
year = {2014}
}
@article{Carayol2017,
author = {Carayol, Arnaud and {\'{E}}sik, Zolt{\'{a}}n},
doi = {10.1016/j.jlamp.2016.09.004},
issn = {23522208},
journal = {J. Log. Algebr. Methods Program.},
number = {1},
pages = {308--318},
publisher = {Elsevier Inc.},
title = {An analysis of the equational properties of the well-founded fixed point},
volume = {86},
year = {2017}
}
@inproceedings{Cheng2003,
author = {Cheng, Eugenia and Hyland, Martin and Power, A. John},
booktitle = {Proc. 19th Conf. Math. Found. Program. Semant.},
doi = {10.1016/S1571-0661(03)50012-3},
issn = {15710661},
pages = {227--245},
publisher = {Elsevier Masson SAS},
title = {Pseudo-distributive Laws},
volume = {83},
year = {2003}
}
@article{Winograd-Cort2017,
abstract = {Differential privacy is a widely studied theory for analyzing sensitive data with a strong privacy guaranteeÐ any change in an individual's data can have only a small statistical effect on the resultÐand a growing number of programming languages now support differentially private data analysis. A common shortcoming of these languages is poor support for adaptivity. In practice, a data analyst rarely wants to run just one function over a sensitive database, nor even a predetermined sequence of functions with fixed privacy parameters; rather, she wants to engage in an interaction where, at each step, both the choice of the next function and its privacy parameters are informed by the results of prior functions. Existing languages support this scenario using a simple composition theorem, which often gives rather loose bounds on the actual privacy cost of composite functions, substantially reducing how much computation can be performed within a given privacy budget. The theory of differential privacy includes other theorems with much better bounds, but these have not yet been incorporated into programming languages. We propose a novel framework for adaptive composition that is elegant, practical, and implementable. It consists of a reformulation based on typed functional programming of privacy filters, together with a concrete realization of this framework in the design and implementation of a new language, called Adaptive Fuzz. Adaptive Fuzz transplants the core static type system of Fuzz to the adaptive setting by wrapping the Fuzz typechecker and runtime system in an outer adaptive layer, allowing Fuzz programs to be conveniently constructed and typechecked on the fly. We describe an interpreter for Adaptive Fuzz and report results from two case studies demonstrating its effectiveness for implementing common statistical algorithms over real data sets.},
author = {Winograd-Cort, Daniel and Haeberlen, Andreas and Roth, Aaron and Pierce, Benjamin C},
doi = {10.1145/3110254},
issn = {24751421},
journal = {Proc. ACM Program. Lang.},
keywords = {Adaptivity,Case Study,Differential Privacy,Fuzz,Privacy Filter},
month = aug,
number = {ICFP},
pages = {1--29},
title = {A framework for adaptive differential privacy},
volume = {1},
year = {2017}
}
@article{Sabelfeld2003,
abstract = {Current standard security practices do not provide substantial assurance that the end-to-end behavior of a computing system satisfies important security policies such as confidentiality. An end-to-end confidentiality policy might assert that secret input data cannot be inferred by an attacker through the attacker's observations of system output; this policy regulates information flow. Conventional security mechanisms such as access control and encryption do not directly address the enforcement of information-flow policies. Previously, a promising new approach has been developed: the use of programming-language techniques for specifying and enforcing information-flow policies. In this paper, we survey the past three decades of research on information-flow security, particularly focusing on work that uses static program analysis to enforce information-flow policies. We give a structured view of work in the area and identify some important open challenges.},
author = {Sabelfeld, Andrei and Myers, A.C.},
doi = {10.1109/JSAC.2002.806121},
isbn = {0733-8716},
issn = {0733-8716},
journal = {IEEE J. Sel. Areas Commun.},
keywords = {Computer security,Concurrency,Confidentiality,Covert channels,Information flow,Noninterference,Security policies,Security-type systems},
month = jan,
number = {1},
pages = {5--19},
title = {Language-based information-flow security},
volume = {21},
year = {2003}
}
@article{Yang2017,
abstract = {Ever since proposed by Dwork, differential privacy has been a hot topic in academia. However, few attempts have been made on reasoning about differential privacy at a system level. In this paper, we propose a formal framework to verify differential privacy in probabilistic systems. With a metric on the states of a system, we formalize differential privacy by the ratio of the probabilities in the distributions after the same labeled transitions of relevant states. We explain how traditional differential privacy can be embedded in our framework and raise an infimum metric, the least distance between two states, while not violating differential privacy. It is proven that the infimum metric is also a metric instance of differential privacy itself. Furthermore, we propose a two-level logic, a privacy variant of the familiar Hennessy–Milner logic, to characterize differential privacy in our framework. Our results have close relations to probabilistic bisimilarity as well.},
author = {Yang, Jiannan and Cao, Yongzhi and Wang, Hanpin},
doi = {10.1016/j.ic.2017.03.002},
issn = {08905401},
journal = {Inf. Comput.},
keywords = {Differential privacy,Logical characterization,Metric,Probabilistic bisimilarity,Probabilistic system},
month = jun,
pages = {84--104},
publisher = {Elsevier Inc.},
title = {Differential privacy in probabilistic systems},
volume = {254},
year = {2017}
}
@incollection{Sestoft2002,
abstract = {We describe lambda calculus reduction strategies using big-step operational semantics and show how to efficiently trace such reductions. This is used in a web-based lambda calculus reducer, at http://www.dina.kvl.dk/$\sim$sestoft/lamreduce/ . ?? 2001 Published by Elsevier Science B.V.},
author = {Sestoft, Peter},
booktitle = {Essence Comput. Complexity, Anal. Transform.},
doi = {10.1007/3-540-36377-7_19},
editor = {Mogensen, Torben {\AE}. and Schmidt, David A. and Sudborough, I. Hal},
isbn = {9783540003267},
issn = {15710661},
pages = {420--435},
publisher = {Springer Berlin Heidelberg},
series = {Lecture Notes in Computer Science},
title = {Demonstrating lambda calculus reduction},

repository: anqurvanillapy/Type-Theory

repo_name: anqurvanillapy/Type-Theory