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

Justin R. Slepak jrslepak at ccs.neu.edu
Wed Jan 30 15:25:45 EST 2013


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.



More information about the Pl-sem-jr mailing list