me on my old motorcycle



I use logic and type theory to try to isolate and describe computational phenomena. I'm interested in things like: homotopy type theory; constructive and substructural logics; mechanized and mechanically-assisted proof; category theory; functional programming; and logic programming.


"Hazelnut: A Bidirectionally Typed Structure Editor Calculus"
C. Omar, I. Voysey, M. Hilton, J. Aldrich, and M. Hammer
44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)
[official] [tech report] [agda] [live impl] [tfp2016 draft]
popl 17 artifact evaluation badge

"Towards Semantic Foundations for Program Editors"
C. Omar, I. Voysey, M. Hilton, J. Sunshine, C. Le Goues, J. Aldrich, and M. Hammer
2nd Summint on Advances in Programming Languages (SNAPL 2017)
[pdf] [slides]

Talks and Workshops

"Toward a Live Stepper for Typed Expressions with Holes"
C. Omar, I. Voysey, and M. Hammer
(to appear) LIVE 2017 at SPLASH 2017

"Running Incomplete Programs"
I. Voysey, C. Omar, and M. Hammer
"Off the Beaten Track" at POPL 2017
[talk abstract] [slides]

"Hazelnut: A Structure Editor Calculus"
PoP Seminar, 13 October 2016

"Proving Theorems About Functional Programs"
Concert RG, 23 February 2016
[code and notes]

Working Papers

"Hazelnut Live: Semantic Foundations for Evaluating Incomplete Programs"
C. Omar, I. Voysey, M. Hilton, and M. Hammer
[draft] [agda]


I am currently a Research Programmer working for Jonathan Aldrich and Manuela Veloso on the BRASS project and the Wyvern language.

On nights and weekends, I work on the mechanized metatheory for the hazelgrove project.

Since 2013 I have been learning about homotopy type theory, cubical type theory, and the connections to machine checked proofs.

In 2012 and 2013, I worked with Iliano Cervesato on the Meta-CLF project and on some more general linear logic research.

In the summer of 2009 I worked with Anupam Datta and Jason Franklin in Cylab, using software model checking techniques to verify security properties of a small hypervisor.

In the summer of 2007 I worked for Katia Sycara in the Robotics Institute. I worked on profiling and optimizing a distributed engine for multi-agent simulation.


I was the TA for Dan Licata at The Oregon Programming Languages Summer School in the summer of 2013.

In the summer of 2012, I was the instructor for 15-150 at Carnegie Mellon University.

I was a TA at Carnegie Mellon University in Qatar for the following courses and semesters:

I was a TA at Carnegie Mellon University for the following courses and semesters:


I received a Bachelor's degree in both Computer Science and Discrete Mathematics and Logic from Carnegie Mellon University in 2010.


In 2012, I received the inaugural A. Nico Habermann Educational Service Award for my part in developing 15-150 and 15-210. My brief acceptance speech can be found here.

In 2010, I helped to design the t-shirt that won the Sweepstakes t-shirt design award.

Contact & Misc

My office is WeH4114.

I can be reached via email at my initials at or my first initial, then my last name at My CV is available upon request.

I keep a research-only blog, mostly as a pensieve. Following tradition, it exists almost entirely as not-quite-finished text files on my hard drive instead of posts on the internet.

A fair number of things I've done can be found on github.

I am proud to run for The Pittsburgh Pharaoh Hounds.

last modified: 22:27, 19 Sep 2017
Valid CSS! Valid XHTML 1.0 Strict