[Pl-seminar] 2009-03-30 Boston Lisp Meeting: Carl Eastlund on Modular ACL2

[Francois-Rene Rideau]

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.