[Colloq] Thesis Defense: Carl Eastlund on 11/13/12 at 1:30pm in 366 WVH

[Bekerian, Nicole]

The College of Computer and Information Science presents:

Thesis Defense by Carl Eastlund
Title: "Modular Proof Development in ACL2"
Date: 11/13/12
Time: 1:30pm
Location: 366 WVH

Abstract
The ACL2 theorem prover combines a first-order dialect of LISP with an automated proof engine for first-order logic.  While ACL2 is logically quite powerful, it can be difficult to build and maintain large models due to its ad hoc systems for modularity, namespace management, logical encapsulation, and macro expansion.  I propose a new language, Refined ACL2, extending ACL2 with expressive component and macro systems designed to accommodate large-scale proof development and flexible logical abstractions.  The component system of Refined ACL2 adapts many features of ML's functors and signatures to ACL2.  Components support nesting, parameterization, translucent specification, and refinement of abstract specifications with concrete definitions.  Refined ACL2 inherits Racket's macro system; furthermore, macro definitions can be incorporated into component specifications.

Committee
Matthias Felleisen, Pete Manolios, Riccardo Pucella, Rex Page (U of Oklahoma), and Ruben Gamboa (U of Wyoming)

Best,
Nicole


Nicole Bekerian
Administrative Coordinator

Northeastern University
College of Computer and Information Science
360 Huntington Ave.
202 West Village H
Boston, MA  02115

Phone: 617.373.2462
Fax: 617.373.5121