{"id":7,"date":"2024-01-06T06:00:43","date_gmt":"2024-01-06T06:00:43","guid":{"rendered":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/?p=7"},"modified":"2024-01-06T06:02:08","modified_gmt":"2024-01-06T06:02:08","slug":"welcome-to-the-updated-scholar","status":"publish","type":"post","link":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/2024\/01\/06\/welcome-to-the-updated-scholar\/","title":{"rendered":"Welcome to The Updated Scholar!"},"content":{"rendered":"\n<p>Welcome to the new version of my blog The Updated Scholar, <a href=\"https:\/\/updatedscholar.blogspot.com\/\">previously hosted by blogspot<\/a>.<\/p>\n\n\n\n<figure class=\"wp-block-image size-full is-resized\"><img loading=\"lazy\" decoding=\"async\" width=\"588\" height=\"882\" src=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-content\/uploads\/sites\/10\/2024\/01\/RanaldClouston.png\" alt=\"Photo of bearded Caucasian man with short hair, smiling\" class=\"wp-image-9\" style=\"width:267px;height:auto\" srcset=\"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-content\/uploads\/sites\/10\/2024\/01\/RanaldClouston.png 588w, https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-content\/uploads\/sites\/10\/2024\/01\/RanaldClouston-200x300.png 200w\" sizes=\"auto, (max-width: 588px) 100vw, 588px\" \/><\/figure>\n\n\n\n<p>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 <a href=\"https:\/\/scholar.google.com.au\/\">Google Scholar<\/a>, which offers personalised recommendations of new literature &#8216;trained&#8217; on <a href=\"https:\/\/scholar.google.com.au\/citations?user=_7YKlyMAAAAJ\">my papers<\/a>. 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.<\/p>\n\n\n\n<p>The good people at the <a href=\"https:\/\/joinmastodon.org\/\">Mastodon<\/a> instance <a href=\"https:\/\/fediscience.org\" data-type=\"link\" data-id=\"https:\/\/fediscience.org\">Fediscience.org<\/a> are hosting this blog. Fediscience.org is an instance focused on working scientists, run by <a href=\"https:\/\/fediscience.org\/@FrankSonntag\">Frank Sonntag<\/a>. If you&#8217;d like to follow me there, <a href=\"https:\/\/fediscience.org\/@RanaldClouston\">here I am<\/a>, and if you&#8217;d like to the other blogs I share this space with, see <a href=\"https:\/\/blogs.fediscience.org\/blogs\/\">here<\/a>. Many thanks to Frank for setting this up for the community.<\/p>\n\n\n\n<p>The remainder of this post are links to my writings on my old blog site. If you click back far enough you&#8217;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&#8217;ll only link to that material:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\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>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 [&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":[4],"class_list":["post-7","post","type-post","status-publish","format-standard","hentry","category-meta","tag-introduction"],"share_on_mastodon":{"url":"","error":""},"_links":{"self":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/7","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=7"}],"version-history":[{"count":1,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/7\/revisions"}],"predecessor-version":[{"id":10,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/posts\/7\/revisions\/10"}],"wp:attachment":[{"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/media?parent=7"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/categories?post=7"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/blogs.fediscience.org\/the-updated-scholar\/wp-json\/wp\/v2\/tags?post=7"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}