De rien messieurs, j'espère n'avoir pas été trop confus, ni trop abstrait dans ma présentation. Je viens de commencer la thèse de Perthmâd, et dans ses prolégomènes vous pourrez y trouver une exposition plus détaillée du sujet. On y trouve en particulier :
les règles de typage du lambda calcul simplement typé (sans variants, ni tuples) à la page 25 ;
celles du lambda-calcul avec variants et tuples à la page 27 ;
les règles d'inférences de la logique propositionnelle intuitionniste page 30.
Puis en haut de la page 33, il montre l'identité formelle entre deux sous-ensembles de ces règles (ce en quoi consiste la correspondance de Curry-Howard) sous la forme d'un tableau de deux lignes et quatre colonnes (la quatrième correspondant à ce que j'ai dit au sujet du modus ponens). Pour les autres règles, il vous suffit de les comparer vous même.
Quelques compléments pourront vous être utiles pour comprendre certaines de ses notations. D'abord sur le lambda-calcul, vous n'avez qu'à lire le lambda-terme Lx.t (le L remplace le lambda minuscule) comme l'expression OCaml fun x -> t. Enfin pour ce qui est du lien entre multiplication-conjonction et addition-disjonction (type produit et type somme), constatez que A et (B ou C) = (A et B) ou (A et C) : loi de distribution comme dans les anneaux. Cette idée vient de la théorie générale des algèbres de Boole que l'on peut définir comme des corps dans lesquels tout élément est son propre carré (A et A = A) : l'algèbre de Boole a deux éléments (true et false) étant la plus simple de toutes.
Pour information, le principe de cette correspondance peut être étendu au typage de protocole réseau. Le prix jeune chercheur INRIA a été attribué à Véronique Cortier qui travaille, entre autre, sur le projet Belenios (système sécurisé de vote en ligne); système qui cherche un développeur OCaml pour le développement de sa plateforme Web : c'est pas un truc cool en France ?! ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Le web
Posté par kantien . En réponse au journal Qui fait des trucs "cools" en France et en Europe?. Évalué à 3.
De rien messieurs, j'espère n'avoir pas été trop confus, ni trop abstrait dans ma présentation. Je viens de commencer la thèse de Perthmâd, et dans ses prolégomènes vous pourrez y trouver une exposition plus détaillée du sujet. On y trouve en particulier :
Puis en haut de la page 33, il montre l'identité formelle entre deux sous-ensembles de ces règles (ce en quoi consiste la correspondance de Curry-Howard) sous la forme d'un tableau de deux lignes et quatre colonnes (la quatrième correspondant à ce que j'ai dit au sujet du modus ponens). Pour les autres règles, il vous suffit de les comparer vous même.
Quelques compléments pourront vous être utiles pour comprendre certaines de ses notations. D'abord sur le lambda-calcul, vous n'avez qu'à lire le lambda-terme
Lx.t(le L remplace le lambda minuscule) comme l'expression OCamlfun x -> t. Enfin pour ce qui est du lien entre multiplication-conjonction et addition-disjonction (type produit et type somme), constatez queA et (B ou C) = (A et B) ou (A et C): loi de distribution comme dans les anneaux. Cette idée vient de la théorie générale des algèbres de Boole que l'on peut définir comme des corps dans lesquels tout élément est son propre carré (A et A = A) : l'algèbre de Boole a deux éléments (trueetfalse) étant la plus simple de toutes.Pour information, le principe de cette correspondance peut être étendu au typage de protocole réseau. Le prix jeune chercheur INRIA a été attribué à Véronique Cortier qui travaille, entre autre, sur le projet Belenios (système sécurisé de vote en ligne); système qui cherche un développeur OCaml pour le développement de sa plateforme Web : c'est pas un truc cool en France ?! ;-)
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.