@misc{leroy_pottier_relsep_2026,
 title = {Relational {Separation} {Logic} for {Compiler} {Verification}},
 author = {Leroy, Xavier and Pottier, Fran\c{c}ois},
 year = {2026},
 month = {January},
 howpublished = {M2 research internship proposal, Coll\`ege de France and Inria Paris},
 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}.}
}