In the semester just finished I have been snowed under revamping and teaching a big (300+ students) introductory course on Logic. If you are interested into how I have gone about that, have a look at the public-facing website for my course, where you will see my lecture slides, tutorial exercises, and exams. It was a great but rather demanding experience, and this blog has been allowed to lie fallow to compensate.

Now that this burden is off me, there is still teaching to do (introductory programming with Haskell) but this will not be so time consuming, and so I am from tomorrow returning to adding material to my blog, reviewing and commenting on highly cited work in my field, as suggested by Google Scholar’s top recommendations. The story so far, for those who wish to see my past writing in a convenient list:

• Proof Analysis in Modal Logic (2005), by Sara Negri
• An algebraic and Kripke-style approach to a certain extension of intuitionistic logic (1980), by Cecylia Rauszer
• A very modal model of a modern, major, general type system (2007), by Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon
• The MetaCoq Project (2020), by Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter
• First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory (2021), by Jonathan Sterling
• Nested Sequents for Intuitionistic Logics (2014), by Melvin Fitting
• Modal Logic (2001), by Patrick Blackburn, Maarten de Rijke, and Yde Venema
• On Intuitionistic Diamonds (and Lack Thereof) (2023), by Anupam Das and Sonia Marin
• A modality for recursion (2000), by Hiroshi Nakano
• On modal logic with an intuitionistic base (1977), by Gisèle Fischer Servi
• Associative n-Categories (2018), by Christopher Dorn
• A Mechanization of the Blakers–Massey Connectivity Theorem in Homotopy Type Theory (2016), by Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine
• Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions (2004), by Yves Bertot and Pierre Castéran
• Computational Types from a Logical Perspective (1998), by Nick Benton, Gavin Bierman, and Valeria de Paiva
• All (∞,1)-Toposes Have Strict Univalent Universes (2019), by Michael Shulman
• Proof Theory and Algebra in Logic (2019), by Hiroakira Ono
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2023), by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel
• Combining Classical and Intuitionistic Logic (1996), by Luis Fariñas del Cerro and Andreas Herzig
• Domain Theory (1994), by Samson Abramsky and Achim Jung
• 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