[Colloq] PhD Thesis Proposal - Carl Eastlund

[Rachel Kalweit]

The College of Computer and Information Science presents a PhD Thesis Proposal

Carl Eastlund
Tuesday, May 12, 2009
6:00pm
366 West Village H


Title:
Practical Programming for ACL2


Abstract:
ACL2, the Common Lisp-based theorem prover designed by Boyer,
Kaufmann, and Moore in the 1980s, has since become the most
commercially successful automated theorem prover.  Despite its
success, ACL2's design restricts several natural methods of reasoning
about programs.  Its abstraction mechanisms prevent programs from
being executed, its model of functions forces users to reason about
invalid inputs such as (+ 5 "non-numeric"), and its unhygienic macro
system allows users to write and verify terms whose surface syntax
belies their meaning.

I propose to alleviate these problems by extension of the programming
language of ACL2.  I have written Modular ACL2, adding a module system
to provide proof abstraction without sacrificing execution.  I further
propose to add a type system to (statically) reject invalid inputs to
ACL2 functions, and a hygienic macro system to preserve reasoning
about lexical scope in the surface syntax.


Thesis Committee:
Matthias Felleisen (advisor)
Panagiotis Manolios (Northeastern University)
Riccardo Pucella (Northeastern University)
Ruben Gamboa (University of Wyoming)
Rex Page (University of Oklahoma)