Cours 7 : PCF

Plotkin et le PCF

PCF :

Prototype de langage comme CamL, Pascal.

Papier rédigé par Plotkin, qui s’est posé le problème et l’a résolu d’un coup.

LCF :

L’ancêtre de Coq

Plotkin se rend compte qu’il y avait un langage de programmation dans LCF, qui était un ancêtre de ML

⟶ étude de ce langage, sémantique opérationnelle / dénotationnelle, etc…

---

• Soit $⟦𝜏⟧$ un dcpo.
• $𝜌∈Env : x_𝜏 \mapsto 𝜌(x_𝜏) ∈⟦𝜏⟧$
• Pour tout terme $u:𝜏$, pour tout env $𝜌$, on veut \(⟦u⟧𝜌∈⟦𝜏⟧\)