Vers un modele formel pour le raisonnement a partir des contextes

摘要

Ces dix dernieres annees de nombreuses recherches dans le domaine des contextes ont ete menees, cependant, peu d'entre elles ont utilise la logique comme semantique. Dans cet article, nous abordons ce probleme en utilisant une theorie constructive des types comme support pour la modelisation des contextes. Nous decrivons un outil theorique forme a partir de la theorie intuitionniste des types. Cette theorie est etendue par les enregistrements a types dependants - DTR - qui permettent la representation de connaissances partielles et le raisonnement sur des donnees evolutives.