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.
Efficient compilation of a verification-friendly programming language. Min Hsien (Sam) Weng. PhD Thesis, University of Waikato, 2019.
Compiling Whiley for WebAssembly. Wei Hua. Final Year Project (COMP489) Thesis, Victoria University of Wellington, 2019.
Compiling Whiley for the Ethereum Virtial Machine. Dylan Kumar. Final Year Project (ENGR489) Thesis, Victoria University of Wellington, 2019.
Towards Compilation of an Imperative Language for FPGAs. Baptiste Pauget, Alex Potanin and David J. Pearce. In Workshop on Virtual Machines and Language Implementations (VMIL), pages 47--56, 2018. ©ACM Press
Rewriting for Sound and Complete Union, Intersection and Negation Types. David J. Pearce. In Proceedings of the Conference on Generative Programming: Concepts & Experience (GPCE), pages 117--130, 2018. ©ACM Press