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.
• $𝜌\in Env:x_{𝜏}\mapsto 𝜌(x_{𝜏})\in ⟦𝜏⟧$
• Pour tout terme $u:𝜏$, pour tout env $𝜌$, on veut $⟦u⟧𝜌\in ⟦𝜏⟧$