Links und Funktionen

You are here: Home / Publikationen / What Is a Pure Functional?


Martin Hofmann, Aleksandr Karbyshev, and Helmut Seidl (2010)

What Is a Pure Functional?

In: ICALP (2), pp. 199-210.

Given an ML function f : (int->int)->int how can we rigorously specify that f is pure, i.e., produces no side-effects other than those arising from calling its functional argument? We show$~$ that existing methods based on preservation of invariants and relational parametricity are insufficient for this purpose and thus define a new notion that captures purity in the sense that for any functional F that is pure in this sense there exists a corresponding question-answer strategy. This research is motivated by an attempt to prove algorithms correct that take such$~$ supposedly pure functionals as input and apply them to stateful arguments in order to inspect intensional aspects of their behaviour.

Document Actions