[Haskell-cafe] A Mascot

Tillmann Vogt Tillmann.Vogt at rwth-aachen.de
Wed Nov 16 11:25:23 CET 2011

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?

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

More information about the Haskell-Cafe mailing list