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.
Together with 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 co-authored the book Realm of Racket with Matthias Felleisen and undergraduates from Northeastern University, which introduces programming interactive video games.
- New draft: Size-Change Termination as a Contract.
- New draft: Type-Level Computations for Ruby Libraries.
- Gradual Liquid Type Inference won a Distinguished Paper award at OOPSLA 2018!
- I'm serving on the OOPSLA 2019 Review Committee.
- New paper: Gradual Liquid Type Inference to appear at OOPSLA'18 in Boston.
- New paper: Theorem Proving for All to appear at Haskell 2018 in St. Louis, MO.
- I served on the thesis committee Quentin Stiévenart's dissertation, Scalable Designs for Abstract Interpretation of Concurrent Programs: Application to Actors and Shared-Memory Multi-Threading.
- I'm co-organizing PLMW @ ICFP, the Programming Languages Mentoring Workshop, co-located with ICFP 2018 in St. Louis, MO.
- I'm serving on the Selection Committee for the Student Research Competition at both PLDI and ICFP 2018.
- My post-doc, Thomas Gilray, will be joining the faculty of the Computer Science department at the University of Alabama at Birmingham.
- 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.