How can one rigorously specify that a given ML functional f : (int → int) → int is pure , i.e., f produces no computational effects except those produced by evaluation of its functional argument? In this paper, we introduce a semantic notion of monadic parametricity for second-order functionals which is a form of purity. 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. © 2013 Springer-Verlag.
CITATION STYLE
Bauer, A., Hofmann, M., & Karbyshev, A. (2013). On monadic parametricity of second-order functionals. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7794 LNCS, pp. 225–240). https://doi.org/10.1007/978-3-642-37075-5_15
Mendeley helps you to discover research relevant for your work.