Desfuncionalizar para Provar

05/20/2019
by   Mário Pereira, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset