SteelCore: an extensible concurrent separation logic for effectful dependently typed programs

Abstract

Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself.

Document Details

Document Type
Pub Defense Publication
Publication Date
Aug 02, 2020
Source ID
10.1145/3409003

Entities

People

  • Aseem Rastogi
  • Aymeric Fromherz
  • Danel Ahman
  • Denis Merigoux
  • Guido Martínez
  • Nikhil Swamy

Organizations

  • Carnegie Mellon University
  • FP7 Ideas: European Research Council
  • Institut National de Recherche en Informatique et en Automatique
  • Microsoft
  • Office of Naval Research
  • University of Ljubljana

Tags

Readers

  • Computational Linguistics
  • Theoretical Analysis.