-
Discussing “Proof Analysis in Modal Logic”
Modal logics of necessity and possibility do not always obviously admit an acceptable notion of structural proof theory. Yet such systems can be invaluable for both work inside the logic (proof search) and work about a logic (metatheory). This paper looks at a general framework for defining sequent calculi for a wide range of classical…
-
Discussing “An algebraic and Kripke-style approach to a certain extension of intuitionistic logic”
Heyting-Brouwer logic (more commonly known now as bi-intuitionistic logic) has fascinated me since I first learned of it. The idea is beguilingly simple: extend intuitionistic logic with a new connective that makes it completely symmetrical. The ‘symmetry’ I am thinking of (perhaps better called ‘duality’, but not quite the same thing as De Morgan duality)…
-
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…
-
Discussing “The MetaCoq Project”
I’ve written before about Coq, recently renamed to Rocq, a proof assistant based on Martin-Löf’s dependent type theory. This paper, along with various sequels written in the six years since the project was first announced, aims to mechanise the syntax and semantics of Rocq, in Rocq.
-
Discussing “First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory”
I’ve been meaning to get more familiar with this dissertation for a while (reading it thoroughly would take longer than the week I try to take for my blog posts), after its ideas were used in a paper I discussed last year. This thesis presents a new technique, synthetic Tait computability, for proving the ‘syntactic’…
-
Discussing “Nested Sequents for Intuitionistic Logics”
About a year and a half ago I wrote about hypersequents, a modification of the tried and trusted sequent calculus approach to structural proof theory. In that setting, instead of working with a single sequent (a set of premises alongside a set of possible conclusions) we work with a list of sequents. In this paper,…
-
Discussing “Modal Logic”
I learned modal logic from a book by Hughes and Cresswell, a pair of philosophers from my home city of Wellington, so it was interesting for me to see the very different approach taken in this week’s book, which is now the standard reference for the field ( along with the Chargrov- Zakharyaschev book of…
-
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 “A modality for recursion”
The algorithm I use to choose reading for this blog, pulling the most cited papers out of my Google Scholar recommendations of new papers, sometimes pops out work close to my heart; quite a few years of my own research have been direct outshoots from this paper, following its adoption by Birkedal et al., and…
-
Discussing “On modal logic with an intuitionistic base”
There is a mini-theme on this blog of important developments in intuitionistic modal logic, in which the modal notion of necessity (and, less often, possibility) is blended with the intuitionistic notion of constructive proofs which denies, for example, the law of the excluded middle. We’ve read through Plotkin and Stirling, Simpson, Davies and Pfenning, and,…
Categories
Recent Posts
- Discussing “Proof Analysis in Modal Logic”
- Discussing “An algebraic and Kripke-style approach to a certain extension of intuitionistic logic”
- Discussing “A very modal model of a modern, major, general type system”
- Discussing “The MetaCoq Project”
Tags
2000 2001 2007 2014 2019 2020 2021 2023 Anupam Das Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University Christopher D. Richards City University of New York Coq Cubical Type Theory Guarded recursion Hiroshi Nakano INRIA Rocquencourt intuitionistic logic intuitionistic modal logic Jonathan Sterling LICS LORIA Maarten de Rijke Melvin Fitting Metaprogramming modal logic nested sequent calculus Notre Dame Journal of Formal Logic Patrick Blackburn POPL Princeton University Rocq Ryukoku University sequent calculus Sonia Marin TABLEAUX types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Université Paris 7 Yde Venema