-
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…
-
Discussing “Domain Theory”
Domains are certain forms of ordered sets used to address problems in the denotational semantics (mathematical interpretation) of programming languages. The area was invented by Dana Scott in a series of papers starting in 1969, building on earlier work by many others that used lattices. This book (which admittedly, I did not have time to…
-
Welcome to The Updated Scholar!
Welcome to the new version of my blog The Updated Scholar, previously hosted by blogspot. This blog exists mostly for me, and perhaps also as […]
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