July 17th, 6:30 - Aaron Mansheim - Continuations: Primitive, Practical, Proof

[Michael Bevilacqua-Linn <michael.bevilacqualinn@gmail.com>]

Hey folks,

This month's meeting will be on July 17th, 6:30 at the Comcast center.  

RSVP at the doodle poll here - http://www.doodle.com/7rn37rixc8fitysb

Aaron Mansheim will be presenting 'Continuations: Primitive, Practical, Proof'.

Abstract as follows.

All levels welcome - we'll reserve half our time for questions. This

talk aims to prepare you for these online tutorials:

matt.might.net/articles and www.cis.upenn.edu/~bcpierce/sf/

We'll examine an interpreter for a primitive functional programming

language (untyped lambda calculus). The interpreter is written in a

practical functional programming language (Scala).

Then we'll introduce continuations. We'll use continuations in place of

any loops, recursion, or exception handling in order to re-implement a

part of the interpreter in a functional programming language similar to

ML (Coq).

Coq facilitates writing proofs about programs. We'll demonstrate using

Coq to prove that the recursive implementation and the continuations

implementation produce the same results.

Thanks,

MBL