leroy_pottier_relsep_2026:
  type: misc
  title: Relational {Separation} {Logic} for {Compiler} {Verification}
  author:
  - Leroy, Xavier
  - Pottier, François
  date: 2026-01
  url: https://cambium.inria.fr/~fpottier/stages/sujet2026-m2.pdf
  note: Asks whether semantic preservation for a compilation pass F can be expressed as a relational triple {P} F(c) <= c {Q}.