Note that a type system, if done properly, is simply another name for a logic for proving properties of programs. Examples: * Agda (http://wiki.portal.chalmer

Note that a type system, if done properly, is simply another name for a logic for proving properties of programs. Examples: * Agda (http://wiki.portal.chalmers.se/agda/pmwiki.php http://wiki.portal.chalmers.se/agda/pmwiki.php) * Coq (https://coq.inria.fr https://coq.inria.fr) * Idris (http://www.idris-lang.org http://www.idris-lang.org)