|
|
|---|
|
|
|
|---|
An ACL2 formalization of the Leo language.
This formalization defines, with mathematical precision, the syntax and semantics of Leo. This formalization covers Leo code, which is the primary artifact of the language, and also related artifacts such as Leo input files, which are considered a part of the language at large in this formalization.
This ACL2 formalization of Leo is work in progress.