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

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA256 On 28/02/14 13:41, Simon Peyton Jones wrote: theorems? So that we have a centralised resource that we can refer to. - -- Alexander alexander@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-----