Flow Typing for References in Whiley

The Whiley language splits into a fully functional “core” and an imperative “outer layer”.  References and objects do not exist within the functional core.  However, they can exist within the imperative outer layer and are necessary for supporting state and other side-effecting computation.  Here’s a simple example:

define Buffer as ref { [int] items . . . → Read More: Flow Typing for References in Whiley

Exploring The Verification Corner

Recently, I was lucky enough to meet Rustan Leino whilst at a conference in Tallin, Estonia.  The Whiley project owes a lot to Rustan, as much of his work has been the inspiration behind Whiley.  In particular, his PhD thesis introduced the idea of Extended Static Checking and he then worked on the seminal . . . → Read More: Exploring The Verification Corner