L3: A Specification Language for Instruction Set Architectures

L3 is implemented in Poly/ML 5.5 and the latest version can be downloaded from l3.tar.bz2 [2015-11-27]. There is also a manual.

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

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 in isa-models.tar.bz2.

HOL4 versions of these models can be found in the examples directory. These models are now available for use in Isabelle/HOL.


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


The following are known users of our models/tools: