Nathan Whitehead


Contact Information

Email:

Office: 387 Engineering 2

Office phone: (831)459-5637

Home phone: (408)245-0084


Papers

With Jordan Johnson and Martín Abadi, Policies and Proofs for Code Auditing, in Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis, 2007, pages 1--14.

A Certified Distributed Security Logic for Authorizing Code, in International Workshop, TYPES 2006, Revised Selected Papers, published in Lecture Notes in Computer Science 4502, Springer-Verlag, 2007.

With Martín Abadi, BCiC: A System for Code Authentication and Verification, in Proceedings of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2004), in Lecture Notes in Artificial Intelligence 3452, Springer-Verlag, 2005, pages 110-124.

With Martín Abadi and George Necula, By Reason and Authority: A System for Authorization of Proof-Carrying Code, in Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW), 2004, pages 236-250. The figure as a separate file is also provided.

a legal note


Dissertations and Reports

Combining Reason and Authority for Authorization of Proof-Carrying Code PhD dissertation, March 2008. Martín Abadi, Cormac Flanagan, George Necula, and Allen Van Gelder comprised the examining committee. Slides from my defense presentation.

Combining Reason and Authority for Code Authentication and Verification. Dissertation Proposal, October 2005. Allen Van Gelder, Martín Abadi, Cormac Flanagan, and George Necula were members of the examining committee.

Combining Reason and Authority for Authorization of Proof-Carrying Code. Masters Project Report, June 2004. Approved by Martín Abadi and Allen Van Gelder.


Projects

My main project at the moment is BCIC, a system for code authentication and verification. Visit the project page for more information.

I have a blog on finance and investing, The Paranoid Brain. Come learn how I think you should manage your money to avoid getting burned. Also, I often post interactive JavaScript calculator applets for doing financial calculations, come and play.

One of my other projects is a new language, QT. It is a functional programming language based on term rewriting that has a very flexible type system. Visit the project page for more information.


Downloads

BCIC Proof Scripts, which includes extractable proofs of Datalog, Binder, and BCIC's decidability, along with various other proofs related to my dissertation.

Blog

Check out my LiveJournal blog.