Syntheto: A Surface Language for APT and ACL2 | |
---|---|
Author | |
Abstract |
Syntheto is a surface language for carrying out formally verified program synthesis by transformational refinement in ACL2 using the APT toolkit. Syntheto aims at providing more familiarity and automation, in order to make this technology more widely usable. Syntheto is a strongly statically typed functional language that includes both executable and non-executable constructs, including facilities to state and prove theorems and facilities to apply proof-generating transformations. |
Year of Publication |
2022
|
Journal |
Electronic Proceedings in Theoretical Computer Science
|
Volume |
359
|
Date Published |
05/2022
|
ISSN Number |
2075-2180
|
URL |
http://dx.doi.org/10.4204/EPTCS.359.13
|
DOI |
10.4204/eptcs.359.13
|
Google Scholar | BibTeX | XML | DOI |