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

Download:

Current browse context:

cs.LO

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: A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java

Authors: Alessandro Coglio (Kestrel Institute)
Abstract: This paper describes a code generator that translates ACL2 constructs to corresponding Java constructs, according to a shallow embedding of ACL2 in Java. Starting from purely functional ACL2 code, the generated Java code exhibits imperative and object-oriented features like destructive updates, loops, and overloading. The overall translation from ACL2 to Java is fairly elaborate, consisting of several ACL2-to-ACL2 pre-translation steps, an ACL2-to-Java proper translation step, and several Java-to-Java post-translation steps. Experiments suggest that the generated Java code is not much slower than the ACL2 code. The code generator can also recognize, and translate to Java, ACL2 representations of certain Java constructs, forerunning a code generation approach based on a shallow embedding of Java in ACL2 (i.e. going the other way). This code generator builds upon, and significantly extends, a simple Java code generator for ACL2 based on a deep embedding of ACL2 in Java.
Comments: In Proceedings ACL2 2022, arXiv:2205.11103
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Software Engineering (cs.SE)
Journal reference: EPTCS 359, 2022, pp. 168-184
DOI: 10.4204/EPTCS.359.14
Cite as: arXiv:2205.11707 [cs.LO]
  (or arXiv:2205.11707v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Tue, 24 May 2022 01:18:46 GMT (24kb,D)

Link back to: arXiv, form interface, contact.