Tag: POPL
-
Discussing “BI as an Assertion Language for Mutable Data Structures”
I’ve written about separation logic and bunched implications for the blog before. This was the paper that brought these topics together. It constitutes a very important middle step in the early development of separation logic between Reynolds’s 2000 “Intuitionistic Reasoning about Shared Mutable Data Structures” and his 2002 “Separation Logic: A Logic for Shared Mutable…
-
Discussing “A very modal model of a modern, major, general type system”
This paper is an influential landmark in the development of what is now usually called guarded recursion, following a trail that roughly goes from Nakano’s introduction of the approximation modality, to this paper, to a Dreyer, Ahmed, and Birkedal paper that I haven’t yet read for this blog but will probably eventually get to, to…
Categories
Recent Posts
- Discussing “BI as an Assertion Language for Mutable Data Structures”
- Discussing “Sheaves in Geometry and Logic”
- Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic”
- Discussing “Basic Proof Theory”
Tags
1994 1996 2000 2001 2014 2019 2020 2021 2023 Bedrock Systems Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University City University of New York Coq Cubical Type Theory Cyril Cohen Côte d'Azur University Fabian Kunze Gregory Malecha Inria Nantes intuitionistic logic intuitionistic modal logic Jonathan Sterling LICS Melvin Fitting Metaprogramming modal logic nested sequent calculus Nicolas Tabareau Notre Dame Journal of Formal Logic POPL Proof theory Rocq Saarland University sequent calculus Simon Boulier Théo Winterhalter types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva Yannick Forster