Michael Greenberg
Post Doc -- Princeton University
Space-Efficient Manifest Contracts
Abstract:
Eiffel popularized
design by contract, a software design philosophy where programmers
specify the requirements and guarantees of functions via executable
pre- and post-conditions written in code. Findler and Felleisen brought
contracts to higher-order programming, inspiring the PLT Racket
implementation of contracts.
In the first half of this talk, I will contrast PLT Racket's "latent" contracts and with so-called manifest contract systems, wherein contracts and types are conflated.
The
standard implementation of contracts destroys tail recursion, possibly
altering a program's asymptotic complexity. In the second half of the
talk, I will explore semantics that avoid this problem.
Bio: Michael
Greenberg is currently a postdoc at Princeton University. He received
his PhD in Computer Science from the University of Pennsylvania (2013).
His research has focused on contracts and runtime checking, with side
forays into bidirectionality, probabalistic programming, and the Web.