The Whiley Programming Language

The Whiley Standard Library. This is a minimal set of primitives for interacting with the world.

Provides support for compiling Whiley programs in JavaScript. See http://whiley.org for more information on Whiley.

The Whiley Compiler (WyC)

A compiler framework for managing the Whiley Compiler and related tooling.

The Whiley2JavaCompiler is responsible for translating Whiley Intermediate Language (WyIL) files into JVM Bytecodes.

Benchmark Suite for Whiley

The WDK build system is responsible for curating and building releases of the Whiley Programming Language. This includes obtaining necessary dependencies, building documentation, etc.

Provides a framework on which compiler backends can be based. This takes a lot of the effort out of turning Whiley into something closer to a normal C-like imperative language or beyond.

Various documents relating to the Whiley Programming Language.

Request for Comment (RFC) proposals for substantial changes to the Whiley language.

A simple web IDE for running Whiley programs on your computer using a web-browser.

The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.

WyRL is a domain specific rewrite language and code generator which has been custom developed for use within the Whiley Compiler. Specifically, WyRL is used to generate the Automated Theorem Prover used within Whiley.

This is a prototype implementation for compiling Whiley to C for execution on an embedded system.

Assembler / Disassembler for Java Bytecode

Whiley Developer Website

Eclipse Plugin for the Whiley Programming Language