L3: An ISA Specification Language

L3 is implemented in Poly/ML 5.5 and can downloaded from here: l3.tar.bz2 (22st July 2015).

Alexandre Joannou has provided support for Vim syntax highlighting. This is maintained at the repository vim-l3.

Some documentation is available here: l3.pdf.

The release contains a sample specification "tiny.spec" that is based on Thaker's Tiny 3 computer. For background information see Simon Moore's ECAD course notes.

ARM, MIPS and x86 models are available here: isa-models.tar.bz2.


Anthony Fox. Directions in ISA specification. In Interactive Theorem Proving (ITP), 2012.


The following are known users of our models/tools: