Dr. David J. Pearce

Whiley

Whiley is a hybrid imperative and functional programming language which has been under development since 2009. Find out more at whiley.org or try it online at whileylabs.com. The complete source code for the compiler and theorem prover is available on GitHub. There is also a Wikipedia page and a dedicated Reddit group.

Related Publication(s)

Language Design Meets Verifying Compilers (Keynote). David J. Pearce. In Proceedings of the Conference on Generative Programming: Concepts and Experiences, pages 104--123, 2022. ©ACM

Verifying Whiley Programs with Boogie. David J. Pearce, Mark Utting and Lindsay Groves. In Journal of Automated Reasoning (JAR), 2022. ©Springer

Whiley to TypeScript Transpiler. Thomas Rainford. Final Year Project (ENGR489) Thesis, Victoria University of Wellington, 2021.

Transpiling Whiley to C++. Max McMurray. Final Year Project (ENGR489) Thesis, Victoria University of Wellington, 2021.

Compiling Whiley for Embedded Systems. Juan van den Anker. Research Project (COMP589) Thesis, Victoria University of Wellington, 2021.

•••

Related Talk(s)

Language Design Meets Verifying Compilers

This is the keynote presentation I gave at the Conference on Generative Programming: Concepts & Experiences (GPCE'22). See also my paper of the same name.

Finding Bugs with Specification-Based Testing is Easy!

This was the (prerecorded) conference presentation that accompanies my paper with the same name.

Functional Reactive Programming in Whiley

Functional Reactive Programming (FRP) is a paradigm which brings functional programming to inherently non-functional environments. FRP has been recently popularised for building web applications through the likes of React, Angular, Elm, etc. In this talk, I'll explore FRP for building web applications and, in particular, examine an FRP framework written in Whiley and how it works.
•••