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