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. My ORCID iD is 0000-0002-6041-2010.

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

Talks and Workshops

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:

• 15-150: Principles of Functional Programming
  • Fall 2012, which was the initial offering in Qatar
• 15-210: Parallel and Sequential Data Structures and Algorithms
  • Spring 2013, which was the initial offering in Qatar

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

• 15-150: Principles of Functional Programming
  • Spring 2012
  • Fall 2011
  • Spring 2011, which was the initial offering
• 15-210: Parallel and Sequential Data Structures and Algorithms
  • Fall 2012, which was the initial offering
• 15-212: Principles of Programming
  • Spring 2010
  • Spring 2011, which was the final offering
• 15-211: Data Structures and Algorithms
  • Fall 2010
• 21-122: Integration, Differential Equations and Approximation
  • Summer 2008
• 15-113/15-123: Introduction to C and UNIX
  • Both Fall and Spring from 2006 to 2008

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.

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

I am proud to run for The Pittsburgh Pharaoh Hounds and WVMTR. I support The Access Fund, The American Alpine Club, and The Southwestern PA Climbers Coalition.