Lingolol

Jesper Agdakx 🔸So I was going through the <a class="u-url mention" href="https://mastodon.acm.org/@icfp_conference" rel="nofollow noopener" target="_blank">@icfp_conference</a> papers of this year and I wanted to highlight a few that I thought are really cool. So here we go! First up is "Type Theory in Type Theory using a Strictified Syntax" by Ambrus Kaposi and Loïc Pujet. Doing formal metatheory of type theory in type theory is notoriously hard but this paper tackles one of the key annoyances which is dealing with substitutions in a way that they commute with the syntax constructors. Even if you're not interested in the technical details, the introduction provides a very nice and approachable (*) overview of different approaches and the problems faced by each of them. (*) except for the paragraph starting with "A short technical summary for category theorists", which I can only dream of understanding one day. <a href="https://dl.acm.org/doi/10.1145/3747535" rel="nofollow noopener" target="_blank">dl.acm.org/doi/10.1145/3747535</a> <a class="hashtag" href="https://agda.club/tag/typetheory" rel="nofollow noopener" target="_blank">#TypeTheory</a> <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener" target="_blank">#Agda</a>

Patrik Jansson🌍 The climate crisis demands urgent action. But which actions are best?Decision makers face tough trade-offs:Policy A lowers emissions at home but increases reliance on imports.Policy B cuts emissions long-term but raises unemployment short-term.Policy C boosts jobs now but increases emissions in the near term.None of these choices are simple. A policy that looks good locally may increase global emissions, or its effects may depend on what other countries do. And sometimes policies cancel each other out.The key point: climate policy is full of hard trade-offs. Technology can’t decide them — but it can help us (and policy-makers) understand them better.That’s the goal of our new project (proposal): building open-source computational tools that let decision makers explore climate policies under uncertainty, weigh different values, and see trade-offs clearly.If funded, we’ll start in late 2026 with a (small) team of researchers and students.More details about the grant proposal I just submitted: <a href="https://patrikja.owlstown.net/posts/4505" rel="nofollow noopener" translate="no" target="_blank">https://patrikja.owlstown.net/posts/4505</a><a href="https://functional.cafe/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://functional.cafe/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://functional.cafe/tags/Climate" class="mention hashtag" rel="nofollow noopener" target="_blank">#Climate</a>

José A. AlonsoReadings shared September 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/09/30-readings_shared_09-29-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/09/30-readings_shared_09-29-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#RustLang</a>

José A. AlonsoCetera: Certified termination with Agda. ~ Dieter Hofbauer, Johannes Waldmann. <a href="https://www.imn.htwk-leipzig.de/~waldmann/WST2025/proceedings/WST2025_paper_12.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www.imn.htwk-leipzig.de/~waldmann/WST2025/proceedings/WST2025_paper_12.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

Brent Yorgey8yo was almost late for school because his dad was proving things in <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> and lost track of time. <a href="https://mathstodon.xyz/tags/academickidproblems" class="mention hashtag" rel="nofollow noopener" target="_blank">#academickidproblems</a>

José A. AlonsoReadings shared September 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/09/24-readings_shared_09-23-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/09/24-readings_shared_09-23-25</a> <a href="https://mathstodon.xyz/tags/Abella" class="mention hashtag" rel="nofollow noopener" target="_blank">#Abella</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="nofollow noopener" target="_blank">#HOL4</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Naproche" class="mention hashtag" rel="nofollow noopener" target="_blank">#Naproche</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#RustLang</a>

Jaro Reinders (he/him)Is there a way to prove ¬ (Bool ≡ ℕ) in (non-cubical) <a href="https://social.edu.nl/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>?Bonus question: how can I figure this out if my usual search engines fail me?

José A. AlonsoFormalising inductive and coinductive containers. ~ Stefania Damato, Thorsten Altenkirch, and Axel Ljungström. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.17/LIPIcs.ITP.2025.17.pdf" rel="nofollow noopener" translate="no" target="_blank">https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.17/LIPIcs.ITP.2025.17.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoReadings shared September 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/09/20-readings_shared_09-19-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/09/20-readings_shared_09-19-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/CoqProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#CoqProver</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Idris2" class="mention hashtag" rel="nofollow noopener" target="_blank">#Idris2</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

José A. AlonsoThe conatural numbers form an exponential commutative semiring. ~ Szumi Xie, Viktor Bense. <a href="https://szumixie.github.io/docs/papers/the-conatural-numbers-form-an-exponential-commutative-semiring.pdf" rel="nofollow noopener" translate="no" target="_blank">https://szumixie.github.io/docs/papers/the-conatural-numbers-form-an-exponential-commutative-semiring.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoThe groupoid-syntax of type theory is a set. ~ Thorsten Altenkirch, Ambrus Kaposi, Szumi Xie. <a href="https://arxiv.org/abs/2509.14988" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2509.14988</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoReadings shared September 9, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/09/10-readings_shared_09-09-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/09/10-readings_shared_09-09-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#HoTT</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoOrdinal exponentiation in homotopy type theory. ~ Tom de Jong et als. <a href="https://arxiv.org/abs/2501.14542" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2501.14542</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener" target="_blank">#HoTT</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoReadings shared August 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/30-readings_shared_08-29-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/08/30-readings_shared_08-29-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoContinuous and algebraic domains in univalent foundations. ~ Tom de Jong, Martín Hötzel Escardó. <a href="https://www.sciencedirect.com/science/article/pii/S0022404925002117" rel="nofollow noopener" translate="no" target="_blank">https://www.sciencedirect.com/science/article/pii/S0022404925002117</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoReadings shared August 25, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/26-readings_shared_08-25-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/08/26-readings_shared_08-25-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/RustLang" class="mention hashtag" rel="nofollow noopener" target="_blank">#RustLang</a> <a href="https://mathstodon.xyz/tags/Waterproof" class="mention hashtag" rel="nofollow noopener" target="_blank">#Waterproof</a>

José A. AlonsoBig-stop semantics: A simple way to get the benefits of small-step semantics in a big-step judgment. ~ David M Kahn, Jan Hoffmann, Runming Li. <a href="https://arxiv.org/abs/2508.15157v1" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2508.15157v1</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a>

José A. AlonsoReadings shared August 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/24-readings_shared_08-23-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/08/24-readings_shared_08-23-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoDecidable equality for indexed data types, take 2. ~ Brent Yorgey. <a href="https://byorgey.github.io/blog/posts/2025/08/22/OneLevelTypesIndexed2.lagda.html" rel="nofollow noopener" translate="no" target="_blank">https://byorgey.github.io/blog/posts/2025/08/22/OneLevelTypesIndexed2.lagda.html</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a>

José A. AlonsoReadings shared August 22, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/08/23-readings_shared_08-22-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/08/23-readings_shared_08-22-25</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

Recent searches

Search options

Administered by:

Server stats:

#agda