François-René Rideau (fare) wrote,
François-René Rideau

Next Boston Lisp Meeting: 2009-03-30 1800 at MIT 34-401B - Carl Eastlund on Modular ACL2

Carl Eastlund will give a talk about Modular ACL2.

ACL2 is a Common Lisp-based fully automated theorem prover. It was originally based on the Boyer-Moore theorem prover (Nqthm), and is currently developed by J Moore and Matt Kaufmann at the University of Texas at Austin. ACL2 has been used to verify critical hardware and software systems by companies including Intel, AMD, Rockwell-Collins, and Sun Microsystems, and won the 2005 ACM Software Systems award. This talk presents Modular ACL2, an extension of the language of ACL2 to include a module system supporting reusable proof components, external specifications, and separate development/verification.

Carl Eastlund is a Ph.D. candidate at Northeastern University's Programming Research Lab. His past research has included hardware description languages, models of object oriented programming, functional GUI representations, and the Fortress programming language. His current work contributes programming tools and language extensions to the ACL2 theorem prover.

His website is at


The Lisp Meeting will take place on Monday March 30th 2009 at 1800 (6pm) at MIT, Room 34-401B.

As the numbers indicate, this is in Building 34, on the 4th floor. This is the usual location, on 50 Vassar Street, Cambridge.

MIT map:

Google map:,+Cambridge,+MA+02139,+USA

Many thanks go to Alexey Radul for arranging for the room, and to MIT for welcoming us.

* *

Dinner: ITA Software, a fine employer of Lisp hackers (disclaimer: I work there), is kindly purchasing a buffet to accompany our monthly Boston Lisp meeting. Anyone who attends is welcome to partake.

We appreciate it if you let us know you're coming, and what food taboos you have, so that we can order the correct amount of food. Tell us by sending email to boston-lisp-meeting-register at We won't send any acknowledgement unless requested; importantly, we'll keep your identity and address confidential and won't communicate any such information to anyone, not even to our sponsors.

* * *

The previous Boston Lisp Meeting on February 23rd had 40 participants. Dimitris Vyzovitis gave a demonstration of his powerful toolkit to build distributed systems in PLT Scheme, Gerbils:

We're always looking for more speakers. The call for speakers and all the other details are at

For more information, see our new web site For posts related to the Boston Lisp meetings in general, follow this link: or subscribe to our RSS feed:

Please forward this information to people you think would be interested. Please accept my apologies for your receiving this message multiple times. My apologies if this announce gets posted to a list where it shouldn't, or fails to get posted to a list where it should. Feedback welcome by private email reply to

Tags: boston, boston-lisp-meeting, en, lisp, meeting
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded