The formal definition of a crash in GHC

[Alexander Berntsen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

On 28/02/14 13:41, Simon Peyton Jones wrote:
> Crashing is usually formalised by the "progress" and "type 
> preservation" theorems that papers about statically-typed
> programming languages usually offer.  You will find many examples
> of such theorems (and their proofs) in the papers about GHC's
> intermediate language 
> http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/
>
>  A "crash" would mean that execution get stuck, and the progress 
> theorem guarantees that cannot happen.
Would you, or anyone else, be able to make a wiki article on these
theorems? So that we have a centralised resource that we can refer to.
- -- 
Alexander
alexander at plaimi.net
https://secure.plaimi.net/~alexander
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
Comment: Using GnuPG with Thunderbird - http://www.enigmail.net/

iF4EAREIAAYFAlP3Ip0ACgkQRtClrXBQc7WfAAD/VoQHW/bZLgdgoLCkSsLBGyIO
B4F30jFLGuEB7NRvoIQBAKm0V4y2eutGUiSii0lTnzsP8Md3hKbZpUlcrqFmEQzf
=OBHG
-----END PGP SIGNATURE-----