16 Nov
2011
16 Nov
'11
10:25 a.m.
Am 16.11.2011 10:07, schrieb Andrew Butterfield: > On 16 Nov 2011, at 08:46, Ertugrul Soeylemez wrote: > >> But I think, despite the well-founded denotational semantics of Haskell, >> bottom does not play that much of a role. > There is one? Where? Last time I looked (a while ago, admittedly) > there was no denotational (or any formal) semantics for Haskell. > - lots of stuff for fragments of Haskell-like languages or parts of Haskell, but not a > full proper definitive semantics for *Haskell*, as found in the wild... > > Looking at > http://en.wikibooks.org/wiki/Haskell/Denotational_semantics > the first footnote states > "In fact, there are no written down and complete denotational semantics of Haskell. This would be a tedious task void of additional insight and we happily embrace the folklore and common sense semantics." > > However, if you have a proof-based tool used for reasoning about Haskell programs > in a safety-critical environment, you might just need to do this tedious task, > particularly in order to show your proof rules sound. > - has anyone in that area done this? is it available ? > > Is there a definitive Operational Semantics? Axiomatic? http://verify.rwth-aachen.de/fp09 The lecture is about reducing (simple) Haskell to the lambda calculus (denotational semantics) and then showing the operational semantics of the untyped lambda calculus. It is amazing that a practical language can be reduced to the lambda calculus so easily. It made me into a Haskell programmer. They also use this practically in a Java tool to prove termination of Haskell programs. It is mentioned in the last hcar under "Automated Termination Analyzer for Haskell".