A study/user group exploring the world of functional programming based in Portland, Oregon. The group welcomes programmers interested in all functional languages, including Haskell, Erlang, OCaml, Scala, 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.

An OCaml-based automated theorem-proving textbook

John Harrison, Intel Corporation

My recently published "Handbook of Practical Logic and Automated Reasoning" ( http://www.cambridge.org/9780521899574 ) is a textbook on automated theorem proving with the unusual feature that all the techniques described are accompanied by actual OCaml source code ( http://www.cl.cam.ac.uk/~jrh13/atp/ ) that the reader can use, modify and otherwise experiment with. I believe that this kind of concrete hands-on approach has significant benefits for many fields of mathematics and computer science, and particularly for the area of automated theorem proving. Indeed, the original ML was specifically designed as an implementation and interaction language (hence Meta Language) for a theorem prover. In this talk I'll describe in more detail my rationale for writing the book in this way, provide a survey of the main contents and give a demo of some of the code.

John Harrison is a Principal Engineer at Intel Corporation, based in Hillsboro OR, specializing in formal verification, automated theorem proving, floating-point arithmetic and mathematical algorithms. He is also interested in the formalization of mathematics for its general 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 University of Cambridge in England, supervised by Mike Gordon.

ABOUT THE GROUP: Join programmers, researchers and enthusiasts to discuss functional programming. pdxfunc is a study/user group exploring the world of functional programming based in Portland, Oregon. The group welcomes programmers interested in all functional languages, including Haskell, Erlang, OCaml, Scala, 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.

ABOUT THE VENUE: The group will meet in the Events Room, the large glassed-in room by the main entrance on Hawthorne. There will a "pdxfunc" sign on the door. Feel free to show up early to eat and socialize, we have the room reserved from 6pm on.

With OSCON in town this week, bringing to town many from the functional programming community among others, we thought it would be a good idea to hold a casual functional programming meetup. There's no agenda and no talks, but there will be beer and good conversation.

We'll be meeting up on the patio at Green Dragon. If you're just visiting and are worried you won't recognize the geeks when you get there (we're usually easy enough to spot), feel free to ping people on the PDXFunc mailing list (https://groups.google.com/forum/#!forum/pdxfunc) or on IRC at #pdxfunc.