9 citations · 12 across the 2 of their papers we have counts for
3 papers
cs.LO2020★ 3 cited
Isomorphic Data Type Transformations
Alessandro Coglio, Stephen Westfold
In stepwise derivations of programs from specifications, data type refinements are common. Many data type refinements involve isomorphic mappings between the more abstract and more…
cs.LO2020★ 9 cited
Ethereum's Recursive Length Prefix in ACL2
Alessandro Coglio
Recursive Length Prefix (RLP) is used to encode a wide variety of data in Ethereum, including transactions. The work described in this paper provides a formal specification of RLP…
cs.PL2017
A Versatile, Sound Tool for Simplifying Definitions
Alessandro Coglio, Matt Kaufmann, Eric W. Smith
We present a tool, simplify-defun, that transforms the definition of a given function into a simplified definition of a new function, providing a proof checked by ACL2 that the old…