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

[Justin R. Slepak]

We meet at 10:00 am in WVH 166.

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

----- Original Message -----
From: Justin R. Slepak <jrslepak at ccs.neu.edu>
To: pl-sem-jr at lists.ccs.neu.edu
Sent: Wed, 30 Jan 2013 15:25:45 -0500 (EST)
Subject: PL Jr, January 31

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.