[Haskell-cafe] A Mascot

[Tillmann Vogt]

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".