Joe Leslie-Hurd

Gilith QR code

Contact Details

Mailing Address:

Joe Leslie-Hurd
Intel Corporation
Mail Stop RA2-406
2501 NW 229th Ave.
Hillsboro, OR 97124, USA

Email:  joe@gilith.com  [GPG key]

Professional Biographies

Joe recently joined Intel Corporation in Portland, Oregon. Before that, he worked at Galois, Inc. where he used functional programming languages to construct correctness proofs of software. He studied at Cambridge University, receiving degrees in mathematics and then computer science as he made the realization that it's easier to program computers to find proofs than to do them by hand. In his free time Joe contributes to open source projects, carries out independent research and regularly gives talks to audiences at all levels.

Joe Leslie-Hurd recently joined Intel Corporation in Portland, Oregon as a Component Design Engineer. Before that, he worked at Galois, Inc. as Formal Methods Lead, where he applied rigorous semantic techniques to design and analyze security-critical software. He completed a Ph.D. at Cambridge University on the formal verification of probabilistic programs, and his work since has included: developing a package management system for higher order logic theories; applying automatic proof techniques for first order logic; and creating the world's first formally verified chess endgame database.

Joe Leslie-Hurd, Ph.D. recently joined Intel Corporation in Portland, Oregon as a Component Design Engineer. Before that, he worked at Galois, Inc. as Formal Methods Lead, where he applied techniques founded on formal semantics to design and analyze security-critical software. He has over 10 years experience formally verifying the correctness of complex software, including probabilistic programs, elliptic curve cryptography and game tree analysis algorithms. He is the developer of Metis, an automatic theorem prover for first order logic, and coordinates the OpenTheory project, a package management system for higher order logic theories. Dr. Leslie-Hurd is an active member of the theorem proving research community, having organized conferences in 2005 and 2008, given invited talks, and regularly appears on program committees and reviews papers for conferences and journals. Prior to joining Galois in 2007, Dr. Leslie-Hurd was a research fellow at Magdalen College, Oxford University. He studied at Cambridge University, receiving a Masters degree in Mathematics in 1997, and a Ph.D. in Computer Science in 2002.

Curriculum Vitae

In HTML and PDF formats. Also: a full list of publications in HTML and PDF formats.

Personal Biography

The eldest of three brothers, I grew up in the Bath end of Somerset: a county in the south west of England. My first nine years were spent in the tiny village of Cranmore, and then my family moved to the nearby town of Frome. There I attended Frome College and took up chess to while away the lunchtimes. I completed my studies in Cambridge, and then worked for a time in the university Computer Laboratory while living in the village of Girton. I continued my research in Oxford, taking up go to while away the evenings, and then moved into industry in Portland, Oregon.

What's in a Name?

J. R. R. Tolkien was a professor of philology at Oxford University, and used his skills to devise languages spoken in his fantasy world of Middle-earth. The word gilith means "outer space" in Sindarin, a language spoken by elves. Here is a poem I like from the Lord of the Rings:

All that is gold does not glitter,
Not all those who wander are lost;
The old that is strong does not wither,
Deep roots are not reached by the frost.
From the ashes a fire shall be woken,
A light from the shadows shall spring;
Renewed shall be blade that was broken,
The crownless again shall be king.