mpri-mellies-cours-1

Modeles` des langages de programmationDomaines, categories,´ jeux` ´Programme de cette premiere seance:Modele` ensembliste du lambda-calcul ;Categor´ ies cartesiennes´ fermees´1´Plan de la seance´1— le-calcul simplement type,` ´2— le modele ensembliste du-calcul simplement type,3— la structure categor´ ique de Ens: categor´ ies et foncteurs,4— la structure categor´ ique de Ens: transformations naturelles et adjonctions,5— la structure categor´ ique de Ens: ccc,6— interpretation´ du-calcul simplement type´ dans une ccc,7— exemples de cccs.2I. Le-calcul simplement type´3´Curry 1958: le-calcul simplement typeIl est possible de typer certaines expressions du-calcul au moyen de types simplesA;Bconstruits par la grammaire:A;B ::=jA)B:On appelle contexte de typage une suite finie = ( x :A ;:::;x :A ) ou` x est unen n1 1 ivariable etA est un type simple, pour tout 1in.iOn appelle sequent´ un triplet:x :A ;:::;x :A ‘P :B1 1 n nou` x : A ;:::;x : A est un contexte de typage, P est un -terme et B est un type1 1 n nsimple.4´Curry 1958: le-calcul simplement typeVariablex :A‘x :A;x :A‘P :BAbstraction‘ x:P :A)B‘P :A)B ‘Q :AApplication; ‘PQ :B‘P :BAffaiblissement;x :A‘P :B;x :A;y :A‘P :BContraction;z :A‘P [x;y z] :B;x :A;y :B; ‘P :CPermutation;y :B;x :A; ‘P :C5Propriet´ es´ remarquables du fragment simplement type´´ ´Un-termeP est appele simplement type lorsqu’il existe un contexte de typage et untype simpleA tels que:‘P ...