Tag: 2007
-
Discussing “A semantics for concurrent separation logic”
This paper is not only cited in my recent Google Scholar recommendations (which is how I choose papers to read for my blog), but is, along with the Peter O’Hearn paper it builds on, the winner of the 2016 Gödel Prize. This prize, although nominally for any “outstanding papers in the area of theoretical computer…
-
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 “A semantics for concurrent separation logic”
- Discussing “Z3: An Efficient SMT Solver”
- Discussing “BI as an Assertion Language for Mutable Data Structures”
- Discussing “Sheaves in Geometry and Logic”
Tags
1994 1996 2000 2001 2007 2014 2019 2021 2023 Abhishek Anand Andrew W. Appel Bedrock Systems Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University Christopher D. Richards City University of New York Coq Cubical Type Theory Cyril Cohen Côte d'Azur University Inria Nantes INRIA Rocquencourt intuitionistic logic intuitionistic modal logic Journal of Automated Reasoning LICS Matthieu Sozeau Metaprogramming modal logic Notre Dame Journal of Formal Logic Paul-André Melliès POPL Princeton University Proof theory Rocq Saarland University Simon Boulier Théo Winterhalter types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva