{"id":112,"date":"2025-08-07T06:54:39","date_gmt":"2025-08-07T06:54:39","guid":{"rendered":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/?p=112"},"modified":"2025-08-07T06:54:39","modified_gmt":"2025-08-07T06:54:39","slug":"a-blog-update-for-2025","status":"publish","type":"post","link":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2025\/08\/07\/a-blog-update-for-2025\/","title":{"rendered":"A Blog Update for 2025"},"content":{"rendered":"\n<p>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 <a href=\"https:\/\/comp.anu.edu.au\/courses\/comp2620\/news\/index.html\" data-type=\"link\" data-id=\"https:\/\/comp.anu.edu.au\/courses\/comp2620\/news\/index.html\">the public-facing website for my course<\/a>, 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. <\/p>\n\n\n\n<p>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&#8217;s top recommendations. The story so far, for those who wish to see my past writing in a convenient list:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/24\/discussing-proof-analysis-in-modal-logic\/\">Proof Analysis in Modal Logic<\/a> (2005), by Sara Negri<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/15\/discussing-an-algebraic-and-kripke-style-approach-to-a-certain-extension-of-intuitionistic-logic\/\">An algebraic and Kripke-style approach to a certain extension of intuitionistic logic<\/a> (1980), by Cecylia Rauszer<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/09\/discussing-a-very-modal-model-of-a-modern-major-general-type-system\/\">A very modal model of a modern, major, general type system<\/a> (2007), by Andrew W. Appel, Paul-Andr\u00e9 Melli\u00e8s, Christopher D. Richards, and J\u00e9r\u00f4me Vouillon<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/07\/discussing-the-metacoq-project\/\">The MetaCoq Project<\/a> (2020), by Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Th\u00e9o Winterhalter<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/05\/03\/discussing-first-steps-in-synthetic-tait-computability-the-objective-metatheory-of-cubical-type-theory\/\">First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory<\/a> (2021), by Jonathan Sterling<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/04\/24\/discussing-nested-sequents-for-intuitionistic-logics\/\" data-type=\"link\" data-id=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/04\/24\/discussing-nested-sequents-for-intuitionistic-logics\/\">Nested Sequents for Intuitionistic Logics<\/a> (2014), by Melvin Fitting<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/04\/23\/discussing-modal-logic\/\">Modal Logic<\/a> (2001), by Patrick Blackburn, Maarten de Rijke, and Yde Venema<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/04\/05\/discussing-on-intuitionistic-diamonds-and-lack-thereof\/\">On Intuitionistic Diamonds (and Lack Thereof)<\/a> (2023), by Anupam Das and Sonia Marin<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/28\/discussing-a-modality-for-recursion\/\">A modality for recursion<\/a> (2000), by Hiroshi Nakano<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/22\/discussing-on-modal-logic-with-an-intuitionistic-base\/\">On modal logic with an intuitionistic base<\/a> (1977), by Gis\u00e8le Fischer Servi<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/20\/discussing-associative-n-categories\/\" data-type=\"link\" data-id=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/20\/discussing-associative-n-categories\/\">Associative n-Categories<\/a> (2018), by Christopher Dorn<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/15\/discussing-a-mechanization-of-the-blakers-massey-connectivity-theorem-in-homotopy-type-theory\/\">A Mechanization of the Blakers\u2013Massey Connectivity Theorem in Homotopy Type Theory<\/a> (2016), by Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/03\/06\/discussing-interactive-theorem-proving-and-program-development-coqart-the-calculus-of-inductive-constructions\/\">Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions<\/a> (2004), by Yves Bertot and Pierre Cast\u00e9ran<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/27\/discussing-computational-types-from-a-logical-perspective\/\">Computational Types from a Logical Perspective<\/a> (1998), by Nick Benton, Gavin Bierman, and Valeria de Paiva<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/15\/discussing-all-%e2%88%9e1-toposes-have-strict-univalent-universes\/\">All (\u221e,1)-Toposes Have Strict Univalent Universes<\/a> (2019), by Michael Shulman<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/09\/discussing-proof-theory-and-algebra-in-logic\/\" data-type=\"link\" data-id=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/09\/discussing-proof-theory-and-algebra-in-logic\/\">Proof Theory and Algebra in Logic<\/a> (2019), by Hiroakira Ono<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/04\/discussing-isabelle-hol-a-proof-assistant-for-higher-order-logic\/\" data-type=\"link\" data-id=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/02\/04\/discussing-isabelle-hol-a-proof-assistant-for-higher-order-logic\/\">Isabelle\/HOL: A Proof Assistant for Higher-Order Logic<\/a> (2023), by Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/01\/17\/discussing-combining-classical-and-intuitionistic-logic\/\" data-type=\"link\" data-id=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/01\/17\/discussing-combining-classical-and-intuitionistic-logic\/\">Combining Classical and Intuitionistic Logic<\/a> (1996), by Luis Fari\u00f1as del Cerro and Andreas Herzig<\/li>\n\n\n\n<li><a href=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/01\/12\/discussing-domain-theory\/\">Domain Theory<\/a> (1994), by Samson Abramsky and Achim Jung<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2024\/01\/discussing-intuitionistic-type-theory.html\">Intuitionistic Type Theory<\/a> (1984), by Per Martin-L\u00f6f<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/04\/discussing-normalization-for-multimodal.html\">Normalization for Multimodal Type Theory<\/a> (2022), by Daniel Gratzer<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/03\/dicussing-multimodal-dependent-type.html\">Multimodal Dependent Type Theory<\/a> (2021), by Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/03\/discussing-coq-proof-assistant.html\">The Coq Proof Assistant<\/a> (version of September 5 2022), by the Coq development team<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/02\/discussing-modal-analysis-of-staged.html\">A Modal Analysis of Staged Computation<\/a> (2001), by Rowan Davies and Frank Pfenning<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/02\/discussing-on-homotopy-groups-of.html\">On the homotopy groups of spheres in homotopy type theory<\/a> (2016), by Guillaume Brunerie<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/02\/discussing-scalable-verification-of.html\">Scalable Verification of Probabilistic Networks<\/a> (2019), by Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/02\/discussing-lean-theorem-prover-system.html\">The Lean Theorem Prover (System Description)<\/a> (2015), by Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/01\/discussing-intuitionistic-theory-of.html\">An Intuitionistic Theory of Types: Predicative Part<\/a> (1975), by Per Martin-L\u00f6f<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/01\/discussing-cubical-type-theory.html\">Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom<\/a> (2018), by Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2023\/01\/discussing-simplicial-model-of.html\">The Simplicial Model of Univalent Foundations (after Voevodsky)<\/a> (2021), by Krzysztof Kapulkin and Peter LeFanu Lumsdaine<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/12\/discussing-internal-universes-in-models.html\">Internal Universes in Models of Homotopy Type Theory<\/a> (2018), by Daniel R. Licata, Ian Orton, Andrew M. Pitts, and Bas Spitters<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/12\/discussing-horn-clause-solvers-for.html\">Horn Clause Solvers for Program Verification<\/a> (2015), by Nikolaj Bj\u00f8rner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/11\/discussing-framework-for-intuitionistic.html\">A Framework for Intuitionistic Modal Logics (Extended Abstract)<\/a> (1986), by Gordon Plotkin and Colin Stirling<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/11\/discussing-categories-for-working.html\">Categories for the Working Mathematician<\/a> (1998), by Saunders Mac Lane<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/11\/discussing-sketches-of-elephant-topos.html\">Sketches of an Elephant: A Topos Theory Compendium<\/a> (2002), by Peter T. Johnstone<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/11\/discussing-some-properties-of-fib-as.html\">Some Properties of Fib as a Fibred 2-category<\/a> (1999), by Claudio Hermida<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/11\/discussing-proof-theory-and-semantics.html\">The Proof Theory and Semantics of Intuitionistic Modal Logic<\/a> (1994), by Alex K. Simpson<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/10\/discussing-first-steps-in-synthetic.html\">First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees<\/a> (2012), by Lars Birkedal, Rasmus Ejlers M\u00f8gelberg, Jan Schwinghammer, and Kristian St\u00f8vring<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/10\/discussing-method-of-hypersequents-in.html\">The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics<\/a> (1996), by Arnon Avron<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/10\/discussing-partiality-revisited.html\">Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type<\/a> (2017), by Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/10\/discussing-iris-from-ground-up-modular.html\">Iris from the ground up: A modular foundation for higher-order concurrent separation logic<\/a> (2018), by Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/09\/discussing-checking-interference-with.html\">Checking Interference with Fractional Permissions<\/a> (2003), by John Boyland<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/09\/discussing-step-indexed-syntactic.html\">Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types<\/a> (2006), by Amal Ahmed<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/09\/discussing-core-calculus-of-dependency.html\">A Core Calculus of Dependency<\/a> (1999), by Mart\u00edn Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/09\/discussing-structural-proof-theory.html\">Structural Proof Theory<\/a> (2001), by Sara Negri and Jan von Plato<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/08\/discussing-separation-logic-logic-for.html\">Separation Logic: A Logic for Shared Mutable Data Structures<\/a> (2002), by John C. Reynolds<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/08\/discussing-homotopy-type-theory.html\">Homotopy Type Theory: Univalent Foundations of Mathematics<\/a> (2013), by The Univalent Foundations Program<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2022\/08\/discussing-notions-of-computation-and.html\">Notions of Computation and Monads<\/a> (1991), by Eugenio Moggi<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/12\/discussing-nominal-unification.html\">Nominal Unification<\/a> (2004), by Christian Urban, Andrew M. Pitts, and Murdoch J. Gabbay<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/12\/discussing-semantics-and-proof-theory.html\">The Semantics and Proof Theory of the Logic of Bunched Implications<\/a> (2002), by David J. Pym<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/12\/discussing-linear-logic.html\">Linear Logic<\/a> (1987), by Jean-Yves Girard<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/11\/discussing-lambda-calculus-notation.html\">Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem<\/a> (1972), by N. G. de Bruijn<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/11\/discussing-nominal-logic-first-order.html\">Nominal logic, a first order theory of names and binding<\/a> (2003), by Andrew M. Pitts<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/11\/discussing-display-logic.html\">Display Logic<\/a> (1982), by Nuel D. Belnap, Jr.<\/li>\n\n\n\n<li><a href=\"https:\/\/updatedscholar.blogspot.com\/2014\/11\/discussing-new-approach-to-abstract.html\">A New Approach to Abstract Syntax with Variable Binding<\/a> (2002), by Murdoch J. Gabbay and Andrew M. Pitts<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"author":10,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":"","_share_on_mastodon":"0","_share_on_mastodon_status":"%title% %permalink%"},"categories":[3],"tags":[],"class_list":["post-112","post","type-post","status-publish","format-standard","hentry","category-meta"],"share_on_mastodon":{"url":"","error":""},"_links":{"self":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/112","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/users\/10"}],"replies":[{"embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/comments?post=112"}],"version-history":[{"count":1,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/112\/revisions"}],"predecessor-version":[{"id":113,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/112\/revisions\/113"}],"wp:attachment":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media?parent=112"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/categories?post=112"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/tags?post=112"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}