TY - UNPD A1 - Sabel, David A1 - Schmidt-Schauß, Manfred T1 - Reconstruction of a logic for inductive proofs of properties of functional programs T2 - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik ; 39 N2 - The interactive verification system VeriFun is based on a polymorphic call-by-value functional language and on a first-order logic with initial model semantics w.r.t. constructors. This paper provides a reconstruction of the corresponding logic when partial functions are permitted. Typing is polymorphic for the definition of functions but monomorphic for terms in formulas. Equality of terms is defined as contextual equivalence based on observing termination in all contexts. The reconstruction also allows several generalizations of the functional language like mutual recursive functions and abstractions in the data values. The main results are: Correctness of several program transformations for all extensions of a program, which have a potential usage in a deduction system. We also proved that universally quantified equations are conservative, i.e. if a universally quantified equation is valid w.r.t. a program P, then it remains valid if the program is extended by new functions and/or new data types. T3 - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 39 KW - Formale Semantik KW - Logik KW - Verifikation Y1 - 2010 UR - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/34436 UR - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-344362 UR - http://www.ki.informatik.uni-frankfurt.de/papers/frank/frank-39.pdf IS - Version: 21 Jan. 2010 EP - 39 PB - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik CY - Frankfurt am Main ER -