9 citations · 18 across the 5 of their papers we have counts for
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2018
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
Alessandro Coglio
AIJ (ACL2 In Java) is a deep embedding in Java of an executable, side-effect-free, non-stobj-accessing subset of the ACL2 language without guards. ATJ (ACL2 To Java) is a simple Ja…
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…