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: | |
---|---|
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 |
id |
doaj-a201eaf7c2f14eb582a437f6cfe40694 |
---|---|
record_format |
Article |
spelling |
doaj-a201eaf7c2f14eb582a437f6cfe406942020-11-24T21:02:18ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802015-09-01192Proc. ACL2 2015173310.4204/EPTCS.192.3:5Second-Order Functions and Theorems in ACL2Alessandro CoglioSOFT ('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. First-order theorems over these second-order functions mimic second-order theorems universally quantified over function variables. Instances of second-order functions and theorems are systematically generated by replacing function variables with functions. SOFT can be used to carry out program refinement inside ACL2, by constructing a sequence of increasingly stronger second-order predicates over one or more target functions: the sequence starts with a predicate that specifies requirements for the target functions, and ends with a predicate that provides executable definitions for the target functions.http://arxiv.org/pdf/1509.06080v1 |
collection |
DOAJ |
language |
English |
format |
Article |
sources |
DOAJ |
author |
Alessandro Coglio |
spellingShingle |
Alessandro Coglio Second-Order Functions and Theorems in ACL2 Electronic Proceedings in Theoretical Computer Science |
author_facet |
Alessandro Coglio |
author_sort |
Alessandro Coglio |
title |
Second-Order Functions and Theorems in ACL2 |
title_short |
Second-Order Functions and Theorems in ACL2 |
title_full |
Second-Order Functions and Theorems in ACL2 |
title_fullStr |
Second-Order Functions and Theorems in ACL2 |
title_full_unstemmed |
Second-Order Functions and Theorems in ACL2 |
title_sort |
second-order functions and theorems in acl2 |
publisher |
Open Publishing Association |
series |
Electronic Proceedings in Theoretical Computer Science |
issn |
2075-2180 |
publishDate |
2015-09-01 |
description |
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. First-order theorems over these second-order functions mimic second-order theorems universally quantified over function variables. Instances of second-order functions and theorems are systematically generated by replacing function variables with functions. SOFT can be used to carry out program refinement inside ACL2, by constructing a sequence of increasingly stronger second-order predicates over one or more target functions: the sequence starts with a predicate that specifies requirements for the target functions, and ends with a predicate that provides executable definitions for the target functions. |
url |
http://arxiv.org/pdf/1509.06080v1 |
work_keys_str_mv |
AT alessandrocoglio secondorderfunctionsandtheoremsinacl2 |
_version_ |
1716775862982934528 |