Benutzer: Gast  Login
Autor(en):
Andrej Bauer; Martin Hofmann; Aleksandr Karbyshev 
Titel:
On monadic parametricity of second-order functionals 
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,...    »
 
Stichworte:
Coq proof assistant; λ-calculus; monadic parametricity; semantics 
Jahr:
2012 
Sprache:
en