[Pl-seminar] 6/17 Seminar: Jay McCarthy, A Coq Library For Internal Verification of Running-Times

[William J. Bowman]

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
-------------- 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/20160609/43b137a0/attachment.pgp>