Latest documents http://publikationen.ub.uni-frankfurt.de/index/index/ Tue, 22 Jun 2010 17:47:16 +0200 Tue, 22 Jun 2010 17:47:16 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828 This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need 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 call-by-need lambda calculus with letrec is an isomorphism between the respective term-models.We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen. Manfred Schmidt-Schauß; David Sabel; Elena Machkasova workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7828 Tue, 22 Jun 2010 17:47:16 +0200 http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826 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. David Sabel; Manfred Schmidt-Schauß workingpaper http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/7826 Tue, 22 Jun 2010 17:44:13 +0200