### Export to

**Thursday, April 16, 2009 at 6:22am**and last updated

**Tuesday, May 12, 2009 at 1:23am**.

# Portland Functional Programmers Study Group: OCaml-based automated theorem-proving

This venue is no longer open for business.

### Website

### Description

*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.