English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

This paper describes a code generator that translates ACL2 constructs tocorresponding Java constructs, according to a shallow embedding of ACL2 inJava. Starting from purely functional ACL2 code, the generated Java codeexhibits imperative and object-oriented features like destructive updates,loops, and overloading. The overall translation from ACL2 to Java is fairlyelaborate, consisting of several ACL2-to-ACL2 pre-translation steps, anACL2-to-Java proper translation step, and several Java-to-Java post-translationsteps. Experiments suggest that the generated Java code is not much slower thanthe ACL2 code. The code generator can also recognize, and translate to Java,ACL2 representations of certain Java constructs, forerunning a code generationapproach based on a shallow embedding of Java in ACL2 (i.e. going the otherway). This code generator builds upon, and significantly extends, a simple Javacode generator for ACL2 based on a deep embedding of ACL2 in Java.

A Complex Java Code Generator for ACL2 Based on a Shallow Embedding of ACL2 in Java