Category: Summaries
-
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,…
-
Discussing “Associative n-Categories”
I have looked at PhD dissertations for this blog before, but never one this gargantuan; at 503 pages it weighs in at 3-4 times longer than the average thesis. The author does not quite apologise for the length, but at least acknowledges it, saying “[the] length of this thesis should by no means deter the…
-
Discussing “A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory”
I first became aware of this paper from a long and fascinating blog comment thread in which mathematicians argued about the utility, or lack thereof, of homotopy type theory for homotopy theorists. Urs Schreiber, arguing for team HoTT, held up this paper an exemplar of the value of the type theoretical approach, saying “it was…
-
Discussing “Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions”
I’ve written before about the Coq Proof Assistant . Since then, after years of bravely ignoring the sniggers its French name produced among English speakers, the developers have decided to remain it Rocq in honour of Rocquencourt, the French town in which much of the development took place. The good news for the authors of…
-
Discussing “Computational Types from a Logical Perspective”
This is a sequel to a paper by Moggi that I discussed some time ago. That paper discussed side effects, which are, roughly speaking, anything interesting that a program does other than map inputs deterministically to outputs, such as failure to terminate with a value, taking in user input, or producing output before the computation…
-
Discussing “All (∞,1)-Toposes Have Strict Univalent Universes”
I have written before about 2-category theory, where we have objects, arrows between objects, and arrows (sometimes called 2-cells) between those arrows. The canonical example are collections of categories, which have layers of categories; functors; and natural transformations. ∞-categories generalise this to an infinite stack of layers of n-cells. An (∞,1)-category is a special case…
-
Discussing “Proof Theory and Algebra in Logic”
I was pleased to see this book bubbling up through my recommendations, as I once saw a keynote talk by Hiroakira Ono at a logic conference in my former home city of Wellington and it was one of the most cogent and exciting logic talks I’ve ever enjoyed. Ono’s textbook is split into two parts,…
-
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…
-
Discussing “Combining Classical and Intuitionistic Logic”
This short but fun little paper discusses how we can combine two different logics – classical and intuitionistic – into one. Classical logic is the logic of Boole where every proposition has a definite value of True or False and negation simply inverts the value, so that ‘p or not p’ holds for any proposition…
Categories
Recent Posts
- Discussing “Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic”
- Discussing “Basic Proof Theory”
- A Blog Update for 2025
- Discussing “Proof Analysis in Modal Logic”
Tags
1996 2000 2001 2014 2019 2020 2021 2023 Abhishek Anand Cambridge Tracts in Theoretical Computer Science Carnegie Mellon University City University of New York Coq Cubical Type Theory Cyril Cohen Fabian Kunze intuitionistic logic intuitionistic modal logic Jonathan Sterling Journal of Automated Reasoning LICS LORIA Maarten de Rijke Matthieu Sozeau Melvin Fitting Metaprogramming modal logic nested sequent calculus Notre Dame Journal of Formal Logic Patrick Blackburn Princeton University Proof theory Rocq sequent calculus Simon Boulier TABLEAUX types type theory University of Amsterdam University of Birmingham University of Cambridge University of Oxford Valeria de Paiva Yannick Forster Yde Venema