Abstract:
We add higher-order functions to Dafny, a programming language designed for reasoning and verification. Our design of the higher-order functions separates their types from their specifications, much like the types of a method’s parameters are separated from the pre/post-condition specification of the method. The verifier translates the use of higher-order functions into first-order verification conditions to be discharged by Boogie/Z3. I will demo the Dafny system using higher-order functions in the presence of heap side effects Joint work with Dan Rosén.
Bio:
K. Rustan M. Leino is a Principal Researcher in the Research in Software Engineering (RiSE) group at Microsoft Research and Visiting Professor in the Department of Computing at Imperial College London. His research interests include a focus on programming tools, both mental and mechanical.