Welcome to Emilio's home page. Bienvenue sur la page d'accueil d'Emilio!

I am a postdoctoral researcher at the FEEVER project in CRI Mines-ParisTech. Find below some of my papers and miscellaneous information. You are very welcome to contact me.

Research

My research background is in programming languages theory. Current topics are:

• 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.
• 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.
• 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.

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. Supercollider is an interesting programming language for sound synthesis and composition.

Software

• JsCoq, use Coq and Ssreflect from your browser.
• 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

• Towards Certified Digital Audio Processing
  @ Marelle Seminar [Slides soon] (Sophia Antipolis, 2015)
• 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.

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 R.04

Mail address

Emilio Jesús Gallego Arias
Investigateur PostDoctoral
Centre de recherche en Informatique, ARMINES
35, rue Saint Honoré
77305 FontaineBleau Cedex
France

Phone

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

Meta

Last modified: December 17th, 2014. XHTML 1.1 compliant. Optimized for mobile.