Desfuncionalizar para Provar
Logic in Computer Science
2019-05-22 v1
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.
Cite
@article{arxiv.1905.08368,
title = {Desfuncionalizar para Provar},
author = {Mário Pereira},
journal= {arXiv preprint arXiv:1905.08368},
year = {2019}
}
Comments
in Portuguese