Links und Funktionen

Sie sind hier: Startseite / 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.



News and Events

For news and events please switch to the German page.