[PRL] Speaking at Boston Lisp meeting, 4/22

[Peter Dillinger]

I will be giving a relatively short talk about ACL2/ACL2s at the
Boston Lisp meeting, at MIT.  It's too late to register, but feel free
to show up if you promise to be last in line for food.  ;)

My talk will give a brief overview of ACL2, explanations and demos of
important features our development environment, ACL2s, and a demo of
an aspect of ACL2 that I think the audience will find interesting:
efficient execution.  I will define the fibonacci function and show
how I can speed up execution by proving it compliant with Common Lisp
and taking advantage of a Common Lisp compiler.  I will take that a
step further by defining a version using a more efficient, more
complicated algorithm, proving the two versions equivalent, and then
getting ACL2 to use the simple one for abstract, logical reasoning and
the fast one for evaluation/execution.  Commercial ACL2 users have
used this approach to define simulators that are both efficient and
provably equivalent to their ACL2 specifications.

Fun stuff. :)

-peter

----- Forwarded message from Faré <fahree at gmail.com> -----

Date: Wed, 2 Apr 2008 20:28:03 -0400
From: Faré <fahree at gmail.com>
To: boston-lisp at common-lisp.net
Subject: [boston-lisp] Next Boston Lisp Meeting: Tuesday April 22nd 2008,
	6pm at MIT 34-401B

http://fare.livejournal.com/121355.html
Next Boston Lisp Meeting: Tuesday April 22nd 2008, 6pm at MIT 34-401B

ITA Software, a fine employer of Lisp hackers (full disclaimer: they
employ me), has kindly offered to sponsor a dinner for our Monthly
Boston Lisp Meeting. Please send mail to boston-lisp-meeting-register
at common-lisp.net with a list of attendees so I may order the correct
amount of food. No registration, no food.

Peter Dillinger will give a 25' talk about Theorem proving with ACL2s.
ACL2, "A Computational Logic for Applicative Common Lisp", was
recognized with the 2005 ACM Software System Award for its power and
usefulness in verifying safety-critical applications. New users,
however, found it difficult to use for a variety of reasons. ACL2s <
http://acl2s.peterd.org/acl2s/ > is an Eclipse-based development
environment we have made to make ACL2 easier to learn and use. Peter
C. Dillinger is a Ph.D. Student at Northeastern University, Panagiotis
Manolios, advisor.

Hans Hübner will give a 50' presentation of The BKNR Common Lisp web
application development environment. BKNR < http://bknr.net/ > is a
one-stop repository of open source Common Lisp modules used to develop
and deploy web applications, featuring a pure Lisp transaction based
persistence layer. Hans Hübner has been a hacker for over 20 years,
and has discovered Common Lisp as his favourite programming language
in 2001. He is a freelance consultant whose research interests include
persistence systems and hardware to support dynamic programming.

Please note that the meeting is taking place at an unusual date, to
accomodate for the availability of the main speaker, who is coming
from Berlin (Germany) to talk to us.

The Lisp Meeting with take place at MIT, room 34-401B. As the numbers
indicate, this is in Building 34, on the 4th floor.

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

PS: The previous Boston Lisp Meeting on March 31st was a big success,
with over 70 attendants. Thanks a lot to all those who came. I hope
we'll meet again and have more of those interesting conversations.

PPS: We're still looking for speakers. We have a lot of potential
speakers, but not enough confirmed speakers at scheduled dates. The
call for speakers and all the other details are at <
http://fare.livejournal.com/120393.html >.

PPPS: Please forward this information to people who would be
interested. Please accept my apologies for your receiving this message
multiple times.

For posts related to the Boston Lisp meetings in general, follow this
link: http://fare.livejournal.com/tag/boston-lisp-meeting

[ François-René ÐVB Rideau | Reflection&Cybernethics | http://fare.tunes.org ]
- "If you're so smart, how come you're not rich?"
- "If you're so rich, how come you're not smart?"
        -- narrated by Steven E. Landsburg, "The Armchair Economist"
_______________________________________________
boston-lisp mailing list
boston-lisp at common-lisp.net
http://common-lisp.net/cgi-bin/mailman/listinfo/boston-lisp

----- End forwarded message -----

-- 
Peter Dillinger
pcd at ccs.neu.edu
http://www.peterd.org