Benutzer: Gast  Login
Originaltitel:
Monadic Parametricity of Second-Order Functionals 
Übersetzter Titel:
Monadische Parametrizität von Funktionen zweiter Stufe 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Seidl, Helmut (Prof. Dr.) 
Gutachter:
Seidl, Helmut (Prof. Dr.); Simpson, Alex (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
monadic parametricity, fixpoint algorithms, certified analysis, Coq 
Übersetzte Stichworte:
monadische Parametrizität, Fixpunktalgorithmen, zertifizierte Analyse, Coq 
Schlagworte (SWD):
Constraint-Erfüllung; Fixpunkt; Algorithmus 
TU-Systematik:
DAT 706d; DAT 325d 
Kurzfassung:
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. 
Übersetzte Kurzfassung:
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. 
Mündliche Prüfung:
23.09.2013 
Dateigröße:
685398 bytes 
Seiten:
145 
Letzte Änderung:
07.10.2015