---
res:
  bibo_abstract:
  - "Prior work on multi-language program verification has achieved impressive results,
    including the compositional verification of complex compilers. But the existing
    approaches to this problem impose a variety of restrictions on the overall structure
    of multi-language programs (e.g. fixing the source language, fixing the set of
    involved languages, fixing the memory model, or fixing the semantics of interoperation).
    In this paper, we explore the problem of how to avoid such global restrictions.\r\nConcretely,
    we present DimSum: a new, decentralized approach to multi-language semantics and
    verification, which we have implemented in the Coq proof assistant. Decentralization
    means that we can define and reason about languages independently from each other
    (as independent modules communicating via events), but also combine and translate
    between them when necessary (via a library of combinators).\r\nWe apply DimSum
    to a high-level imperative language Rec (with an abstract memory model and function
    calls), a low-level assembly language Asm (with a concrete memory model, arbitrary
    jumps, and syscalls), and a mathematical specification language Spec. We evaluate
    DimSum on two case studies: an Asm library extending Rec with support for pointer
    comparison, and a coroutine library for Rec written in Asm. In both cases, we
    show how DimSum allows the Asm libraries to be abstracted to Rec-level specifications,
    despite the behavior of the Asm libraries not being syntactically expressible
    in Rec itself. We also verify an optimizing multi-pass compiler from Rec to Asm,
    showing that it is compatible with these Asm libraries.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Michael Joachim
      foaf_name: Sammler, Michael Joachim
      foaf_surname: Sammler
      foaf_workInfoHomepage: http://www.librecat.org/personId=510d3901-2a03-11ee-914d-d9ae9011f0a7
  - foaf_Person:
      foaf_givenName: Simon
      foaf_name: Spies, Simon
      foaf_surname: Spies
  - foaf_Person:
      foaf_givenName: Youngju
      foaf_name: Song, Youngju
      foaf_surname: Song
  - foaf_Person:
      foaf_givenName: Emanuele
      foaf_name: D'Osualdo, Emanuele
      foaf_surname: D'Osualdo
  - foaf_Person:
      foaf_givenName: Robbert
      foaf_name: Krebbers, Robbert
      foaf_surname: Krebbers
  - foaf_Person:
      foaf_givenName: Deepak
      foaf_name: Garg, Deepak
      foaf_surname: Garg
  - foaf_Person:
      foaf_givenName: Derek
      foaf_name: Dreyer, Derek
      foaf_surname: Dreyer
  bibo_doi: 10.1145/3571220
  bibo_issue: POPL
  bibo_volume: 7
  dct_date: 2023^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/2475-1421
  dct_language: eng
  dct_publisher: Association for Computing Machinery@
  dct_title: 'DimSum: A decentralized approach to multi-language semantics and verification@'
...