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⟧𝜌∈⟦𝜏⟧\)

Leave a comment