Technical report Frank / JohannWolfgangGoetheUniversität, Fachbereich Informatik und Mathematik, Institut für Informatik
2 search hits
 40

Simulation in the callbyneed lambdacalculus with letrec
(2010)

Manfred SchmidtSchauß
David Sabel
Elena Machkasova
 This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic callbyneed lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the callbyneed lambda calculus with letrec is an isomorphism between the respective termmodels.We show that the equivalence property proven in this paper transfers to a callbyneed letrec calculus developed by Ariola and Felleisen.
 39 [v.3]

Reconstructing a logic for inductive proofs of properties of functional programs
(2010)

David Sabel
Manfred SchmidtSchauß
 A logical framework consisting of a polymorphic callbyvalue functional language and a firstorder 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 nontermination, which is a standard semantical approach. The main results of this paper are: Metatheorems 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.