Publications

Using Parallelism in a Functional Programming Language to Improve Theorem Prover Interactivity

Dissertation Proposal, 2010

My PhD dissertation research affects two main areas: (1) the development of mechanisms to permit applicative programs to execute in parallel while simultaneously being embedded in a semi-automatic reasoning system; and (2) the development of a parallel version of the primary ACL2 theorem proving process, with management of user interaction issues, such as output and goal ordering.

An Executable Model for Security Protocol JFKr

Eighth International Workshop on the ACL2 Theorem Prover and Its Applications, 2009

See the security page.

Implementing a Parallelism Library for a Functional Subset of Lisp

The International Lisp Conference, 2009

See the parallelism page.

Implementing a Parallelism Library for ACL2 in Modern Day Lisps

Master's Thesis, 2008

See the parallelism page.

Adding Parallelism Capabilities to ACL2

Sixth International Workshop on the ACL2 Theorem Prover and Its Applications, 2006

See the parallelism page.