BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:DAYLIGHT
DTSTART:20090308T020000
RDATE:20090308T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20090416T132202Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090511T210000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20090511T190000
DTSTAMP;VALUE=DATE-TIME:20090416T132202Z
LAST-MODIFIED;VALUE=DATE-TIME:20090512T082337Z
UID:http://calagator.org/events/1250456998
DESCRIPTION:A study/user group exploring the world of functional programm
ing based in Portland\, Oregon. The group welcomes programmers intereste
d in all functional languages\, including Haskell\, Erlang\, OCaml\, Sca
la\, and others. The group meets regularly and provides presentations\,
demos and discussions applicable to all skill levels\, from newbies and
experts. The meetings are usually on the second Monday of the month.
\;\n
\;\nAn OCaml-based automated theorem-proving textbook
\;\n
3\;\nJohn Harrison\, Intel Corporation
\;\n
\;\nMy recently publis
hed "\;Handbook of Practical Logic and Automated Reasoning"\; (
http://www.cambridge.org/9780521899574 ) is a textbook on automated theo
rem proving with the unusual feature that all the techniques described a
re accompanied by actual OCaml source code ( http://www.cl.cam.ac.uk/~jr
h13/atp/ ) that the reader can use\, modify and otherwise experiment wit
h. I believe that this kind of concrete hands-on approach has significan
t benefits for many fields of mathematics and computer science\, and par
ticularly for the area of automated theorem proving. Indeed\, the origin
al ML was specifically designed as an implementation and interaction lan
guage (hence Meta Language) for a theorem prover. In this talk I'll desc
ribe in more detail my rationale for writing the book in this way\, prov
ide a survey of the main contents and give a demo of some of the code.&#
13\;\n
\;\nJohn Harrison is a Principal Engineer at Intel Corporation
\, based in Hillsboro OR\, specializing in formal verification\, automat
ed theorem proving\, floating-point arithmetic and mathematical algorith
ms. He is also interested in the formalization of mathematics for its ge
neral intellectual interest and has formalized numerous classic theorems
in his own HOL Light theorem prover (see http://www.cs.ru.nl/~freek/100
/ ). Before joining Intel in 1998\, he received his PhD from the Univers
ity of Cambridge in England\, supervised by Mike Gordon.
\;\n\n\nTags
: pdxfunc\, functional programming\, ocaml\n\nImported from: http://cala
gator.org/events/1250456998
URL:http://pdxfunc.org/
SUMMARY:Portland Functional Programmers Study Group: OCaml-based automate
d theorem-proving
LOCATION:CubeSpace [ *sniff* out of business 12 June 2009]: 622 SE Grand
Ave.\, Portland Oregon 97214 USA
SEQUENCE:0
END:VEVENT
END:VCALENDAR