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? PS - I love the mascot - thanks Heath !
Greets, Ertugrul
-- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-------------------------------------------------------------------- Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 Lero@TCD, Head of Foundations & Methods Research Group Director of Teaching and Learning - Undergraduate, School of Computer Science and Statistics, Room G.39, O'Reilly Institute, Trinity College, University of Dublin http://www.scss.tcd.ie/Andrew.Butterfield/ --------------------------------------------------------------------