TY  - UNPD
A1  - Sabel, David
A1  - Schmidt-Schauß, Manfred
T1  - Reconstructing 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  - A logical framework consisting of a polymorphic call-by-value functional language and a first-order logic on the values is presented, which is a reconstruction of the logic of the verification system VeriFun. The reconstruction uses contextual semantics to define the logical value of equations. It equates undefinedness and non-termination, which is a standard semantical approach. The main results of this paper are: Meta-theorems about the globality of several classes of theorems in the logic, and proofs of global correctness of transformations and deduction rules. The deduction rules of VeriFun are globally correct if rules depending on termination are appropriately formulated. The reconstruction also gives hints on generalizations of the VeriFun framework: reasoning on nonterminating expressions and functions, mutual recursive functions and abstractions in the data values, and formulas with arbitrary quantifier prefix could be allowed.
T3  - Technical report Frank / Johann-Wolfgang-Goethe-Universität, Fachbereich Informatik und Mathematik, Institut für Informatik - 39 [v.3] 
KW  - Logik
KW  - Formale Semantik
KW  - Verifikation
KW  - Logics
KW  - Verification
KW  - Semantics
Y1  - 2010
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30-77876
N1  - Frühere Version (21. Januar 2010) u.d.T.: Reconstruction a Logic for Inductive Proofs of Properties of Functional Programs Reconstruction
IS  - Version: 22 Juni 2010
EP  - 42
PB  - Johann Wolfgang Goethe-Univ., Fachbereich Informatik und Mathematik, Inst. für Informatik, Research group for Artificial Intelligence and Software Technology
CY  - Frankfurt [am Main]
ER  -