activity
20132018
most citedjsCoq: Towards Hybrid Theorem Proving Interfaces

15 citations · 29 across the 3 of their papers we have counts for

collaborators

5 papers

cs.DB2018

Certified Graph View Maintenance with Regular Datalog

Angela Bonifati, Stefania Dumbrava, Emilio Jesus Gallego Arias

We employ the Coq proof assistant to develop a mechanically-certified framework for evaluating graph queries and incrementally maintaining materialized graph instances, also called…

cs.PL2017★ 15 cited

jsCoq: Towards Hybrid Theorem Proving Interfaces

Emilio Jesús Gallego Arias, Benoît Pin, Pierre Jouvelot

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 typical…

cs.GT2015★ 14 cited

Computer-aided verification in mechanism design

Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias +3

In mechanism design, the gold standard solution concepts are dominant strategy incentive compatibility and Bayesian incentive compatibility. These solution concepts relieve the (po…

cs.DS2014

Dual Query: Practical Private Query Release for High Dimensional Data

Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu +2

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 h…

cs.PL2013

The Ciao clp(FD) Library. A Modular CLP Extension for Prolog

Emilio Jesús Gallego Arias, Rémy Haemmerlé, Manuel V. Hermenegildo +1

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 C…