Miranda Perea, Favio Ezequiel (2004): On Extensions of AF2 with Monotone and Clausular (Co)inductive Definitions. Dissertation, LMU München: Fakultät für Mathematik, Informatik und Statistik 

PDF
MirandaPerea_Favio.pdf 999kB 
Abstract
This thesis discusses some extensions of secondorder logic AF2 with primitive constructors representing least and greatest fixed points of monotone operators, which allow to define predicates by induction and coinduction. Though the expressive power of secondorder logic has been wellknown for a long time and suffices to define (co)inductive predicates by means of its (co)induction principles, it is more userfriendly to have a direct way of defining predicates inductively. Moreover recent applications in computer science oblige to consider also coinductive definitions useful for handling infinite objects, the most prominent example being the data type of streams or infinite lists. Main features of our approach are the use clauses in the (co)inductive definition mechanism, concept which simplifies the syntactic shape of the predicates, as well as the inclusion of not only (co)iteration but also primitive (co)recursion principles and in the case of coinductive definitions an inversion principle. For sake of generality we consider full monotone, and not only positive definitions, after all positivity is only used to ensure monotonicity. Working towards practical use of our systems we give them realizability interpretations where the systems of realizers are strongly normalizing extensions of the secondorder polymorphic lambda calculus, system F in Currystyle, with (co)inductive types corresponding directly to the logical systems via the CurryHoward correspondence. Such realizability interpretations are therefore not reductive: the definition of realizability for a (co)inductive definition is again a (co)inductive definition. As main application of realizability we extend the socalled programmingwithproofs paradigm of Krivine and Parigot to our logics, by means of which a correct program of the lambda calculus can be extracted from a proof in the logic.
Dokumententyp:  Dissertation (Dissertation, LMU München) 

Keywords:  secondorder logic AF2, system F, inductive types, coinductive types, realizability, inductive definitions, coinductive definitions, programmingwithproofs 
Themengebiete:  500 Naturwissenschaften und Mathematik
500 Naturwissenschaften und Mathematik > 510 Mathematik 
Fakultäten:  Fakultät für Mathematik, Informatik und Statistik 
Sprache der Hochschulschrift:  Englisch 
Datum der mündlichen Prüfung:  12. November 2004 
1. Berichterstatter/in:  Schwichtenberg, Helmut 
MD5 Prüfsumme der PDFDatei:  09669c05d17983bac4671ff743c6ee55 
Signatur der gedruckten Ausgabe:  0001/UMC 14150 
ID Code:  2855 
Eingestellt am:  25. Nov. 2004 
Letzte Änderungen:  19. Jul. 2016 16:17 