|
|
|---|
|
|
|
|---|
An ACL2 library for the Syntheto language.
Syntheto is a surface language for ACL2 and APT, aimed at a wider range of users than typical ACL2 and APT experts.
Syntheto is being developed by Kestrel Institute, in collaboration with Vanderbilt University.
This library includes, both under development, a shallow and a deep embedding of Syntheto in ACL2.
The shallow embedding consists of ACL2 macros that correspond very closely to the Syntheto abstract syntax. These macros can be bidirectionally translated to/from non-ACL2 representations of the Syntheto abstract syntax. In particular, this is used in an IDE for Syntheto that Vanderbilt University is developing in collaboration with Kestrel Institute.
The deep embedding consists of a formalization of the syntax and semantics of Syntheto in ACL2. It serves to provide a precise definition of the language, and may be useful, in the future, when developing APT-like transformations that operate directly on the Syntheto language.