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


"Live Functional Programming with Typed Holes"
C. Omar, I. Voysey, R. Chugh, and M. A. Hammer
(to appear, POPL19)
[draft] [agda]
      19 artifact evaluation badgepopl 19 artifact evaluation badge

"Model-Based Adaptation for Robotics Software"
J. Aldrich, J. Biswas, J. Camara, D. Garlan, A. Guha, J. Holtz, P. Jamshidi, C. Kästner, C. Le Goues, A. Mohseni-Kabir, I. Ruchkin, S. Samuel, B. Schmerl, C. Timperly, M. Veloso, I. Voysey
(in submission, IEEE Software)
"Hazelnut: A Bidirectionally Typed Structure Editor Calculus"
C. Omar, I. Voysey, M. Hilton, J. Aldrich, and M. A. 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 Summit on Advances in Programming Languages (SNAPL 2017)
[pdf] [slides]

Talks and Workshops

"Live and Direct Programming with Typed Holes"
C. Omar, I. Voysey, M. A. Hammer, and R. Chugh
LIVE 2018 at SPLASH 2018

"Toward a Live Stepper for Typed Expressions with Holes"
C. Omar, I. Voysey, and M. Hammer
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]


I am excited to currently be a research programmer working for Robert Harper on RedTT.

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

From August 2016 until December 2019, I was a research programmer working for Jonathan Aldrich and Manuela Veloso on the now-finished BRASS project and the Wyvern language.

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 GHC9213. I can be reached via email at my initials at cs dot cmu dot edu. My CV is available upon request.

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: 15:57, 08 Jan 2020
Valid CSS! Valid XHTML 1.0 Strict