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

http://fare.livejournal.com/140695.html

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 http://www.ccs.neu.edu/home/cce/

*

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: http://whereis.mit.edu/bin/map?selection=34

Google map: http://maps.google.com/maps?q=50+Vassar+St,+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 common-lisp.net. 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: http://web.media.mit.edu/~vyzo/gerbil/

NB: the following Boston Lisp Meeting is scheduled to take place on Monday April 24th 2009. Norman Ramsey will speak about purely functional dataflow optimization (in Haskell).

We're always looking for more speakers. The call for speakers and all the other details are at http://fare.livejournal.com/120393.html

For more information, see our new web site boston-lisp.org. For posts related to the Boston Lisp meetings in general, follow this link: http://fare.livejournal.com/tag/boston-lisp-meeting or subscribe to our RSS feed: http://fare.livejournal.com/data/rss?tag=boston-lisp-meeting

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 fare at tunes.org.