We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.SE

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: An approach to translating Haskell programs to Agda and reasoning about them

Abstract: We are using the Agda programming language and proof assistant to formally verify the correctness of a Byzantine Fault Tolerant consensus implementation based on HotStuff / LibraBFT. The Agda implementation is a translation of our Haskell implementation based on LibraBFT. This short paper focuses on one aspect of this work.
We have developed a library that enables the translated Agda implementation to closely mirror the Haskell code on which it is based. This makes it easier and more efficient to review the translation for accuracy, and to maintain the translated Agda code when the Haskell code changes, thereby reducing the risk of translation errors. We also explain how we capture the semantics of the syntactic features provided by our library, thus enabling formal reasoning about programs that use them; details of how we reason about the resulting Agda implementation will be presented in a future paper.
The library that we present is independent of our particular verification project, and is available, open-source, for others to use and extend.
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Software Engineering (cs.SE)
Cite as: arXiv:2205.08718 [cs.LO]
  (or arXiv:2205.08718v1 [cs.LO] for this version)

Submission history

From: Mark Moir [view email]
[v1] Wed, 18 May 2022 04:33:48 GMT (26kb)

Link back to: arXiv, form interface, contact.