My research focuses on directly applying formalism to practical problems. Much of my work takes place in the emerging field of semantics engineering, where I scale PL techniques up to work on real systems.
My primary focus is on improving the the POSIX shell and building tools to support its use.
I work in a variety of other areas: contracts and gradual types; tools for directly expressing PL formalism, using logic programming and SMT solving; and foundational semantics for decidable languages, like Kleene algebra with tests.
| Semester | Courses |
|---|---|
| S2021 |
CS 105 (w/ Prof. Birrell)
CS 190 |
| F2020 |
CS 054 (archived)
CS 190 (archived) |
| S2020 |
CS 054 (archived) (w/ Prof. Osborn)
CS 181-N (archived) |
| F2019 | On leave |
| S2019 | On leave |
| F2018 | On leave |
| S2018 |
CS 131 (archived)
CS 54 (archived) |
| F2017 |
CS 131 (archived)
CS 190 (archived) |
| S2017 |
CS 55 (archived)
CS 131 (archived) |
| F2016 |
CS 131 (archived)
CS 190 (archived) |
| S2016 |
CS 51 (w/ Profs. Chen, Kampe, and Wu)
CS 181-N Software Foundations (archived) |
| F2015 |
CS 51 (w/ Profs. Chen, Kampe, and Wu)
CS 131 (archived) |
| Course | Day | Time | Location |
|---|---|---|---|
| CS 105 | Tue | 9-11am PT | Zoom |
| CS 105 | Fri | 1:30-3pm PT | Zoom |
I can be reached via email to schedule meetings on Zoom, Skype, or telephone. I am also on Zulip for my respective courses.
| Year | Student | Title |
|---|---|---|
| 2019 | Teddy Katz (MIT) |
Verified Compilation of Abstract Network Policies (with Adam Chlipala) |
| 2018 | Austin Blatt | Mechanized Semantics for Word Expansion in the POSIX Shell |
| 2017 | Eric Campbell | Infiniteness and Linear Temporal Logic |