Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Portland Functional Programmers Study Group: OCaml-based automated theorem-proving</h1> <div class='date'><time class="dtstart dt-start" title="2009-05-11T19:00:00" datetime="2009-05-11T19:00:00">Monday, May 11, 2009 from 7</time>–<time class="dtend dt-end" title="2009-05-11T21:00:00" datetime="2009-05-11T21:00:00">9pm</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202389907'><span class='fn org p-name'>CubeSpace [ *sniff* out of business 12 June 2009]</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">622 SE Grand Ave.</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">Oregon</span> <span class="postal-code p-postal-code">97214</span> <div class="country-name p-country-name">USA</div> (<a href='https://maps.google.com/maps?q=622%20SE%20Grand%20Ave.,%20Portland%20Oregon%2097214%20USA'>map</a>) </div> </div> <div class="description p-description"> <p><i>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.</i></p> <p><b>An OCaml-based automated theorem-proving textbook</b></p> <p>John Harrison, Intel Corporation</p> <p>My recently published "Handbook of Practical Logic and Automated Reasoning" ( <a href="http://www.cambridge.org/9780521899574">http://www.cambridge.org/9780521899574</a> ) is a textbook on automated theorem proving with the unusual feature that all the techniques described are accompanied by actual OCaml source code ( <a href="http://www.cl.cam.ac.uk/~jrh13/atp/">http://www.cl.cam.ac.uk/~jrh13/atp/</a> ) 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.</p> <p>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 <a href="http://www.cs.ru.nl/~freek/100/">http://www.cs.ru.nl/~freek/100/</a> ). Before joining Intel in 1998, he received his PhD from the University of Cambridge in England, supervised by Mike Gordon.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://pdxfunc.org/">Website</a></li> </ul> </div>