Tag: 2023
-
Discussing “On Intuitionistic Diamonds (and Lack Thereof)”
I choose papers for this blog by looking at the most cited papers in my Google Scholar recommendations of recent papers. This week, my algorithm has read my mind by recommending a fairly new paper that was already at the top of my list of papers to read. Its topic, as with a few papers…
-
Discussing “Isabelle/HOL: A Proof Assistant for Higher-Order Logic”
In the world of interactive theorem provers two systems stand out for their maturity and wide adoption. One is Rocq, until recently known as Coq, about which I have written previously; Isabelle/HOL, the topic of this week’s reading, is the other. Rocq is one of a number of systems (for example, Lean) based on Martin-Löf’s…
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