Books
Realm of Racket. With Matthias Felleisen, Conrad Baski, Forrest Bice, Rose DeMaio, Spencer Florence, Feng-Yun Mimi Lin, Scott Lindeman, Nicole Nussbaum, Eric Peterson, and Ryan Plessner.
Papers
Webs and Flow-Directed Well-Typedness Preserving Program Transformations. With Benjamin Quiring, John Reppy, and Olin Shivers.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'25), Seoul, South Korea, June 2025.
[ ACM ]
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis. With Benjamin Quiring.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'24), Milan, Italy, September 2024.
[ ACM ]
A Formal Model of Checked C. With Liyi Li, Yiyun Liu, Deena Postol, Leonidas Lampropoulos, and Michael Hicks.
IEEE Computer Security Foundations Symposium, Haifa, Israel, August 2022.
[ IEEE | arXiv ]
RbSyn: Type- and Effect-Guided Program Synthesis. With Sankha Guria and Jeffrey S. Foster.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'21), Online, June 2021.
[ ACM | arXiv ]
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification. With Cameron Moy, Phúc C. Nguyễn, and Sam Tobin-Hochstadt.
The 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'21), Online, January 2021.
[ ACM | arXiv ]
Constructive Galois Connections. With David Darais.
Journal of Functional Programming, 29(11), July 2019.
[ CUP | arXiv ]
Size-Change Termination as a Contract. With Phúc C. Nguyễn, Thomas Gilray, and Sam Tobin-Hochstadt.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), Phoenix, Arizona, June 2019.
[ ACM | arXiv ]
Type-Level Computations for Ruby Libraries. With Milod Kazerounian, Sankha Guria, Niki Vazou, and Jeffrey S. Foster.
The ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'19), Phoenix, Arizona, June 2019.
[ ACM | arXiv ]
Gradual Liquid Type Inference (Distinguished Paper). With Niki Vazou and Éric Tanter.
The ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'18), Boston, USA, October 2018.
[ ACM | arXiv ]
Theorem Proving for All: Equational Reasoning in Liquid Haskell. With Niki Vazou, Joachim Breitner, Rose Kunkel, and Graham Hutton.
The ACM SIGPLAN International Symposium on Haskell (Haskell'18), St. Louis, Missouri, September 2018.
[ ACM | arXiv ]
Soft Contract Verification for Higher-order Stateful Programs. With Phúc C. Nguyễn, Thomas Gilray, and Sam Tobin-Hochstadt.
The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL'18), Los Angeles, USA, January 2018.
[ ACM | arXiv ]
Abstracting Definitional Interpreters. With David Darais, Phúc C. Nguyễn, and Nicholas Labich.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'17), Oxford, UK, September 2017.
[ ACM | arXiv ]
Higher-order symbolic execution for contract verification and refutation. With Phúc C. Nguyễn and Sam Tobin-Hochstadt.
Journal of Functional Programming, 27(3), January 2017.
[ CUP | arXiv ]
A Vision for Online Verification-Validation. With Matthew A. Hammer and Bor-Yuh Evan Chang.
The 15th International Conference on Generative Programming: Concepts & Experience (GPCE'16), Amsterdam, Netherlands, November 2016.
[ ACM | arxiv ]
Constructive Galois Connections. With David Darais.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'16), Nara, Japan, September 2016.
[ ACM | arXiv ]
Pushdown Control-Flow Analysis for Free. With Thomas Gilray, Steven Lyde, Michael D. Adams, and Matthew Might.
The 43rd ACM SIGPLAN-SIGACT Symposium on Principles in Programming Languages (POPL'16), St. Petersburg, Florida, January 2016.
[ ACM | arXiv ]
Tutorial: An Introduction to Redex with Abstracting
Abstract Machines.
Tutorials at The 43rd ACM SIGPLAN-SIGACT Symposium on Principles in Programming Languages (POPL'16), St. Petersburg, Florida, January 2016.
[ HTML | PDF ]
Incremental Computation with Names. With Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, and Michael Hicks.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'15), Pittsburgh, Pennsylvania, October 2015.
[ ACM | arXiv ]
Galois Transformers and Modular Abstract Interpreters. With David Darais and Matthew Might.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'15), Pittsburgh, Pennsylvania, October 2015.
[ ACM | arXiv ]
Relatively Complete Counterexamples for Higher-Order Programs. With Phúc C. Nguyễn.
The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, Oregon, June, 2015.
[ ACM | arXiv ]
Running Probabilistic Programs Backwards. With Neil Toronto and Jay McCarthy.
The European Symposium on Programming (ESOP'15), London, United Kingdom, April, 2015.
[ Springer | arXiv ]
Abstracting Abstract Control. With Dionna Amalie Glaze.
The 10th ACM Symposium on Dynamic Languages (DLS'14), Portland, Oregon, October 2014.
[ ACM | arXiv ]
Pruning, Pushdown Exception-Flow Analysis. With Shuying Liang, Weibin Sun, Matthew Might, and Andrew W. Keep.
The 14th IEEE International Conference on Software Code Analysis and Manipulation, Victoria, British Columbia, September 2014.
[ IEEE | arXiv ]
Soft Contract Verification. With Phúc C. Nguyễn and Sam Tobin-Hochstadt.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'14), Gothenburg, Sweden, September 2014.
[ ACM | arXiv ]
Pushdown flow analysis with abstract garbage collection. With Dionna Amalie Glaze, Ilya Sergey, Christopher Earl, and Matthew Might.
Journal of Functional Programming, 24(2-3), May 2014.
[ CUP | arXiv ]
Optimizing Abstract Abstract Machines. With Dionna Amalie Glaze, Nicholas Labich, and Matthew Might.
The ACM SIGPLAN International Conference on Functional Programming (ICFP'13), Boston, Massachusetts, September 2013.
[ ACM | arXiv ]
Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. With Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, and Petey Aldous.
Proceedings of the Third ACM workshop on Security and privacy in smartphones & mobile devices, Berlin, Germany, November 2013.
[ ACM | arXiv ]
AnaDroid: Malware Analysis of Android with User-supplied Predicates. With Shuying Liang and Matthew Might.
Workshop on Tools for Automatic Program Analysis, Seattle, Washington, June 2013.
[ arXiv ]
Concrete Semantics for Pushdown Analysis: The Essence of Summarization. With Dionna Amalie Glaze.
Workshop on Higher-Order Program Analysis, New Orleans, Louisiana, June 2013.
[ arXiv ]
From Principles to Practice with Class in the First Year. With Sam Tobin-Hochstadt.
International Workshop on Trends in Functional Programming in Education, Provo, Utah, May 2013.
[ EPCTCS | arXiv ]
Higher-Order Symbolic Execution via Contracts. With Sam Tobin-Hochstadt.
The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), Tuscon, Arizona, October 2012.
[ ACM | arXiv ]
Introspective Pushdown Analysis of Higher-Order Programs. With Christopher Earl, Ilya Sergey, and Matthew Might.
The 17th ACM SIGPLAN International Conference on Functional Programming (ICFP'12), Copenhagen, Denmark, September 2012.
[ ACM | arXiv ]
Systematic Abstraction of Abstract Machines. With Matthew Might.
Journal of Functional Programming, 22(4-5), September 2012.
[ CUP | arXiv ]
Abstracting Abstract Machines. With Matthew Might.
Communications of the ACM, Research Highlights, 54(9), September 2011.
[ ACM | arXiv ]
A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. With Matthew Might.
The 18th International Static Analysis Symposium (SAS 2011), Venice, Italy, September 2011.
[ Springer | arXiv ]
Semantic Solutions to Program Analysis Problems. With Sam Tobin-Hochstadt.
FIT Session, The ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation (PLDI'11), San Jose, California, June 2011.
[ arXiv ]
Abstracting Abstract Machines. With Matthew Might.
The 15th ACM SIGPLAN International Conference on Functional Programming (ICFP'10), Baltimore, Maryland, September 2010.
[ ACM | arXiv ]
Pushdown Control-Flow Analysis of Higher-Order Programs. With Christopher Earl and Matthew Might.
The 2010 Workshop on Scheme and Functional Programming (SFP'10), Montréal, Québec, August 2010.
[ arXiv ]
Evaluating Call-By-Need on the Control Stack. With Stephen Chang and Matthias Felleisen.
Symposium on Trends in Functional Programming (TFP 2010), Norman, Oklahoma, May 2010.
[ Springer | arXiv ]
Resolving and Exploiting the k-CFA Paradox. With Matthew Might and Yannis Smaragdakis.
The ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation (PLDI'10), Toronto, Canada, June 2010.
[ ACM | arXiv ]
The Complexity of Flow Analysis in Higher-Order Languages.
PhD dissertation, Brandeis University, August 2009.
[ UMI | arXiv ]
Deciding kCFA is complete for EXPTIME. With Harry G. Mairson.
The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08), Victoria, British Columbia, Canada, September 2008.
[ ACM | arXiv ]
Flow Analysis, Linearity, and PTIME. With Harry G. Mairson.
The 15th International Static Analysis Symposium (SAS 2008), Valencia, Spain, July 2008.
[ Springer | arXiv ]
Types and Trace Effects of Higher Order Programs. With Christian Skalka and Scott F. Smith.
Journal of Functional Programming, 18(2), March 2008.
[ CUP ]
Relating Complexity and Precision in Control Flow Analysis. With Harry G. Mairson.
The Twelth ACM SIGPLAN International Conference on Functional Programming (ICFP'07), Freiburg, Germany, October 2007.
[ ACM ]
Algorithmic Trace Effect Analysis.
MS thesis, University of Vermont, May 2006.
[ UVM ]
A Type and Effect System for Flexible Abstract Interpretation of Java. With Christian Skalka and Scott F. Smith.
The ACM Workshop on Abstract Interpretations of Object-Oriented Programs, Paris, France, January 2005.
[ Elsevier ]