Martin Hofmann, Aleksandr Karbyshev and Helmut Seidl. What Is a Pure Functional?. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide and Paul G. Spirakis, editors, ICALP (2), volume 6199 of Lecture Notes in Computer Science, pages 199-210, July 2010. Springer.

Given an ML function $f : (int \to int) \to 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.

Download: PDF Reference: Bibtex The original publication is available at