Veuillez choisir le dossier dans lequel vous souhaitez ajouter ce contenu :
Filtrer les résultats
Colloque
Soit T le calcul fonctionnel classique d'ordre ω et C la formulation de la théorie des types due à A. Church (1940) contenant le formalisme du calcul de conversion lambda. A toute proposition A∈C correspond une proposition A'∈T telle que ⊢c A si et seulement si ⊢T A', ce qui prouve que C≲T. De la même façon on obtient T≲C. Les systèmes C et T sont donc équivalents.
