An overview of the Sloth2005 curry system: system description. - Emilio Jesús Gallego Arias; Julio Mariño (WCFLP, 2005)

A Proposal for Disequality Constraints in Curry. - Emilio Jesús Gallego Arias; Julio Mariño-Carballo; José María Rey Poza (WFLP, 2006)

First-order unification using variable-free relational algebra. - Emilio Jesús Gallego Arias; James Lipton; Julio Mariño; Pablo Nogueira (Log. J. IGPL, 2011)

Logic Programming in Tabular Allegories. - Emilio Jesús Gallego Arias; James Lipton (ICLP (Technical Communications), 2012)

Relational and Allegorical Semantics for Constraint Logic Programming. - Emilio Jesús Gallego Arias (2012)

Sensitivity analysis using type-based constraints. - Loris D'Antoni; Marco Gaboardi; Emilio Jesús Gallego Arias; Andreas Haeberlen; Benjamin C. Pierce (FPCDSL@ICFP, 2013)

The Ciao clp(FD) Library. A Modular CLP Extension for Prolog - Emilio Jesús Gallego Arias; Rémy Haemmerlé; Manuel V. Hermenegildo; José F. Morales 001 (CoRR, 2013)

Proving Differential Privacy in Hoare Logic. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; César Kunz; Pierre-Yves Strub (CSF, 2014)

Really Natural Linear Indexed Type Checking. - Arthur Azevedo de Amorim; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu (IFL, 2014)

Declarative Compilation for Constraint Logic Programming. - Emilio Jesús Gallego Arias; James Lipton; Julio Mariño-Carballo (LOPSTR, 2014)

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (POPL, 2015)

Differentially Private Bayesian Programming. - Gilles Barthe; Gian Pietro Farina; Marco Gaboardi; Emilio Jesús Gallego Arias; Andy Gordon 001; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

Computer-Aided Verification for Mechanism Design. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (WINE, 2016)

jsCoq: Towards Hybrid Theorem Proving Interfaces. - Emilio Jesús Gallego Arias; Benoît Pin; Pierre Jouvelot (UITP, 2016)

Dual Query: Practical Private Query Release for High Dimensional Data. - Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Zhiwei Steven Wu (J. Priv. Confidentiality, 2016)

Constraint logic programming with a relational machine. - Emilio Jesús Gallego Arias; James Lipton; Julio Mariño (Formal Aspects Comput., 2017)

Certified Graph View Maintenance with Regular Datalog. - Angela Bonifati; Stefania Dumbrava; Emilio Jesús Gallego Arias (Theory Pract. Log. Program., 2018)

Mutation Analysis for Coq. - Ahmet Çelik; Karl Palmskog; Marinela Parovic; Emilio Jesús Gallego Arias; Milos Gligoric 001 (ASE, 2019)

Towards Principled Compilation of Ethereum Smart Contracts (SoK). - Emilio Jesús Gallego Arias (NTMS, 2019)

mCoq: mutation analysis for Coq verification projects. - Kush Jain; Karl Palmskog; Ahmet Çelik; Emilio Jesús Gallego Arias; Milos Gligoric 001 (ICSE (Companion Volume), 2020)

The w-calculus: a synchronous framework for the verified modelling of digital signal processing algorithms. - Emilio Jesús Gallego Arias; Pierre Jouvelot; Sylvain Ribstein; Dorian Desblancs (FARM@ICFP, 2021)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants - A Case Study. - Jules Viennot; Guillaume Baudart; Emilio Jesús Gallego Arias; Marc Lelarge (CoRR, 2025)

Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. - Ana de Almeida Borges; Annalí Casanueva Artís; Jean-Rémy Falleri; Emilio Jesús Gallego Arias; Érik Martin-Dorel; Karl Palmskog; Alexander Serebrenik; Théo Zimmermann (J. Autom. Reason., 2025)