My Picture

Welcome to Emilio's home page. Bienvenue sur la page d'accueil d'Emilio! I am a starting researcher in the PiCube Inria team, hosted at the IRIF, Institut de Recherche en Informatique Fondamentale laboratory of the CNRS and Université de Paris Cité. You are very welcome to contact me.


My research background is in mechanically-verified functional and logic programming. These days my main project is the Coq proof assistant, which I mainly use in conjunction with the Mathematical Components Library. Have a look at my publications and GitHub profile for recent projects; some recent topics are:

I am a big fan of collaborative development platforms and I am often around on Gitter, Gitlab, and Github.

In the past I've worked on: logic programming, constraint solving, operating systems, server and network administration, collaborative web tools design and implementation, multi-paradigm declarative programming.



The W-Calculus: a synchronous framework for the verified modelling of digital signal processing algorithms with Pierre Jouvelot,Sylvain Ribstein,Dorian Desblancs Proceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design (FARM). [HAL] (corrected) [ACM DL]


Mutation Analysis for Coq with Ahmet Celik, Karl Palmskog, Marinela Parovic, and Milos Gligoric 34th International Conference on Automated Software Engineering (ASE), Nov 2019, San Diego, USA. [IEEE]


Certified Graph View Maintenance with Regular Datalog with Angela Bonifati, Stefania Dumbrava. 34th International Conference on Logic Programming, July 2018, Oxford, UK. [TPLP] [ArXiV] [HAL] [Coq Code]
SerAPI: Machine-Friendly, Data-Centric Serialization for Coq., Working Preprint. October 2016 -- Software updated to 2018 / Coq 8.8. [HAL] [GitHub]


Bringing Theorem Proving to the (Sonic) Masses with Pierre Jouvelot, and Benoît Pin. Chapter in "Innovative Tools and Methods to Teach Music and Signal Processing", Presse de Mines, [To appear]
Dual Query: Practical Private Query Release for High Dimensional Data, with Gaboardi, Marco; Hsu, Justin; Roth, Aaron; and Wu, Zhiwei Steven (2017) Journal of Privacy and Confidentiality: Vol. 7 : Iss. 2 , Article 4. [JPC] [GitHub]


jsCoq: Towards hybrid theorem proving interfaces, with Pierre Jouvelot, and Benoît Pin. Proceedings of the 12th workshop on User Interfaces for Theorem Provers, (UITP 2016), July 2016, Coimbra . [EPTCS] [ArXiV] [GitHub] [Slides]
Computer-aided verification in mechanism design, with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. 12th Conference on Web and Economics (WINE 2016), Montreal. [arXiv] [Springer]
Differentially private bayesian programming , with Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Andy Gordon, Justin Hsu, and Pierre-Yves Strub. ACM SIGSAC Conference in Computer and Communications Security, CCS'16, NY USA. [arXiv] [ACM]
Constraint Logic Programming with a Relational Machine with James Lipton and Julio Mariño y Carballo. Formal Aspects of Computing 2016. [Preprint PDF] [Springer] [Coq Code]


Adventures in the (not so) complex space, with Pierre Jouvelot. The 7th Coq workshop, Sophia Antipolis, France, 2015. [github]
A Taste of Sound Reasoning, with Olivier Hermant, Pierre Jouvelot. 13th Linux Audio Conference. Mainz, April 9-12th, 2015. [github]
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy, with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. POPL 2015. [arXiv] [ACM] [GitHub]


Declarative Compilation for Constraint Logic Programming, with James Lipton and Julio Mariño y Carballo. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LNCS 8981). Canterbury, September 9-11, 2014. [Extended] [Springer]
Really Naturally Linear Indexed Type Checking, with Arthur Azevedo de Amorim, Marco Gaboardi, and Justin Hsu. Proceedings of the 26th symposium on Implementation and Application of Functional Languages. Boston, Oct 1-3, 2014. [ArXiV] [ACM]
Proving Differential Privacy in Hoare Logic, with Gilles Barthe, Marco Gaboardi, Justin Hsu, César Kunz, and Pierre-Yves Strub 27th IEEE Computer Security Foundations Symposium (CSF 2014). Vienna, Austria, July 2014. [arXiv] [IEEE]
Dual Query: Practical Private Query Release for High Dimensional Data, with Marco Gaboardi, Justin Hsu, Aaron Roth, and Zhiwei Steven Wu 31st International Conference on Machine Learning (ICML 2014). Beijing, China, June 2014. [arXiv] [Poster] [GitHub] [JMLR]

2013 and before

