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 a service for the community interested, via web search or likewise, in one of the topics I write about in logic, type theory, program semantics, category theory, and so on. For me, it is a discipline to keep me reading, and appreciating, new and older papers and books in the literature. Every week I look at the Update service of Google Scholar, which offers personalised recommendations of new literature ‘trained’ on my papers. I then look at the citations in those paper to pull out an older paper cited by multiple papers in my recommendations. In this way, I get a sense of the most important older work that underlies the relevant work of today. I then try to read these works (not always possible in detail in reasonable time if it is a multi-volume book or piece of software!) and write a few paragraphs about it as a blog post.

The good people at the Mastodon instance Fediscience.org are hosting this blog. Fediscience.org is an instance focused on working scientists, run by Frank Sonntag. If you’d like to follow me there, here I am, and if you’d like to the other blogs I share this space with, see here. Many thanks to Frank for setting this up for the community.

The remainder of this post are links to my writings on my old blog site. If you click back far enough you’ll find the earliest version of my blog focused on new literature, but I eventually decided that the older literature was more consistently satisfying and fun to write about, so I’ll only link to that material:

• Intuitionistic Type Theory (1984), by Per Martin-Löf
• Normalization for Multimodal Type Theory (2022), by Daniel Gratzer
• Multimodal Dependent Type Theory (2021), by Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal
• The Coq Proof Assistant (version of September 5 2022), by the Coq development team
• A Modal Analysis of Staged Computation (2001), by Rowan Davies and Frank Pfenning
• On the homotopy groups of spheres in homotopy type theory (2016), by Guillaume Brunerie
• Scalable Verification of Probabilistic Networks (2019), by Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva
• The Lean Theorem Prover (System Description) (2015), by Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer
• An Intuitionistic Theory of Types: Predicative Part (1975), by Per Martin-Löf
• Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom (2018), by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg
• The Simplicial Model of Univalent Foundations (after Voevodsky) (2021), by Krzysztof Kapulkin and Peter LeFanu Lumsdaine
• Internal Universes in Models of Homotopy Type Theory (2018), by Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters
• Horn Clause Solvers for Program Verification (2015), by Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko
• A Framework for Intuitionistic Modal Logics (Extended Abstract) (1986), by Gordon Plotkin and Colin Stirling
• Categories for the Working Mathematician (1998), by Saunders Mac Lane
• Sketches of an Elephant: A Topos Theory Compendium (2002), by Peter T. Johnstone
• Some Properties of Fib as a Fibred 2-category (1999), by Claudio Hermida
• The Proof Theory and Semantics of Intuitionistic Modal Logic (1994), by Alex K. Simpson
• First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees (2012), by Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring
• The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics (1996), by Arnon Avron
• Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (2017), by Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus
• Iris from the ground up: A modular foundation for higher-order concurrent separation logic (2018), by Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer
• Checking Interference with Fractional Permissions (2003), by John Boyland
• Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types (2006), by Amal Ahmed
• A Core Calculus of Dependency (1999), by Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke
• Structural Proof Theory (2001), by Sara Negri and Jan von Plato
• Separation Logic: A Logic for Shared Mutable Data Structures (2002), by John C. Reynolds
• Homotopy Type Theory: Univalent Foundations of Mathematics (2013), by The Univalent Foundations Program
• Notions of Computation and Monads (1991), by Eugenio Moggi
• Nominal Unification (2004), by Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay
• The Semantics and Proof Theory of the Logic of Bunched Implications (2002), by David J. Pym
• Linear Logic (1987), by Jean-Yves Girard
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972), by N. G. de Bruijn
• Nominal logic, a first order theory of names and binding (2003), by Andrew M. Pitts
• Display Logic (1982), by Nuel D. Belnap, Jr.
• A New Approach to Abstract Syntax with Variable Binding (2002), by Murdoch J. Gabbay and Andrew M. Pitts