Andrew Appel's students
Former students
-
Andrew P. Tolmach,
Ph.D. (1992)
Debugging Standard ML. Professor,
Portland State University.
-
Zhong Shao,
Ph.D. (1994)
Compiling Standard ML for Efficient Execution on Modern Machines.
Professor, Yale University.
-
Marcelo J. R. Goncalves,
Ph.D. (1995)
Cache
Performance of Programs with Intensive Heap Allocation and
Generational Garbage Collection.
-
Matthias Blume,
Ph.D. (1997)
Hierarchical
Modularity and Intermodule Optimization.
Senior Software Engineer, Google, Inc.
-
Richard (Drew) Dean,
Ph.D. (1999) Formal Aspects
of Mobile Code Security.
Computer Scientist, SRI and then Amazon; deceased 2022.
-
Jeffrey L. Korn,
Ph.D. (1999) Abstraction and Visualization in Graphical Debuggers.
Software Engineer, Google, Inc.
-
Daniel C. Wang,
Ph.D. (2002) Managing Memory with Types. Computer Scientist, Amazon.com.
-
Kedar N. Swadi,
Ph.D. (2003) Typed Machine Language.
Head of Data Science, PhonePe, Pune, India.
-
Lujo Bauer,
Ph.D. (2003) Access Control for the Web
via Proof-Carrying Authorization. Professor,
Carnegie Mellon University.
- Eunyoung Lee,
Ph.D. (2003) Secure Linking:
A Logical Framework for Policy-Enforced Component Composition.
Associate Professor, Dongduk Women's University, Seoul, Korea.
- Juan Chen,
Ph.D. (2004) A Low-Level Typed Assembly Language with a Machine-checkable
Soundness Proof. Computer Scientist, Google, Inc.
- Amal J. Ahmed,
Ph.D. (2004) Semantics of Types for Mutable State.
Professor, Northeastern University.
- Gang Tan,
Ph.D. (2005)
A Compositional Logic for Control Flow and its Application to
Foundational Proof-Carrying Code.
Professor, Pennsylvania State University.
- Dinghao Wu,
Ph.D. (2005)
Interfacing Compilers, Proof Checkers, and Proofs for Foundational
Proof-Carrying Code.
Professor, Pennsylvania State University.
- Xinming Ou,
Ph.D. (2005)
A Logic Programming Approach to Network Security Analysis.
Professor, University of South Florida.
-
Sudhakar Govindavajhala,
Ph.D. (2006)
A Formal Approach to Practical Network Security Management.
Software consultant in the financial industry.
-
Aquinas Hobor,
Ph.D. (2008)
Oracle Semantics.
Associate Professor, University College London.
-
Chris Richards,
Ph.D. (2010)
The Approximation Modality in Models of Higher-Order Types.
Computer Scientist, Google, Inc.
- Robert Dockins,
Ph.D. (2012) Operational Refinement for Compiler Correctness.
Applied Scientist, Amazon Web Services.
- James Gordon Stewart, Ph.D. (2015) Verified Separate Compilation for C.
Lead, Formalized Security, Riverside Research.
- Josiah Dodds,
Ph.D. (2015) Computation Improves Interactive Symbolic Execution.
Researcher, Amazon Web Services.
- Qinxiang Cao,
Ph.D. (2018) Separation-Logic-based Program Verification in Coq.
Associate Professor, Shanghai Jiao Tong University.
- Olivier Savary Bélanger, Ph.D. (2019) Verified Extraction for Coq. Research Engineer, Galois.com.
- Santiago Cuellar, PhD (2020) Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency. Research Engineer, Galois.com.
- Zoe Paraskevopoulou,
PhD (2020) Verified Optimizations for Functional Languages. Assistant Professor, National Technical University of Athens.
- Qinshi Wang, PhD (2023) Foundationally Verified Data Plane Programming. Principal Engineer, Formal Methods Group, Huawei.
- Joomy Korkut, PhD (2024) Foreign Function Verification Through Metaprogramming. Researcher, Bloomberg LLC
- Matthew Weaver, PhD (2024) Bicubical Directed Type Theory
- Ariel Kellison, Cornell PhD (2024, co-advised with David Bindel), Type-Based Approaches to Rounding Error Analysis. Postdoc, Sandia National Labs
Current students
Josh Cohen