L3: A Specification Language for Instruction Set Architectures

L3 is implemented in Poly/ML 5.7 and the latest version is l3.tar.bz2 [2018-02-09]. There is also a manual and an ITP 2012 paper: Directions in ISA specification.

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.


The following are known users of our models/tools: