Second-Order Functions and Theorems in ACL2
SOFT ('Second-Order Functions and Theorems') is a tool to mimic second-order functions and theorems in the first-order logic of ACL2. Second-order functions are mimicked by first-order functions that reference explicitly designated uninterpreted functions that mimic function variables. Fir...
Main Author: | Alessandro Coglio |
---|---|
Format: | Article |
Language: | English |
Published: |
Open Publishing Association
2015-09-01
|
Series: | Electronic Proceedings in Theoretical Computer Science |
Online Access: | http://arxiv.org/pdf/1509.06080v1 |
Similar Items
-
A Simple Java Code Generator for ACL2 Based on a Deep Embedding of ACL2 in Java
by: Alessandro Coglio
Published: (2018-10-01) -
Adding 32-bit Mode to the ACL2 Model of the x86 ISA
by: Alessandro Coglio, et al.
Published: (2018-10-01) -
The Fundamental Theorem of Algebra in ACL2
by: Ruben Gamboa, et al.
Published: (2018-10-01) -
Bit-Blasting ACL2 Theorems
by: Sol Swords, et al.
Published: (2011-10-01) -
Parallelizing an interactive theorem prover : functional programming and proofs with ACL2
by: Rager, David Lawrence
Published: (2013)