I work toward making the construction of reusable, trusted software components possible and effective. My research has spanned program analysis; semantics; verification and model-checking; security; logic; complexity; and algorithms.
With Jeff Foster and Mike Hicks, I direct the laboratory for Programming Languages at the University of Maryland (PLUM). Previously, I’ve worked with the Programming Research Laboratory (PRL) at Northeastern University.
I currently serve as the PC chair for TFP 2016, as a program committee member for ECOOP 2016 and POPL 2017, and as co-editor of the Journal of Functional Programming special issue for ICFP 2015.
I co-authored the book Realm of Racket with Matthias Felleisen and undergraduates from Northeastern University, which introduces programming interactive video games.
- New paper: Soft Contract Verification for Higher-order Stateful Programs published at POPL'18 in Los Angeles, USA.
- New paper: Abstracting Definitional Interpreters published at ICFP'17 in Oxford, UK.
- My PhD student, David Darais, will be joining the faculty of the Computer Science department at the University of Vermont in January 2018!
- I'll be lecturing at the Oregon Programming Languages Summer School at the University of Oregon in late June, early July, 2017.
- Niki Vazou and Thomas Gilray have joined the PLUM lab as the inaugural Basili Post-doctoral Fellows.
- New paper: Higher-order symbolic execution for contract verification and refutation published in JFP in January.
- New paper: A Vision for Online Verification-Validation published at GPCE'16 in November.
- New paper: Constructive Galois Connections published at ICFP'16 in September.
- New grant: Online Verification-Validation, funded by the National Science Foundation, Software and Hardware Foundations program. This collaborative project is with Matthew Hammer and Bor-Yuh (Evan) Chang at the University of Colorado at Boulder.
- Trends in Functional Programming will be hosted at the University of Maryland, June 2016.
- I'm attending the NII Shonan Village Seminar on Higher-Order Model Checking and the Dagstuhl Seminar on Language Based Verification Tools for Functional Programs, both in March.
- New paper: Pushdown Control-Flow Analysis for Free published at POPL'16 in January.
- New tutorial: An Introduction to Redex with Abstracting Abstract Machines presented at POPL'16 in January.