Andrew W. Appel

Eugene Higgins Professor of Computer Science
Department of Computer Science
Princeton University

Andrew Appel Bio & Contact

Publications

Vita

My students

Research Interests: program verification, computer security, programming language semantics, machine-checked proofs, compilers, and election technology.

Verified Software Toolchain
VST project page
     CertiCoq</img
CertiCoq project page
      VeriFFI</img
VeriFFI
Verified Network Toolchain
      VeriNum
     
Voting machines

Selected articles on voting: (more here and here)
Securing the Vote — National Academies report
Florida is the Florida of ballot-design mistakes
Pilots of risk-limiting election audits in California and Virginia
BMDs are not meaningfully auditable
New Jersey gets ballot-tracking only half right
Did Sean Hannity misquote me?
Georgia’s election avoided an even worse nightmare...
New Hampshire Election Audit, part 1; and part 2
ES&S Uses Undergraduate Project to Lobby New York Legislature...
A PDF File Is Not Paper, So PDF Ballots Cannot Be Verified
Five-part series on the Swiss e-voting system:   1 2 3 4 5
Magical thinking about BMD contingency plans
The anomaly of cheap complexity
Is Internet Voting Secure? The Science and the Policy Battles

   Internet Voting? Really?

Technology Policy

Center for Information Technology Policy

My blog at Freedom to Tinker

Other technology policy work I've done


Previous research projects

2015-2021: The Science of Deep Specification
2013-2017: Formally Verified Cryptography
2006-now: Verified Software Toolchain
2004-2006: Enterprise Network Security Analysis
1997-2005: Foundational Proof-Carrying Code for security of untrusted code.
1986-1996: Standard ML of New Jersey, a compiler for the type-safe functional programming language ML.