me

Ian E. Voysey

I am a research programmer working for Jonathan Aldrich on the Obsidian programming language. I can be reached via email at my initials at cs dot cmu dot edu; my office is TCS441.

Research

Interests

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.

Publications

"Filling Typed Holes with Live GUIs"
C. Omar, D. Moon, A. Blinn, I. Voysey, N. Collins, and R. Chugh
42nd ACM SIGPLAN International Conference on
Programming Language Design and Implementation (PLDI '21)

[paper text] [agda]
acm
      artifact evaluation badgeacm artifact evaluation badge
"Live Functional Programming with Typed Holes"
C. Omar, I. Voysey, R. Chugh, and M. A. Hammer
46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '19)
[extended version] [agda]
popl
      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, and I. Voysey
IEEE Software (Volume: 36, Issue: 2, March-April 2019)
[website] [article]
"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 '17)
[official] [tech report] [agda] [live impl]
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 '17)
[pdf] [slides]

Talks and Workshops

"Live and Direct Programming with Typed Holes"
C. Omar, I. Voysey, M. A. Hammer, and R. Chugh
LIVE '18 at SPLASH '18
[draft]
"Toward a Live Stepper for Typed Expressions with Holes"
C. Omar, I. Voysey, and M. Hammer
LIVE '17 at SPLASH '17
[draft]
"Running Incomplete Programs"
I. Voysey, C. Omar, and M. Hammer
"Off the Beaten Track" at POPL '17
[talk abstract] [slides]
"Hazelnut: A Structure Editor Calculus"
PoP Seminar, 13 October 2016
[slides]
"Proving Theorems About Functional Programs"
Concert RG, 23 February 2016
[code and notes]

Projects

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

From January 2020 to September 2020, I was a research programmer working for Robert Harper on RedTT.

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.

Teaching

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:

Education

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

Miscellaneous

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.

I am proud to run for The Pittsburgh Pharaoh Hounds. In 2010, I helped to design the t-shirt that won the Sweepstakes t-shirt design award.

last modified: 15:29, 29 Apr 2021
Valid CSS! Valid XHTML 1.0 Strict github mark