Mini-CV
- 2025-now: Researcher Engineer, CNRS, π³ team (previously πr²)
“MALINCA: bridging the linguistic gap between the mathematician and the machine”, - 2019–2024: Starting Researcher, Inria, π³ team (previously πr²)
“Unified Environments for Large Scale Verification”, “Collaborative Verified Mathematical Documents” - 2017–2019: Associated Member, Télécom ParisTech
BART Blockchain Joint Center - 2014–2019: Postdoctoral Researcher, MINES ParisTech
(advisor, Pierre Jouvelot)
“Faust Everywhere: Strongly typed FP for audio”
“Towards Universal Proof Development Environments” - 2012–2014: Postdoctoral Researcher, University of Pennsylvania (advisor, Benjamin Pierce)
“Putting Differential Privacy to Work” - 2012: PhD in Computer Science (cum laude) Technical University of Madrid (advisors Jim Lipton, Julio Mariño)
“Relational and Allegorical Semantics for Constraint Logic Programming”
(Mathematics Genealogy Project) - 2007: European Master in Computational Logic (w. honors), Technical University of Madrid (advisor Jim Lipton)
“Relational Unification” - 2005: Computer Science Degree (w. honors), Technical University of Madrid (advisor Julio Mariño)
“The Sloth2005 Logic-Functional System”
Detailed CV
I was interested in computers and machines since I can remember. Given my insistence, my parents (with a lot of effort!) got me a ZX Spectrum +2A, which I used to teach myself how to program at age 8.
Later, I moved to a PC architecture, and I played along with Borland Turbo C++, around 15, I started to use Linux, and my generous high-school teacher got me some classic books like the Dragon Book, Algorithms + Data Structures = Programs, and Tanenbuam's Structured Computer Organization.
This allowed me to understand computers from the ground up; at the time my main interests were systems and compilers. While in high-school, I participated in the 1st and 2nd Spanish Computer Olympic, classing 9ᵗʰ both times.
In 1998 I went to study computer science at Madrid's Technical University; there, I was quickly introduced to functional and logic programming, which quickly became my tools of choice (in particular Haskell).
In 2004, while reading SPJ's The Implementation of Functional Programming Languages, I met my future PhD advisor Jim Lipton. To my biggest shock, he introduced me to the Curry-Howard-Kolmogorov correspondence, and thus my interest in formal systems and logic started.
Then, I joined the Babel research group (a precursor of IMDEA Software), where I did complete my Master's and PhD studies.
In 2012, I joined the programming language department of the University of Pennsylvania to start my post-doctoral studies. There I was exposed to the theory community, which I highly enjoyed, and more crucially, to the Rocq Prover which is my main line of work today.
More about me
I enjoy contributing to open source projects and collaborative development. Access to open source software and in particular to the GNU toolchain and the Linux kernel were essential for me back in the day. I'm very grateful to all of the people that made that possible.
My editor of choice is GNU Emacs; this is the patch I'm most proud of 🤣.
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. The most impressive player I've ever seen live is Martha Argerich, just incredible! Rafael Orozco and Alicia de Larrocha cannot be missed either, IMVHO.
I like audio gear. 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.