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 ...
Proprie´t´esremarquablesdufragmentsimplementtyp´e Unλ-termeP´eatseleppsimplement type´lorsqu’il existe un contexte de typageΓet un type simpleAtels que:
Logique constructive: monstrationL’assistant de de´CoQevd´´p`elepoRNAIlaI’as´eestb sur un langage de type extreˆ mement raffine´ , avec des typespolymoprehsetde´ pendants. Permet dectiereicfir monstration et d’enune de´extriaerun programme OCaml.
Logique classique:La logique classique est aussi constructive! a` condition d’ajouter un ´ teur de controˆ lecc-llactaynasalduxe`λmetdrpertreemetL.o’cllutaue´preca-opera enm´emoirel’environnementduλ(= la pile, la continuation) et d’y revenir plus tard-terme dans l’e´ valuation.
Interpre´ tation ensembliste On associe un ensembleXαmoqieuuetypeat`achaqα. Ensuite,one´tendl’interpr´etation`atouslestypes: [α]=Xα[A⇒B]=[B][A]=HomEns([A],[B])