appel_vst_2011:
  type: article
  title: Verified {Software} {Toolchain}
  author: Appel, Andrew W.
  date: 2011
  note: Separation logic for Clight, sound against CompCert's semantics; the logic is a client of the compiler, not a component of it.
  parent:
    type: proceedings
    title: Programming {Languages} and {Systems} ({ESOP} 2011)
    publisher: Springer
    parent:
      type: proceedings
      title: Lecture {Notes} in {Computer} {Science}