Abstract

Whiley is a new programming language being developed at Victoria University of Wellington, New Zealand (see whiley.org). Whiley is designed specifically to simplify program verification. This goal has constrained the language in many ways, some of which will be expected whilst others are less apparent. The language includes first-class pre- and post-conditions, and the ultimate aim is to check them at compile time. Such constraints must be pure and may range over first-class data-types (sets, lists, etc) with value semantics, and also functions that are explicitly declared pure. To simplify verification, arithmetic operates over unbounded integers and rationals. For flexibility, a flow-sensitive type system with structural subtyping is employed.

Despite being a primarily functional language, Whiley retains a distinctly imperative syntax with the look and feel of a dynamic language (i.e. Python). Whiley currently compiles to the JVM and is fully inter-operable with Java. Many challenges exist in compiling Whiley programs to the JVM for efficient execution. Furthermore, other compilation targets (e.g. JavaScript) are planned for the future. In this talk, I will introduce Whiley and discuss some of the main challenges involved.

About the Presenter

David graduated from Imperial College London in 2005, and took up a lecturer position at Victoria University of Wellington, NZ. David’s thesis was on efficient algorithms for pointer analysis of C, and his techniques have since been incorporated into GCC . His interests are in programming languages, compilers and static analysis. Since 2009, he has been developing the Whiley Programming Language (whiley.org) which is designed specifically to simplify program verification. David has previously interned at Bell Labs, New Jersey, where he worked on compilers for FPG As; and also at IBM Hursely, UK, where he worked with the AspectJ development team on profiling systems.