Juan José Moreno Navarro, José Manuel Fernández de Labastida, Emilio Jesús Gallego Arias, and Antonio Cidoncha. Modern development of a Law Proceedings of the International Conference on ICT LAW 2013 (Information and Communication Technology and Law - Protection and Access Rights) November 2013, Porto, Portugal. [Draft]
Loris D'Antoni, Marco Gaboardi, Emilio Jesús Gallego Arias, Andreas Haeberlen, and Benjamin C. Pierce. Sensitivity Analysis using Type-Based Constraints Functional Programming Concepts In Domain-Specific Languages September 2013, Boston, MA. [PDF]
Emilio Jesús Gallego Arias. Relational and Allegorical Semantics for Constraint Logic Programming Advisors: James Lipton and Julio Mariño. July 2012, Universidad Politécnica de Madrid. [Updated PDF] [Sumbitted version, UPM-OA]
The Ciao CLP(FD) Library, A Modular CLP Extension for Prolog with Rémy Haemmerlé, Manuel V. Hermenegildo, and José F. Morales2 Proceedings of the 12th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS). 2012. [arXiv]
Emilio Jesús Gallego Arias and James Lipton. Logic Programming in Tabular Allegories Technical Communications of the 28th International Conference on Logic Programming. September 2012. [PDF] [LIPICS]
Emilio Jesús Gallego Arias, James Lipton, Julio Mariño, and Pablo Nogueira. First-order unification using variable-free relational algebra. Logic Journal of IGPL, Oxford University Press, 19(6):790-820, 2011. [PDF] [OUP]
Álvaro García, Pablo Nogueira and Emilio Jesús Gallego Arias The beta cube (extended abstract) In César Muñoz and Hélène Kirchner, editors, Proceedings of the 1st International Workshop on Strategies in Rewriting, Proving, and Programming (IWS’10) Edinburgh, UK, July 9 2010. [PDF]
Emilio Jesús Gallego Arias, Julio Mariño, and José María Rey Poza. A generic semantics for constraint functional logic programming. In Proc. of the 16th Int'l Workshop on Functional and (Constraint) Logic Programming (WFLP 2007), 2007. [PDF]
Emilio Jesús Gallego Arias, Julio Mariño, and José María Rey Poza A proposal for disequality contraints in Curry Electr. Notes Theor. Comput. Sci., 177:269-285, 2007. [PDF] [Springer OA]
Emilio Jesús Gallego-Arias and Julio Mariño. An overview of the Sloth2005 Curry system. In Michael Hanus, editor, Workshop on Curry and Functional Logic Programming, ACM press, 2005. [PDF] [ACM]



See my GitHub Profile for a complete list of contributions.

Some Talks

Brief CV

I hold an Engineering Degree in Computer Science, Master in Computational Logic and PhD from the Technical University of Madrid. From 2012 to 2014, I was a postdoc in the Putting Differential Privacy to Work team at the University of Pennsylvania. From 2014 to 2019, I was a postdoc in the Centre de Recherche en Informatique, MINES ParisTech.


I'm a native of Las Pedroñeras, Cuenca, Spain, placed in "La Mancha" region and included in "La Ruta de Don Quijote". My hometown is distinctly known for its superior purple garlic (ajo morado).

My first name is Emilio Jesús and my two family names are Gallego (father's) and Arias (mother's), as is customary in Spain.

I was close to pursuing a career in piano playing. I maintain interest in piano and classical music and try to practice often. My favorite pianist is Claudio Arrau. See him here and here, performing at his best. A true heir to Liszt's spiritual school, his playing is one of the last witnesses of the romantic style.

I consider myself an "Objective" audiophile. See NwAvGuy's great blog for more information about audio myths. Building an excellent Hi-Fi setup is not expensive, don't be fooled by snake-oil vendors, an O2 and a pair of good headphones will provide superior sound quality for a modest cost. The O2 is "open hardware", so you can built it yourself for much less money, but you'll need to invest a significant amount of time.

Tools I use


Electronic address

e at(@) x80 (dot) org

My gpg public key F878 DB33 AA77 EB4E 058F 94B3 D3DA 7A34 4681 F041. Provided you have control over your browser and you trust TERENA, you can securely retrieve my public key from here.

Physical Location

Office 4030

Mail address

Emilio Jesús Gallego Arias
Université Paris Diderot
Batiment Sophie Germain, Case 7014
8 place Aurélie-Nemours
75013, Paris


+33 (0) (Work)
ejgallego (Skype/Hangouts)


Last modified: Jan 14th, 2020. XHTML 1.1 compliant. Optimized for mobile.
Valid XHTML	1.1