Zobrazeno 1 - 10
of 17
pro vyhledávání: '"Arias, Emilio Jesús Gallego"'
We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called views. The language we use for defining queries and views is Regular
Externí odkaz:
http://arxiv.org/abs/1804.10565
Publikováno v:
EPTCS 239, 2017, pp. 15-27
We describe jsCcoq, a new platform and user environment for the Coq interactive proof assistant. The jsCoq system targets the HTML5-ECMAScript 2015 specification, and it is typically run inside a standards-compliant browser, without the need of exter
Externí odkaz:
http://arxiv.org/abs/1701.07125
Autor:
Barthe, Gilles, Farina, Gian Pietro, Gaboardi, Marco, Arias, Emilio Jesùs Gallego, Gordon, Andy, Hsu, Justin, Strub, Pierre-Yves
We present PrivInfer, an expressive framework for writing and verifying differentially private Bayesian machine learning algorithms. Programs in PrivInfer are written in a rich functional probabilistic programming language with constructs for perform
Externí odkaz:
http://arxiv.org/abs/1605.00283
Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfull
Externí odkaz:
http://arxiv.org/abs/1503.04522
Autor:
Barthe, Gilles, Gaboardi, Marco, Arias, Emilio Jesús Gallego, Hsu, Justin, Roth, Aaron, Strub, Pierre-Yves
In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (possibly unsophisticated) bidders from the need to engage in complicated
Externí odkaz:
http://arxiv.org/abs/1502.04052
Autor:
Barthe, Gilles, Gaboardi, Marco, Arias, Emilio Jesús Gallego, Hsu, Justin, Roth, Aaron, Strub, Pierre-Yves
Mechanism design is the study of algorithm design in which the inputs to the algorithm are controlled by strategic agents, who must be incentivized to faithfully report them. Unlike typical programmatic properties, it is not sufficient for algorithms
Externí odkaz:
http://arxiv.org/abs/1407.6845
Autor:
Barthe, Gilles, Gaboardi, Marco, Arias, Emilio Jesús Gallego, Hsu, Justin, Kunz, César, Strub, Pierre-Yves
Differential privacy is a rigorous, worst-case notion of privacy-preserving computation. Informally, a probabilistic program is differentially private if the participation of a single individual in the input database has a limited effect on the progr
Externí odkaz:
http://arxiv.org/abs/1407.2988
Publikováno v:
Journal of Privacy and Confidentiality 7(2) 53--77 (2017)
We present a practical, differentially private algorithm for answering a large number of queries on high dimensional datasets. Like all algorithms for this task, ours necessarily has worst-case complexity exponential in the dimension of the data. How
Externí odkaz:
http://arxiv.org/abs/1402.1526
We present a new free library for Constraint Logic Programming over Finite Domains, included with the Ciao Prolog system. The library is entirely written in Prolog, leveraging on Ciao's module system and code transformation capabilities in order to a
Externí odkaz:
http://arxiv.org/abs/1301.7702
Publikováno v:
Logic Journal of the IGPL. Dec2011, Vol. 19 Issue 6, p790-820. 31p.
