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

Auteurs : Alessandro Coglio (Kestrel Institute)

EPTCS 359, 2022, pp. 168-184
In Proceedings ACL2 2022, arXiv:2205.11103
Licence : CC BY 4.0

Résumé : 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.

Soumis à arXiv le 24 Mai. 2022

Posez des questions sur cet article à notre assistant IA

Vous pouvez aussi discutez avec plusieurs papiers à la fois ici.

Instructions pour utiliser l'assistant IA ?

Résultats du processus de synthèse de l'article arXiv : 2205.11707v1

Le résumé n'est pas encore prêt
Créé le 06 Mai. 2023

Évaluez la qualité du contenu généré par l'IA en votant

Note : 0

Pourquoi avons-nous besoin de votes ?

Les votes sont utilisés pour déterminer si nous devons réexécuter nos outils de synthèse. Si le compte atteint -10, nos outils peuvent être redémarrés.

Le résumé précédent a été créé il y a plus d'un an et peut être réexécuté (si nécessaire) en cliquant sur le bouton Exécuter ci-dessous.

Recherchez des articles similaires (en version bêta)

En cliquant sur le bouton ci-dessus, notre algorithme analysera tous les articles de notre base de données pour trouver le plus proche en fonction du contenu des articles complets et pas seulement des métadonnées. Veuillez noter que cela ne fonctionne que pour les articles pour lesquels nous avons généré des résumés et que vous pouvez le réexécuter de temps en temps pour obtenir un résultat plus précis pendant que notre base de données s'agrandit.

Avertissement : Notre outil de synthèse basé sur l'IA et l'assistant virtuel fournis sur ce site Web peuvent ne pas toujours fournir des résumés complets ou des réponses exactes. Nous vous encourageons à examiner attentivement et à évaluer le contenu généré pour vous assurer de sa qualité et de sa pertinence par rapport à vos besoins.