How can one rigorously specify that a given ML-functional, say, f : (int → int) → int is pure, i.e., f produces no effects (e.g., changes in a store, raises of exceptions etc.) except those possibly produced by its functional argument? In this paper, we introduce a semantic notion of monadic parametricity (purity) for second-order functionals. We show that every monadically parametric f admits a question-answer strategy tree representation. We discuss possible applications of this notion, e.g., to the verification of generic fixpoint algorithms. The results are presented in two settings: a total set-theoretic setting and a partial domain-theoretic one. All proofs are formalized by means of the proof assistant Coq.     «

How can one rigorously specify that a given ML-functional, say, f : (int → int) → int is pure, i.e., f produces no effects (e.g., changes in a store, raises of exceptions etc.) except those possibly produced by its functional argument? In this paper, we introduce a semantic notion of monadic parametricity (purity) for second-order functionals. We show that every monadically parametric f admits a question-answer strategy tree representation. We discuss possible applications of this notion, e.g...     »