[Pl-seminar] Reminder: Seminar Tomorrow: Jay McCarthy, A Coq Library For Internal Verification of Running-Times

[William J. Bowman]

Reminder: Talk tomorrow!

On Thu, Jun 09, 2016 at 02:53:40PM -0400, William J. Bowman wrote:
> NUPRL Seminar presents
> 
> Jay McCarthy
> University of Massachusetts Lowell
> 
> 1:30pm--3:30pm
> Friday, June 17th 2016
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
> 
> Title: A Coq Library For Internal Verification of Running-Times
> 
> Abstract:
> We present a Coq library that lifts an abstract yet precise
> notion of running-time into the type of a function. Our library is
> based on a monad that counts abstract steps, controlled by one of the
> monadic operations. The monad's computational content, however, is
> simply that of the identity monad so programs written in our
> monad (that recur on the natural structure of their arguments) extract
> into idiomatic OCaml code. We evaluated the expressiveness of the
> library by proving that red-black tree insertion and search, merge
> sort, insertion sort, Fibonacci, iterated list insertion, BigNum
> addition, and Okasaki's Braun Tree algorithms all have their expected
> running times.
> 
> Bio:
> Jay McCarthy is an associate professor at UMass Lowell in the Computer
> Science Department. He is a member of the PLT research group and works
> on the Racket programming language. He is passionate about computer
> science education & diversity, formal verification, programming
> language expressiveness, and his wonderful family.
> 
> 
> -- 
> William J. Bowman
> Northeastern University
> College of Computer and Information Science



> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20160616/82e2ddc4/attachment.pgp>