Syntheto: A Surface Language for APT and ACL2
Alessandro Coglio (Kestrel Institute), Eric McCarthy (Kestrel, Institute), Stephen Westfold (Kestrel Institute), Daniel Balasubramanian, (Institute for Software-Integrated Systems, Vanderbilt University), Abhishek, Dubey (Institute for Software-Integrated Systems
TL;DR
Syntheto is a user-friendly, strongly typed surface language integrated into an IDE that simplifies formally verified program synthesis in ACL2 using the APT toolkit through automated transformations and bidirectional translation.
Contribution
It introduces Syntheto, a new surface language with an IDE for more accessible and automated formal program synthesis in ACL2 using APT.
Findings
Enhanced usability with an IDE and notebook interface
Automated translation between Syntheto and ACL2/APT
Supports theorem proving and transformations seamlessly
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. Syntheto is integrated into an IDE with a notebook-style, interactive interface that translates Syntheto to ACL2 definitions and APT transformation invocations, and back-translates the prover's results to Syntheto; the bidirectional translation happens behind the scenes, with the user interacting solely with Syntheto.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.