A higher-order logic for concurrent termination-preserving refinement

Joseph Tassarotti, Ralf Jung, Robert Harper

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Compiler correctness proofs for higher-order concurrent languages are difficult: they involve establishing a termination-preserving refinement between a concurrent high-level source language and an implementation that uses low-level shared memory primitives. However, existing logics for proving concurrent refinement either neglect properties such as termination, or only handle first-order state. In this paper, we address these limitations by extending Iris, a recent higher-order concurrent separation logic, with support for reasoning about termination-preserving refinements. To demonstrate the power of these extensions, we prove the correctness of an efficient implementation of a higher-order, session-typed language. To our knowledge, this is the first program logic capable of giving a compiler correctness proof for such a language. The soundness of our extensions and our compiler correctness proof have been mechanized in Coq.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
EditorsHongseok Yang
PublisherSpringer Verlag
Pages909-936
Number of pages28
ISBN (Print)9783662544334
DOIs
StatePublished - 2017
Event26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden
Duration: Apr 22 2017Apr 29 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10201 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
Country/TerritorySweden
City Uppsala
Period4/22/174/29/17

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A higher-order logic for concurrent termination-preserving refinement'. Together they form a unique fingerprint.

Cite this