@inproceedings{tassarotti_jung_harper_2017,
 title = {A {Higher}-{Order} {Logic} for {Concurrent} {Termination}-{Preserving} {Refinement}},
 author = {Tassarotti, Joseph and Jung, Ralf and Harper, Robert},
 year = {2017},
 booktitle = {Programming {Languages} and {Systems} ({ESOP} 2017)},
 series = {Lecture {Notes} in {Computer} {Science}},
 publisher = {Springer},
 note = {Iris-based relational separation logic used to verify a compiler from a session-typed channel language into a language with references.}
}