9 citations
- University of OxfordGB5 papers
- The University of Texas at AustinUS3 papers
- University of California San DiegoUS2 papers
- Forschungszentrum JülichDE1 paper
- Fujitsu (Japan)JP1 paper
- Integrated Software (United States)US1 paper
- Intel (United Kingdom)GB1 paper
- Northeastern UniversityUS1 paper
- Technische Universität BerlinDE1 paper
- Universidad del NoresteMX1 paper
- University of WyomingUS1 paper
Showing cs.PLShow all
2 papers · 1 filter
cs.PL2018★ 3 cited
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★ 8 cited
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…