Colloque

Sur l'équivalence de certaines formulations de la théorie des types

M. L'Abbé

ML

Membre a labase

M. L'Abbé

Résumé du 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.

Contexte

Section :

Physique et mathématiques

Thème du colloque :

Physique et mathématiques

Responsables :

Georges Hall

Hôte : Université Laval

Découvrez d'autres communications scientifiques

Dans le même colloque
Du même congressiste

Titre du colloque :

Physique et mathématiques

Théorie de la régression de l'image latente des particules ionisantes

P. Demers

Sur l'équivalence de certaines formulations de la théorie des types

M. L'Abbé

Sur les représentations P-adiques, entières d'un groupe fini

J. Maranda

Voir tous les contenus de ce colloque

Autres communications du même congressiste :

Thème du colloque :

Physique et mathématiques

Sur l'équivalence de certaines formulations de la théorie des types

M. L'Abbé