Andrew Appel's students

Former students

  1. Andrew P. Tolmach, PhD (1992) Debugging Standard ML.
  2. Zhong Shao, PhD (1994) Compiling Standard ML for Efficient Execution on Modern Machines.
  3. Marcelo J. R. Goncalves, PhD (1995) Cache Performance of Programs with Intensive Heap Allocation and Generational Garbage Collection.
  4. Matthias Blume, PhD (1997) Hierarchical Modularity and Intermodule Optimization.
  5. Drew Dean, PhD (1999) Formal Aspects of Mobile Code Security.
  6. Jeffrey L. Korn, PhD (1999) Abstraction and Visualization in Graphical Debuggers.
  7. Daniel C. Wang, PhD (2002) Managing Memory with Types.
  8. Kedar N. Swadi, PhD (2003) Typed Machine Language.
  9. Lujo Bauer, PhD (2003) Access Control for the Web via Proof-Carrying Authorization.
  10. Eunyoung Lee, PhD (2004) Secure Linking: A Logical Framework for Policy-Enforced Component Composition.
  11. Juan Chen, PhD (2004) A Low-Level Typed Assembly Language with a Machine-checkable Soundness Proof.
  12. Amal J. Ahmed, PhD (2004) Semantics of Types for Mutable State.
  13. Gang Tan, PhD (2005) A Compositional Logic for Control Flow and its Application to Foundational Proof-Carrying Code.
  14. Dinghao Wu, PhD (2005) Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code.
  15. Xinming Ou, PhD (2005) A Logic Programming Approach to Network Security Analysis.
  16. Sudhakar Govindavajhala, PhD (2006) A Formal Approach to Practical Network Security Management.
  17. Aquinas Hobor, PhD (2008) Oracle Semantics.
  18. Chris Richards, PhD (2010) The Approximation Modality in Models of Higher-Order Types.
  19. Robert Dockins, PhD (2012) Operational Refinement for Compiler Correctness.
  20. James Gordon Stewart, PhD (2015) Verified Separate Compilation for C.
  21. Josiah Dodds, PhD (2015) Computation Improves Interactive Symbolic Execution.
  22. Qinxiang Cao, PhD (2018) Separation-Logic-based Program Verification in Coq.
  23. Olivier Savary Bélanger, PhD (2019) Verified Extraction for Coq.
  24. Santiago Cuellar, PhD (2020) Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency.
  25. Zoe Paraskevopoulou, PhD (2020) Verified Optimizations for Functional Languages.
  26. Qinshi Wang, PhD (2023) Foundationally Verified Data Plane Programming.
  27. Joomy Korkut, PhD (2024) Foreign Function Verification Through Metaprogramming
  28. Matthew Weaver, PhD (2024) Bicubical Directed Type Theory
  29. Ariel Kellison, Cornell PhD (2024, co-advised with David Bindel), Type-Based Approaches to Rounding Error Analysis

Current students

Josh Cohen