Zobrazeno 1 - 10
of 20
pro vyhledávání: '"Emilio Jesús Gallego Arias"'
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 239, Iss Proc. UITP 2016, Pp 15-27 (2017)
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 ext
Externí odkaz:
https://doaj.org/article/c0d0e65544174445867f27afe7ae70a6
Publikováno v:
The Journal of Privacy and Confidentiality, Vol 7, Iss 2 (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:
https://doaj.org/article/8061ee11d63245759d4f0645c1680942
Publikováno v:
FARM 2021: Proceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design
FARM 2021-9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design
FARM 2021-9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design, Aug 2021, Virtual, South Korea. ⟨10.1145/3471872.3472970⟩
FARM@ICFP
FARM 2021-9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design
FARM 2021-9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design, Aug 2021, Virtual, South Korea. ⟨10.1145/3471872.3472970⟩
FARM@ICFP
International audience; We introduce the W-calculus, an extension of the call-byvalue λ-calculus with synchronous semantics, designed to be flexible enough to capture different implementation forms of Digital Signal Processing algorithms, while perm
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1ccce05eed81a8c216573eefcbcbf90f
https://mines-paristech.hal.science/hal-03322174v2/file/A-755-v2.pdf
https://mines-paristech.hal.science/hal-03322174v2/file/A-755-v2.pdf
Publikováno v:
ICSE (Companion Volume)
Software developed and verified using proof assistants, such as Coq, can provide trustworthiness beyond that of software developed using traditional programming languages and testing practices. However, guarantees from formal verification are only as
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4c59614fc58167d3306ef839dd2559b9
https://doi.org/10.1145/3377812.3382156
https://doi.org/10.1145/3377812.3382156
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 239, Iss Proc. UITP 2016, Pp 15-27 (2017)
12th International Workshop on User Interfaces for Theorem Provers (UITP '16)
12th International Workshop on User Interfaces for Theorem Provers (UITP '16), Jul 2016, Coimbra, Portugal. pp.15-27, ⟨10.4204/EPTCS.239.2⟩
UITP
12th International Workshop on User Interfaces for Theorem Provers (UITP '16)
12th International Workshop on User Interfaces for Theorem Provers (UITP '16), Jul 2016, Coimbra, Portugal. pp.15-27, ⟨10.4204/EPTCS.239.2⟩
UITP
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:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a12d7b305d4fbed732514948d6c384bb
https://doaj.org/article/c0d0e65544174445867f27afe7ae70a6
https://doaj.org/article/c0d0e65544174445867f27afe7ae70a6
Publikováno v:
34th International Conference on Automated Software Engineering (ASE 2019
34th International Conference on Automated Software Engineering (ASE 2019, Nov 2019, San Diego, United States
ASE
34th International Conference on Automated Software Engineering (ASE 2019, Nov 2019, San Diego, United States
ASE
International audience; Mutation analysis, which introduces artificial defects into software systems, is the basis of mutation testing, a technique widely applied to evaluate and enhance the quality of test suites. However, despite the deep analogy b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a87d60e298025a501d499572d457b2c5
https://hal-mines-paristech.archives-ouvertes.fr/hal-02434236/document
https://hal-mines-paristech.archives-ouvertes.fr/hal-02434236/document
Publikováno v:
Theory and Practice of Logic Programming
Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2018, 34th International Conference on Logic Programming, 18 (3-4), pp.372-389. ⟨10.1017/S1471068418000224⟩
Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2018, 34th International Conference on Logic Programming, 18 (3-4), pp.372-389. ⟨10.1017/S1471068418000224⟩
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:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b089ccaade25b47d1c693818178b3fbb
https://hal.archives-ouvertes.fr/hal-01932818
https://hal.archives-ouvertes.fr/hal-01932818
Autor:
Gilles Barthe, Pierre-Yves Strub, Emilio Jesús Gallego Arias, Andrew D. Gordon, Marco Gaboardi, Gian Pietro Farina, Justin Hsu
Publikováno v:
The 23rd ACM Conference on Computer and Communications Security
The 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienne, Austria. pp.68-79 ⟨10.1145/2976749.2978371⟩
Barthe, G, Farina, G P, Gaboardi, M, Arias, E J G, Gordon, A, Hsu, J & Strub, P-Y 2016, Differentially Private Bayesian Programming . in 23rd ACM Conference on Computer and Communications Security CCS 2016 . pp. 68-79, 23rd ACM Conference on Computer and Communications Security, Vienna, Austria, 24/10/16 . https://doi.org/10.1145/2976749.2978371
The 23rd ACM Conference on Computer and Communications Security, Oct 2016, Vienne, Austria. pp.68-79 ⟨10.1145/2976749.2978371⟩
Barthe, G, Farina, G P, Gaboardi, M, Arias, E J G, Gordon, A, Hsu, J & Strub, P-Y 2016, Differentially Private Bayesian Programming . in 23rd ACM Conference on Computer and Communications Security CCS 2016 . pp. 68-79, 23rd ACM Conference on Computer and Communications Security, Vienna, Austria, 24/10/16 . https://doi.org/10.1145/2976749.2978371
International audience; 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 wit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b84206a0304c86f3839cdc1ee3e6524f
https://doi.org/10.1145/2976749.2978371
https://doi.org/10.1145/2976749.2978371
Publikováno v:
Formal Aspects of Computing
Formal Aspects of Computing, Springer Verlag, 2016, 29 (Issue 1), pp.97-124. ⟨10.1007/s00165-016-0369-z⟩
Formal Aspects of Computing, Springer Verlag, 2016, 29 (Issue 1), pp.97-124. ⟨10.1007/s00165-016-0369-z⟩
We present a declarative framework for the compilation of constraint logic programs into variable-free relational theories which are then executed by rewriting. This translation provides an algebraic formulation of the abstract syntax of logic progra
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d8189956ecb007ac95428a301f91ca4b
https://hal-mines-paristech.archives-ouvertes.fr/hal-01433373
https://hal-mines-paristech.archives-ouvertes.fr/hal-01433373
Publikováno v:
Logic Journal of IGPL. 19:790-820
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0fa0c4d575d924f697a62c235a861ea0
https://doi.org/10.1093/jigpal/jzq011
https://doi.org/10.1093/jigpal/jzq011