Syntheto: A Surface Language for APT and ACL2

Alessandro Coglio, Eric McCarthy, Stephen Westfold, Daniel Balasubramanian, Abhishek Dubey, Gabor Karsai

Electronic Proceedings in Theoretical Computer Science 2022

PDF DOI Preprint

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.

Cite This Paper

@inbook{Coglio_2022,
  author = {Coglio, Alessandro and McCarthy, Eric and Westfold, Stephen and Balasubramanian, Daniel and Dubey, Abhishek and Karsai, Gabor},
  pages = {151--167},
  publisher = {Open Publishing Association},
  title = {Syntheto: A Surface Language for {APT} and {ACL}2},
  year = {2022},
  month = {may},
  volume = {359},
  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.},
  contribution = {minor},
  doi = {10.4204/eptcs.359.13},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  preprint = {https://arxiv.org/abs/2205.11706},
  url = {https://doi.org/10.4204%2Feptcs.359.13},
  month_numeric = {5}
}
Quick Info
Year 2022
DOI 10.4204/eptcs.359.13
Search Tags

Syntheto, Surface, Language, ACL2, 2022, Coglio, McCarthy, Westfold, Balasubramanian, Dubey, Karsai