[PL-sem-jr] PL Jr, January 31

[Justin R. Slepak]

Higher-Order Contracts

Contracts offer an easy way to express invariants that might be difficult or impossible to express in some type system. The programmer makes precondition and postcondition assertions on a function, with blame attributed to the caller or the callee if a precondition or postcondition is violated. The story for checking a first-order function's contract is simple. On the other hand, Rice's theorem means it is impossible to check most assertions about functions, and it may not be immediately obvious where a higher-order value will flow to (and require assertion checks). We will see how to generalize this contract checking strategy to handle higher-order contracts while still keeping track of the blameworthy parties and "dependent" contracts, where a function's arguments are mentioned in the postcondition.

---
Justin Slepak
PhD student, Computer Science dept.