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.
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.
Faculty Host: Frank Pfenning
sdinardo [atsymbol] cs.cmu.edu