Back to Search
Start Over
Desfuncionalizar para Provar
- Publication Year :
- 2019
-
Abstract
- This paper explores the idea of using defunctionalization as a proof technique for higher-order programs. Defunctionalization builds on substituting functional values by a first-order representation. Thus, its interest is that one can use an existing program verification tool, without further extensions in order to support higher-order. This papers illustrates and discusses this approach by means of several running examples, built and verified using the Why3 verification framework.<br />Comment: in Portuguese
- Subjects :
- Computer Science - Logic in Computer Science
Subjects
Details
- Language :
- Portuguese
- Database :
- arXiv
- Publication Type :
- Report
- Accession number :
- edsarx.1905.08368
- Document Type :
- Working Paper