Études-Mathématique/La vérification des types

From Lazi wiki
Jump to: navigation, search

Contexte

Sans vérification des types il est pénible d'écrire un logiciel. La vérification des types consiste à prouver des propriétés sur des formules. La plupart des preuves doivent être automatiques, sinon ce ne serait pas pratique. D'autre part, quand il y a blocage de la preuve automatique, il faut donner des informations. Il est nécessaire de prévoir un système de base, ressemblant à ce qui existe dans d'autres langages informatique. Mais il faut aussi prévoir un système ouvert qui ne limite ni les propriétés exprimées sur le code source, ni les preuves de ces propriétés.

Question

Comment implémenter la vérification des types ?

Étude

/Cas d'étude

/Système global

/Problème de la récurrence et du sans-domaine

/Qu'est-ce qu'un type

/Syntaxe des types

/Preuve automatique sur les types

Réponse