Language
A formalization of the Syntheto language in ACL2.
This is a deep embedding of Syntheto in ACL2.
We explicitly formalize the syntax of the languge,
along with its semantics.
This is work in progress.
Subtopics
- Static-semantics
- Static semantics of Syntheto.
- Abstract-syntax
- Abstract syntax of Syntheto.
- Outcome
- Fixtype of Syntheto outcomes.
- Abstract-syntax-operations
- Operations on the Syntheto abstract syntax.
- Outcome-list
- Fixtype of lists of Syntheto Ocutomes
- Outcomes
- Syntheto outcomes.
