Create accountLogin

Recent searches

No recent searches

Search options

Not available on lingo.lol.
lingo.lol is one of the many independent Mastodon servers you can use to participate in the fediverse.
A place for linguists, philologists, and other lovers of languages.

Administered by:

Server stats:

70
active users

lingo.lol: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.7

#agda

0 posts0 participants0 posts today
José A. Alonso<p>Readings shared March 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-23-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/23-readings_shared_03-23-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SetTheory</span></a></p>
José A. Alonso<p>Concurrent games in Agda. ~ Amy Yin. <a href="https://project-archive.inf.ed.ac.uk/ug4/20244250/ug4_proj.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">project-archive.inf.ed.ac.uk/u</span><span class="invisible">g4/20244250/ug4_proj.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
Jesper Agdakx 🔸New inconsistency in <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> just dropped: <a href="https://github.com/agda/agda/issues/7751" rel="nofollow noopener noreferrer" target="_blank">github.com/agda/agda/issues/7751</a>
Jesper Agdakx 🔸<p>As part of our (@sarantja@mastodon.social and yt) research on <strong>the usability of interactive theorem provers</strong>, we are conducting a study on the usage and state of tools and languages for type-driven development. We are interested in <strong>tools that encourage and facilitate type-driven development</strong>, especially in cases when they can help us reason about complex problems.</p><p>We are hoping to use your responses to identify the characteristic language features and tool interactions that enable type-driven development, with the eventual goals of enhancing them and bringing their benefits to a wider range of programmers.</p><p>Please fill in our <em>anonymous</em>, 10-minute survey here: <a href="https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS" rel="nofollow noopener noreferrer" target="_blank">https://tudelft.fra1.qualtrics.com/jfe/form/SV_bIsMxYTKUJkhVuS</a></p><p>You are welcome to participate if you have experience with <em>any</em> type-driven development tool, including dependently-typed languages (e.g., Coq, Lean, Agda), refinement types (e.g., Liquid Haskell), or even other static type systems (e.g., in Rust or Haskell).</p><p>P.S. In case you remember signing up for an interview with us in a previous survey and are now wondering whether that study will still go on, the answer is: yes! We’ve had to revise our schedule, but we are still excited to talk to you and will start inviting people for an interview soon.</p><p><a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a class="hashtag" href="https://agda.club/tag/coq" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a class="hashtag" href="https://agda.club/tag/rocq" rel="nofollow noopener noreferrer" target="_blank">#Rocq</a> <a class="hashtag" href="https://agda.club/tag/lean" rel="nofollow noopener noreferrer" target="_blank">#Lean</a> <a class="hashtag" href="https://agda.club/tag/liquidhaskell" rel="nofollow noopener noreferrer" target="_blank">#LiquidHaskell</a> <a class="hashtag" href="https://agda.club/tag/rust" rel="nofollow noopener noreferrer" target="_blank">#Rust</a> <a class="hashtag" href="https://agda.club/tag/haskell" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a class="hashtag" href="https://agda.club/tag/typedrivendevelopment" rel="nofollow noopener noreferrer" target="_blank">#TypeDrivenDevelopment</a> <a class="hashtag" href="https://agda.club/tag/tyde" rel="nofollow noopener noreferrer" target="_blank">#TyDe</a> <a class="hashtag" href="https://agda.club/tag/dependenttypes" rel="nofollow noopener noreferrer" target="_blank">#DependentTypes</a> <a class="hashtag" href="https://agda.club/tag/liquidtypes" rel="nofollow noopener noreferrer" target="_blank">#LiquidTypes</a> <a class="hashtag" href="https://agda.club/tag/refinementtypes" rel="nofollow noopener noreferrer" target="_blank">#RefinementTypes</a> <a class="hashtag" href="https://agda.club/tag/proofassistants" rel="nofollow noopener noreferrer" target="_blank">#ProofAssistants</a> <a class="hashtag" href="https://agda.club/tag/survey" rel="nofollow noopener noreferrer" target="_blank">#Survey</a></p>
José A. Alonso<p>Readings shared March 7, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/07-readings_shared_03-07-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/03/07-readings_shared_03-07-25</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/Reasoning" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Reasoning</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a></p>
José A. Alonso<p>On the formalization of the simplicial model of HoTT. ~ Kunhong Du. <a href="https://florisvandoorn.com/theses/KunhongDu.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">florisvandoorn.com/theses/Kunh</span><span class="invisible">ongDu.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
Woke Leftist Trash<p>The road to Agda: how should someone interested in programs go about learning in today?</p><p>Haskell programmer frustrated with injective type families wants to develop a mental model and intuition to make working with them easier. </p><p><a href="https://types.pl/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a> <a href="https://types.pl/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haskell</span></a></p>
Tom de Jong<p>The above is all formalized in the <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> TypeTopology development, see<br><a href="https://martinescardo.github.io/TypeTopology/Apartness.Properties.html#At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">martinescardo.github.io/TypeTo</span><span class="invisible">pology/Apartness.Properties.html#At-Most-One-Tight-Apartness-on-Cantor-gives-WLPO-implies-LPO</span></a></p><p>A (topological) model of intuitionistic set theory validating WLPO but not LPO is given in the below paper (see its fifth page and Theorem 5.1 in particular).</p><p>Matt Hendtlass and Robert Lubarsky. 'Separating Fragments of WLEM, LPO, and MP'<br>The Journal of Symbolic Logic. Vol. 81, No. 4, 2016, pp. 1315-1343.<br>DOI: 10.1017/jsl.2016.38<br>URL: <a href="https://www.math.fau.edu/people/faculty/lubarsky/separating-llpo.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">math.fau.edu/people/faculty/lu</span><span class="invisible">barsky/separating-llpo.pdf</span></a></p>
José A. Alonso<p>Readings shared January 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/30-readings_shared_01-30-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/30-readings_shared_01-30-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Cellular methods in homotopy type theory. ~ Axel Ljungström, Loïc Pujet. <a href="https://pujet.fr/pdf/cellular.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">pujet.fr/pdf/cellular.pdf</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
Tom de Jong<p>I'm pleased to advertise our latest paper titled "Ordinal Exponentiation in Homotopy Type Theory".<br><a href="https://arxiv.org/abs/2501.14542" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.14542</span><span class="invisible"></span></a></p><p>This is joint work with <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@fnf" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>fnf</span></a></span> <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@Nicolai_Kraus" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>Nicolai_Kraus</span></a></span> and Chuangjie Xu.</p><p>All our results are formalized in Agda, building on <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@MartinEscardo" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>MartinEscardo</span></a></span>'s TypeTopology development, see the HTML version at <a href="https://ordinal-exponentiation-HoTT.github.io/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ordinal-exponentiation-HoTT.gi</span><span class="invisible">thub.io/</span></a><br>In particular, the Paper file links every numbered environment in the paper to its implementation in Agda.</p><p><a href="https://mathstodon.xyz/tags/logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>logic</span></a> <a href="https://mathstodon.xyz/tags/TypeTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TypeTheory</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
Jack Leightcap<p>Hey all! I'm due for an (re-)introduction: I'm Jack, an engineer in the NYC area from a firmware &amp; cybersecurity background, currently working in something like hardware-software co-design.</p><p>Technical work is often with <a href="https://recurse.social/tags/rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>rust</span></a> <a href="https://recurse.social/tags/kicad" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>kicad</span></a> <a href="https://recurse.social/tags/python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>python</span></a> <a href="https://recurse.social/tags/verilog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verilog</span></a> <a href="https://recurse.social/tags/c" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>c</span></a>, and in all-too-rare moments stuff like <a href="https://recurse.social/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haskell</span></a> <a href="https://recurse.social/tags/forth" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>forth</span></a> <a href="https://recurse.social/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a> and <a href="https://recurse.social/tags/prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>prolog</span></a><br> <br>I've never been much for social media, usually preferring to keep interests local: a better-detailed <a href="https://recurse.social/tags/introduction" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>introduction</span></a> to follow as I figure this out 🙂</p>
José A. Alonso<p>Readings shared January 25, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/25-readings_shared_01-25-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/25-readings_shared_01-25-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/JuliaLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>JuliaLang</span></a></p>
José A. Alonso<p>Pinpointing the learning obstacles of an interactive theorem prover. ~ Sára Juhošová, Andy Zaidman, Jesper Cockx. <a href="https://sarajuhosova.com/assets/files/2025-icpc.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">sarajuhosova.com/assets/files/</span><span class="invisible">2025-icpc.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared January 16, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/16-readings_shared_01-16-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/16-readings_shared_01-16-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/SAT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SAT</span></a> <a href="https://mathstodon.xyz/tags/SMT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SMT</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Matem%C3%A1ticas" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Matemáticas</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>An agda2hs-compatible representation of exact real arithmetic. ~ Viktor Csimma. <a href="https://csimmaviktor.web.elte.hu/acorn.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">csimmaviktor.web.elte.hu/acorn</span><span class="invisible">.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a></p>
José A. Alonso<p>Readings shared January 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/11-readings_shared_01-11-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/11-readings_shared_01-11-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CategoryTheory</span></a> <a href="https://mathstodon.xyz/tags/ComputerSci" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ComputerSci</span></a> <a href="https://mathstodon.xyz/tags/Education" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Education</span></a> <a href="https://mathstodon.xyz/tags/GenAI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>GenAI</span></a></p>
José A. Alonso<p>On the correctness of Barron and Strachey’s cartesian product function. ~ Wouter Swierstra, Jason Hemann. <a href="https://trendsfp.github.io/abstracts/paper-006.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">trendsfp.github.io/abstracts/p</span><span class="invisible">aper-006.pdf</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a></p>
José A. Alonso<p>Readings shared January 6, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/06-readings_shared_01-06-25" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/06-readings_shared_01-06-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LLMs</span></a></p>
José A. Alonso<p>On planarity of graphs in homotopy type theory. ~ Cubides, Jonathan Steven Prieto; Gylterud, Håkon Robbestad. <a href="https://bora.uib.no/bora-xmlui/handle/11250/3170892" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">bora.uib.no/bora-xmlui/handle/</span><span class="invisible">11250/3170892</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/HoTT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HoTT</span></a></p>
ExploreLive feeds
About