Andrew Appel's students
Andrew P. Tolmach,
Debugging Standard ML.
- Zhong Shao,
Compiling Standard ML for Efficient Execution on Modern Machines.
Marcelo J. R. Goncalves,
Performance of Programs with Intensive Heap Allocation and
Generational Garbage Collection.
Modularity and Intermodule Optimization.
Ph.D. (1999) Formal Aspects
of Mobile Code Security.
Jeffrey L. Korn,
Ph.D. (1999) Abstraction and Visualization in Graphical Debuggers.
Daniel C. Wang,
Ph.D. (2002) Managing Memory with Types.
Kedar N. Swadi,
Ph.D. (2003) Typed Machine Language.
Ph.D. (2003) Access Control for the Web
via Proof-Carrying Authorization.
- Eunyoung Lee,
Ph.D. (2004) Secure Linking:
A Logical Framework for Policy-Enforced Component Composition.
- Juan Chen,
Ph.D. (2004) A Low-Level Typed Assembly Language with a Machine-checkable Soundness Proof.
- Amal J. Ahmed,
Ph.D. (2004) Semantics of Types for Mutable State.
- Gang Tan,
A Compositional Logic for Control Flow and its Application to
Foundational Proof-Carrying Code.
- Dinghao Wu,
Interfacing Compilers, Proof Checkers, and Proofs for Foundational
- Xinming Ou,
A Logic Programming Approach to Network Security Analysis.
A Formal Approach to Practical Network Security Management.
Christopher D. Richards,
Ph.D. (2010) The Approximation Modality in Models of Higher-Order Types.
- Robert Dockins,
Operational Refinement for Compiler Correctness.
- James Gordon Stewart, Ph.D. (2015) Verified Separate Compilation for C.
- Josiah Dodds, Ph.D. (2015) Computation Improves Interactive Symbolic Execution.
- Qinxiang Cao,
Ph.D. (2018) Separation-Logic-based Program Verification in Coq.
- Olivier Savary Bélanger, PhD (2019) Verified Extraction for Coq.
- Santiago Cuellar, PhD (2020) Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency.
- Zoe Paraskevopoulou,
PhD (2020) Verified Optimizations for Functional Languages.