A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java

A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java

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 Java code generator that turns ACL2 functions into AIJ representations that are evaluated by the AIJ interpreter. AIJ and...

Full description

Bibliographic Details
Main Author: Alessandro Coglio
Format: Article
Language:English
Published: Open Publishing Association 2018-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1810.04308v1
id doaj-3bc009225f694137ba186254679a67b4
record_format Article
spelling doaj-3bc009225f694137ba186254679a67b42020-11-25T02:12:44ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-10-01280Proc. ACL2 201811710.4204/EPTCS.280.1:15A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in JavaAlessandro Coglio0 Kestrel Institute 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 Java code generator that turns ACL2 functions into AIJ representations that are evaluated by the AIJ interpreter. AIJ and ATJ enable possibly verified ACL2 code to run as, and interoperate with, Java code, without much of the ACL2 framework or any of the Lisp runtime. The current speed of the resulting Java code may be adequate to some applications.http://arxiv.org/pdf/1810.04308v1
collection DOAJ
language English
format Article
sources DOAJ
author Alessandro Coglio
spellingShingle Alessandro Coglio
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
Electronic Proceedings in Theoretical Computer Science
author_facet Alessandro Coglio
author_sort Alessandro Coglio
title A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
title_short A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
title_full A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
title_fullStr A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
title_full_unstemmed A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
title_sort simple java code generator for acl2 based on a deep embedding of acl2 in java
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-10-01
description 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 Java code generator that turns ACL2 functions into AIJ representations that are evaluated by the AIJ interpreter. AIJ and ATJ enable possibly verified ACL2 code to run as, and interoperate with, Java code, without much of the ACL2 framework or any of the Lisp runtime. The current speed of the resulting Java code may be adequate to some applications.
url http://arxiv.org/pdf/1810.04308v1
work_keys_str_mv AT alessandrocoglio asimplejavacodegeneratorforacl2basedonadeepembeddingofacl2injava
AT alessandrocoglio simplejavacodegeneratorforacl2basedonadeepembeddingofacl2injava
_version_ 1724908509325164544

Similar Items