User: Guest  Login
Original title:
Monadic Parametricity of Second-Order Functionals
Translated title:
Monadische Parametrizität von Funktionen zweiter Stufe
Author:
Karbyshev, Aleksandr
Year:
2013
Document type:
Dissertation
Institution:
Fakultät für Informatik
Advisor:
Seidl, Helmut (Prof. Dr.)
Referee:
Seidl, Helmut (Prof. Dr.); Simpson, Alex (Prof., Ph.D.)
Language:
en
Subject group:
DAT Datenverarbeitung, Informatik
Keywords:
monadic parametricity, fixpoint algorithms, certified analysis, Coq
Translated keywords:
monadische Parametrizität, Fixpunktalgorithmen, zertifizierte Analyse, Coq
Controlled terms:
Constraint-Erfüllung; Fixpunkt; Algorithmus
TUM classification:
DAT 706d; DAT 325d
Abstract:
We provide a characterization of the class of monadically parametric (pure) second-order functionals. We show that purity of F : (AB) → C in this sense implies the existence of a strategy tree which represents a strategy for computation of F. We consider possible applications of purity among which is the design of verified local generic solvers. All the formalized proofs are carried out by means of the proof assistant Coq.
Translated abstract:
Wir führen eine Charakterisierung für die Klasse der monadisch parametrischen (reinen) Funktionen zweiter Stufe ein. Es wird gezeigt, dass für eine Funktion F : (AB) → C, die in diesem Sinne rein ist, ein Strategiebaum existiert, der eine Auswertungsstrategie für F repräsentiert. Wir diskutieren mögliche Anwendungen für diesen Reinheitsbegriff, u.a. die Entwicklung von verifizierten lokalen generischen Lösern. Alle formalisierten Beweise wurden mit dem Beweis-Assistenten Coq erstellt.
WWW:
https://mediatum.ub.tum.de/?id=1144371
Date of submission:
06.05.2013
Oral examination:
23.09.2013
File size:
685398 bytes
Pages:
145
Urn (citeable URL):
https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130923-1144371-0-6
Last change:
07.10.2015
 BibTeX