SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
Mon 24 Aug 2020 23:15 - 23:30 at ICFP Asia 1 - Asia 1 Chair(s): Adam Chlipala
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.
Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F* proof assistant in a manner that enables dependently typed, effectful F* programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL.
In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the \emph{effectful} semantics of non-deterministically interleaved atomic actions.
Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming.
Mon 24 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
11:30 - 13:00: New York 1ICFP Program at ICFP NY 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
11:30 - 11:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
11:45 - 12:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
12:00 - 12:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
12:15 - 12:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
12:30 - 12:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
12:45 - 13:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached |
22:30 - 00:00: Asia 1ICFP Program at ICFP Asia 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
22:30 - 22:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
22:45 - 23:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
23:00 - 23:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
23:15 - 23:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
23:30 - 23:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
23:45 - 00:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached |