Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
On Monadic Parametricity of Second-Order Functionals
verfasst von : Andrej Bauer, Martin Hofmann, Aleksandr Karbyshev
Erschienen in: Foundations of Software Science and Computation Structures
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
How can one rigorously specify that a given ML functional
$f : (\texttt{int} \to \texttt{int}) \to \texttt{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
.