Verified Functional Algorithms

Software Foundations #3

by Andrew W. Appel, Andrew Tolmach (Contributor), Michael Clarkson (Contributor)

The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.

Verified Functional Algorithms shows how a variety of fundamental data structures can be mechanically verified.

Genres: Computer Science

Unknown Binding

Published January 1, 2021

About the author

Andrew W. Appel, Ph.D. (Computer Science, Carnegie Mellon University, 1985; A.B., Princeton University, 1981) is the Eugene Higgins Professor of Computer Science at Princeton University, where he has been on the faculty since 1986. He served as department chair from 2009 to 2015. His research is in software verification, computer security, programming languages and compilers, and technology policy.

He has been editor-in-chief of ACM Transactions on Programming Languages and Systems and is a fellow of the ACM (Association for Computing Machinery). He has worked on fast N-body algorithms (1980s), Standard ML of New Jersey (1990s), Foundational Proof-Carrying Code (2000s), and the Verified Software Toolchain (2010s). He is the author of several scientific papers on voting machines and election technology, served as an expert witness on two voting-related court cases in New Jersey, and has taught a course at Princeton on election machinery.