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.

Research

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:

• User Interfaces in Theorem Proving: We have develop jsCoq a new accesible interface for the Coq Proof Assistant. SerAPI is an experimental Coq toplevel intended to power the next-generation theorem proving IDEs.
• Formalized Computing in Relation Algebra: We study relational and categorical formalisms for constraint logic programming, lessening the gap between the operational and denotational models using combinatorial proof search, and provide mechanically verified implementations.
• Verification of Mechanism Design and Differential Privacy: We work on language-based tools to facilitate the construction of formally-verified mechanisms and real-world privacy.
• Programming Languages for Audio: Faust (Functional Audio Stream) is a functional programming language specifically designed for real-time signal processing and synthesis. We are working on logics for the verification of Faust programs, semantics, efficient compilation and extensions. See also the ANR FEEVER project.

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.

Publications

Interests

• Logic: I highly enjoy logic and model theory, in particular I try to closely follow developments in λ-calculus, intuitionism, categorical and higher-order logic, and foundations of mathematics
• Programming languages: I strongly favor the use of functional strongly-typed Programming Languages such as Haskell, Coq and Agda. Programming techniques such as laziness and monads allow the programmer to write better and more correct code in less time. My current programming language of choice is Coq + SSReflect.
• Activism: Mainly computer related, I believe we can do better. Some pointers: Free Software; defend your rights in the digital world; Debian, a free operating system built by a community of volunteers; burbuja.info, collective thinking about economy and politics.
• Music: I have a strong interest in music. I'm planning to extend my research on programming languages and logic into to computer-aided composition and synthesis. I enjoy playing the piano; I usually listen to classical, industrial, rock and experimental music. In addition to Faust, Supercollider, and Chuck are interesting programming languages for sound synthesis and composition.

Software

See my GitHub Profile for a complete list of contributions.

• SerAPI, machine-friendly communication with the Coq Proof Assistant.
• JsCoq, use Coq and Ssreflect from your browser.
• HOARe2, Higher-Order Approximate Relational Refinement Types.
• ssrbits, a small library for bit vectors.
• DualQuery, practical private query release for high dimensional data.
• DFuzz, a type checker for linear dependent types.
• FuzzInf, a compiler and runtime for Differential Privacy.
• RAM, the relational abstract machine. It is currently undergoing a full rewrite, contact me if you are interested.
• A CLPFD solver for Ciao Prolog. It is now included in the Ciao distribution.
• Sloth, a Curry compiler written in Ciao-Prolog.
• ffuzz, a toy fuzzy logic library written in Haskell.
• hjsc, a toy JavaScript to assembler compiler, written in Haskell.
• ConvexHull, a 3D convex hull calculation program written in C# and OpenGL. Contact me if you are interested.

Some Talks

• Coq and User Interfaces @ Coq Implementors Workshop [Slides] (Le Croisic, 2017)
• Towards Unified Verification Environments @ Marelle (Sophia-Antipolis, 2017)
• Computer-Aided Verification of Mechanism Design:
  Challenges Combining Interactive Proof Systems @ LSV (Cachan, 2016)
• JsCoq: Towards Hybrid Theorem Proving Interfaces @ Deducteam (Cachan, 2016)
• Experiments in Certified Digital Audio Processing
  @ SpecFun [Slides] (Palaiseau, 2016)
• Bringing Theorem Proving to the (sonic) Masses
  @ CIEREC - Colloque International Des Outils Et Des Méthodes
  Innovantes Pour L'Enseignement De La Musique
  Et Du Traitement Du Signal (St-Etienne, 2015)
• Adventures in the (not-so) complex space @ 7th Coq Workshop
  [Slides] (Sophia Antipolis, 2015)
• Verification of Mechanism Design with
  Approximate Relational Refinement Types @ Inria [Slides] (Rennes, 2015)
• Reasoning About Sound Programs @ Inria [Slides] (Rennes, 2015)
• A Taste of Sound Reasoning @ LAC 2015 [Slides] (Mainz, 2015)
• Can Webaudio be Liberated from the Von Neumann Style?
  @ 1st Web Audio Conference 2015 (IRCAM) [Video] (Paris, 2015)
• Approximate Relational Refinement Types with Applications to Verification of Differential Privacy and Mechanism Design [Slides] (Gallium/PPS, 2014)
• Relation Algebra, Allegories, and Logic Programming [Slides] (Deducteam, 2014)
• Why Free Software Matters? [Slides] (Wilmington Charter School, 2013)
• Logic Programming in Tabular Allegories (IMDEA, 2012)
• Abstract Notions of Computation and Monads (Wesleyan, 2011)
• Allegories and Logic Programming (IMDEA, 2009)
• Relational Unification (UCM, 2008)
• A Taste of Functional Logic Programming (Wesleyan, 2008)
• A Framework for Combining Analysis and Verification (UPM, 2006)
• Concurrent System Verification Using Maude (UPM, 2006)
• Developing Component Based Software with Ruby on Rails (UPM, 2006)
• Higher-Order Logic and Henkin Models (UPM, 2006)
• Game Semantics and Linear Logic (Dresden, 2006)
• Linear Types and Program Optimization (UPM, 2005)

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.

Personal

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

• Debian GNU/Linux: A free, community-developed operating system.
• Emacs (Gnus + Org + AucTeX + RefTeX): The most powerful e-mail reader, personal organizer and counselor on earth. It can also edit files.
• LaTeX: The right way to write for-print documents.
• Subversion: Centralized version control. Keep the history of all your files!
• Git: Distributed version control, forget about servers, work on your own!
• GHC: A very nice compiler for a very nice language.
• OCaml: A very nice compiler for a fast and practical language.
• Unison: File synchronization has never been so easy.
• utf-8: The universal character set, please move away from legacy and headache-provoking text encodings, do it the right way!

Contact

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

Phone

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

Meta

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