Boyd Stephen Smith Jr.<p>Whelp. Just got let go. They actually disabled my account while I was in the exit interview. Corporate IT is _cold_.</p><p>Anyway, I guess I'm looking for a new position maybe even be <a href="https://hachyderm.io/tags/FediHired" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FediHired</span></a> ?</p><p>I have to live in Cove, AR with my disabled family, so it will probably need to be 100% remote.</p><p>I'd prefer to keep doing <a href="https://hachyderm.io/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Haskell</span></a> or try out <a href="https://hachyderm.io/tags/PureScript" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>PureScript</span></a> in production, or even something more exotic like <a href="https://hachyderm.io/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> or <a href="https://hachyderm.io/tags/Idris" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Idris</span></a></p>
Recent searches
No recent searches
Search options
Not available on dice.camp.
dice.camp is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon server for RPG folks to hang out and talk. Not owned by a billionaire.
Administered by:
Server stats:
1.7Kactive users
dice.camp: About · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.3.7
#agda
0 posts · 0 participants · 0 posts today
José A. Alonso<p>Code generation via meta-programming in dependently typed proof assistants. ~ Mathis Bouverot-Dupuis, Yannick Forster. <a href="https://hal.science/hal-05024207/document" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">hal.science/hal-05024207/docum</span><span class="invisible">ent</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/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LeanProver</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>
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>
DiazCarrete<p>NbE PHOAS <a href="https://oleg.fi/gists/posts/2025-02-11-nbe-phoas.html" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">oleg.fi/gists/posts/2025-02-11</span><span class="invisible">-nbe-phoas.html</span></a></p><p><a href="https://hachyderm.io/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a></p>
Jesper Agdakx 🔸Save the date: The next <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> Implementors' Meeting will be in Budapest between<br><br> 26 and 31 May 2025<br><br>(Monday to Saturday).<br><br>Some information on the location available here:<br><a href="https://wiki.portal.chalmers.se/agda/Main/AIMXXXX" rel="nofollow noopener noreferrer" target="_blank">wiki.portal.chalmers.se/agda/Main/AIMXXXX</a>
Tom de Jong<p>It turns out there is an even simpler example of a set that "fails" (in a much stronger sense) to have at most one tight apartness, following an idea of <span class="h-card" translate="no"><a href="https://mathstodon.xyz/@aws" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>aws</span></a></span>.</p><p>Suppose ℕ has at most one tight apartness.<br>We show that double negation elimination (¬¬P ⇒ P for all P) holds.</p><p>Since ℕ is discrete (i.e. it has decidable equality), the relation ≠ is a tight apartness.</p><p>Let P be an arbitrary proposition.<br>The relation n ♯ m := P ∧ (n ≠ m) on ℕ is an apartness.<br>Furthermore, it is tight if we assume ¬¬P.<br>But it clearly coincides with ≠ if and only if P holds.</p><p>Thus, if the natural numbers have at most one tight apartness then double negation elimination, or equivalently excluded middle, holds.<br>Moreover, this generalizes to any discrete type with two distinct points.</p><p>The above is formalized in TypeTopology using <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a>, see <a href="https://martinescardo.github.io/TypeTopology/Apartness.Properties.html#At-Most-One-Tight-Apartness-on-%E2%84%95-gives-DNE" 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-%E2%84%95-gives-DNE</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>
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 & 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>
Jencel Panic<p>At the <a href="https://mathstodon.xyz/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a> headquaters:</p><p>"OK, guys, so our user pool consists only of folks who already know <a href="https://mathstodon.xyz/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haskell</span></a> and <a href="https://mathstodon.xyz/tags/emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>emacs</span></a> Is there a way to narrow it down more?"</p><p>"I got it, what if we allow unicode, so they also have to also know <a href="https://mathstodon.xyz/tags/latex" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>latex</span></a> ?"</p><p>"Brilliant!"</p><p><a href="https://mathstodon.xyz/tags/joke" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>joke</span></a> </p><p>(just kidding, agda is very cool (hope to learn it someday))</p>
Jesper Agdakx 🔸I just updated the list of <a class="hashtag" href="https://agda.club/tag/agda" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> tutorials and videos at <a href="https://agda.readthedocs.io/en/latest/getting-started/tutorial-list.html" rel="nofollow noopener noreferrer" target="_blank">agda.readthedocs.io/en/latest/getting-started/tutorial-list.html</a> to add materials by <span class="h-card"><a class="u-url mention" href="https://mathstodon.xyz/@MartinEscardo" rel="nofollow noopener noreferrer" target="_blank">@<span>MartinEscardo</span></a></span> <span class="h-card"><a class="u-url mention" href="https://mathstodon.xyz/@andrejbauer" rel="nofollow noopener noreferrer" target="_blank">@<span>andrejbauer</span></a></span> <span class="h-card"><a class="u-url mention" href="https://types.pl/@JacquesC2" rel="nofollow noopener noreferrer" target="_blank">@<span>JacquesC2</span></a></span> <span class="h-card"><a class="u-url mention" href="https://mathstodon.xyz/@mortberg" rel="nofollow noopener noreferrer" target="_blank">@<span>mortberg</span></a></span> among other people. Thank you to everyone for bringing Agda to new people!
Stefano "Foxy🦊" Volpe<p><span class="h-card" translate="no"><a href="https://a.gup.pe/u/typst" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>typst@a.gup.pe</span></a></span></p><p>The <span class="h-card" translate="no"><a href="https://mastodon.social/@typst" class="u-url mention" rel="nofollow noopener noreferrer" target="_blank">@<span>typst@mastodon.social</span></a></span> package repository just accepted my <a href="https://social.edu.nl/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> syntax highlighting package 🐔</p><p><a href="https://codeberg.org/foxy/color-my-agda" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">codeberg.org/foxy/color-my-agd</span><span class="invisible">a</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>
Jesper Agdakx 🔸<p>The pre-print for the <a class="hashtag" href="https://agda.club/tag/icpc" rel="nofollow noopener noreferrer" target="_blank">#ICPC</a> paper “Pinpointing the Learning Obstacles of an Interactive Theorem Prover” by <span class="h-card"><a class="u-url mention" href="https://mastodon.social/@sarantja" rel="nofollow noopener noreferrer" target="_blank">@<span>sarantja</span></a></span> <span class="h-card"><a class="u-url mention" href="https://mastodon.social/@azaidman" rel="nofollow noopener noreferrer" target="_blank">@<span>azaidman</span></a></span> and yt is now available at <a href="https://sarajuhosova.com/assets/files/2025-icpc.pdf" rel="nofollow noopener noreferrer" target="_blank">https://sarajuhosova.com/assets/files/2025-icpc.pdf</a></p><p>I very much hope this will inspire more research on the usability and accessibility of the languages we build going forward!</p><p>Abstract:</p><blockquote><p>Interactive theorem provers (ITPs) are programming languages which allow users to reason about and verify their programs. Although they promise strong correctness guarantees and expressive type annotations which can act as code summaries, they tend to have a steep learning curve and poor usability. Unfortunately, there is only a vague understanding of the underlying causes for these problems within the research community. To pinpoint the exact usability bottlenecks of ITPs, we conducted an online survey among 41 computer science bachelor students, asking them to reflect on the experience of learning to use the Agda ITP and to list the obstacles they faced during the process. Qualitative analysis of the responses revealed confusion among the participants about the role of ITPs within software development processes as well as design choices and tool deficiencies which do not provide an adequate level of support to ITP users. To make ITPs more accessible to new users, we recommend that ITP designers look beyond the language itself and also consider its wider contexts of tooling, developer environments, and larger software development processes. </p></blockquote><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/theoremproving" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</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/usability" rel="nofollow noopener noreferrer" target="_blank">#Usability</a> <a class="hashtag" href="https://agda.club/tag/accessibility" rel="nofollow noopener noreferrer" target="_blank">#Accessibility</a> <a class="hashtag" href="https://agda.club/tag/icpc25" rel="nofollow noopener noreferrer" target="_blank">#ICPC25</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>
Jan de Muijnck-Hughes<p>Users of <a href="https://discuss.systems/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Agda</span></a> <a href="https://discuss.systems/tags/Lean" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Lean</span></a> <a href="https://discuss.systems/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a> <a href="https://discuss.systems/tags/Isabelle" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Isabelle</span></a> <a href="https://discuss.systems/tags/FStar" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FStar</span></a> <a href="https://discuss.systems/tags/Dafny" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Dafny</span></a> </p><p>I am looking to collect examples of 'notable' projects that used the language for verified software that _is_ used.</p><p>I have a list (Lean, Ceder, Idris, Sail, Bedrock, HAX, SEL4, Hax, Cardano) but want to know if there are more that I have missed...</p>
Programming Languages Delft<p>Master thesis by Jakob Nauke: Compiling Dependent Type Preconditions to Runtime Checks With Agda2Hs</p><p>"As an extension to Agda2Hs, we<br>have implemented a solution to automatically insert runtime checks for the preconditions and only make those definitions accessible in the output that are also checkable."</p><p><a href="https://repository.tudelft.nl/record/uuid:0a13ca4a-9d3c-416e-bb88-affc3f14ee52" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">repository.tudelft.nl/record/u</span><span class="invisible">uid:0a13ca4a-9d3c-416e-bb88-affc3f14ee52</span></a></p><p><a href="https://akademienl.social/tags/agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda</span></a> <a href="https://akademienl.social/tags/agda2hs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>agda2hs</span></a> <a href="https://akademienl.social/tags/haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>haskell</span></a> <a href="https://akademienl.social/tags/dependenttypes" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>dependenttypes</span></a> <a href="https://akademienl.social/tags/thesis" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>thesis</span></a></p>
ExploreLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
Create accountLoginDrag & drop to upload