Benutzer: Gast  Login
Titel:

On monadic parametricity of second-order functionals

Autor(en):
Andrej Bauer; Martin Hofmann; Aleksandr Karbyshev
Abstract:
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...     »
Stichworte:
Coq proof assistant; λ-calculus; monadic parametricity; semantics
Jahr:
2012
Sprache:
en
 BibTeX