Heinrich Apfelmus wrote: > > Lambda calculus is the basis for all three types of semantics: > > 1) Call-by-need (usually, implementations of Haskell are free to choose > other evaluation strategies as long as the denotational semantics match) > > 2) The denotational semantics of a lambda calculus with general > recursion, see also > > http://en.wikibooks.org/wiki/Haskell/Denotational_semantics > > 3) Not sure what you mean by proof theoretic semantics. Apparently, the > trace of any program execution like, say > > product [1..5] -> 1 * product [2..5] -> .. -> 120 > > is a proof that the initial and the final expression denote the same value. > > The Curry-Howards correspondence is about the type system, viewing types > as logical propositions and programs as their proofs.
This seems to address the first point (the role of lambda calculus. But what of the second point, the role equational logic. I assume (perhaps incorrectly) that lambda calculus is not *a logic*. See: http://lambda-the-ultimate.org/node/3719 Best Regards, Pat This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe