Mastodon

もく<a href="https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001" rel="nofollow noopener" translate="no" target="_blank">https://discourse.rocq-prover.org/t/coq-community-survey-2022-results-part-iv-and-itp-paper-announcement/2001</a>This is the saddest Discourse post I've ever read😢 <a href="https://social.mikutter.hachune.net/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> -> <a href="https://social.mikutter.hachune.net/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a>

HoldMyTypetil - fiat <a href="https://mathstodon.xyz/tags/coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#coq</a> Mostly Automated Synthesis of Correct-by-Construction Programs > Deductive Synthesis of Abstract Data Types in a Proof Assistant <a href="https://github.com/mit-plv/fiat" rel="nofollow noopener" translate="no" target="_blank">https://github.com/mit-plv/fiat</a> re/mod to my previous toot - cc <a href="https://recurse.social/@redmp" class="u-url mention" rel="nofollow noopener" target="_blank">@redmp</a>

José A. AlonsoReadings shared April 13, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/13-readings_shared_04-13-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ATP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</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/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/Mace4" class="mention hashtag" rel="nofollow noopener" target="_blank">#Mace4</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Prover9" class="mention hashtag" rel="nofollow noopener" target="_blank">#Prover9</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

José A. AlonsoEfficient formal verification of quantum error correcting programs. ~ Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying. <a href="https://arxiv.org/abs/2504.07732" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2504.07732</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a>

José A. AlonsoReadings shared April 11, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/11-readings_shared_04-11-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/04/11-readings_shared_04-11-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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Hakell" class="mention hashtag" rel="nofollow noopener" target="_blank">#Hakell</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/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/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

José A. AlonsoA comparative review of ZFC, NBG, and MK axiom systems: Theoretical foundations and formalization in Coq. ~ Si Chen, Wensheng Yu. <a href="https://www.preprints.org/manuscript/202504.0684/v1" rel="nofollow noopener" translate="no" target="_blank">https://www.preprints.org/manuscript/202504.0684/v1</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

LénonÀ Champagnac la rivière, comme dans beaucoup de villages, il y a des coqs et des poules. Ceux là ont l'air pas mal logés. Comme par hasard le symbole de la résidence Super Rural qui nous amène là est un coq... Bref je dessine des volailles pour ce projet depuis des mois et des fois c'est sur le motif. En + on a appris que cette parcelle était une ancienne chenevière (parcelle de culture du chanvre). <a href="https://pixelfed.fr/discover/tags/superrural?src=hash" class="u-url hashtag" rel="nofollow noopener" target="_blank">#superrural</a> <a href="https://pixelfed.fr/discover/tags/poules?src=hash" class="u-url hashtag" rel="nofollow noopener" target="_blank">#poules</a> <a href="https://pixelfed.fr/discover/tags/coq?src=hash" class="u-url hashtag" rel="nofollow noopener" target="_blank">#coq</a> <a href="https://pixelfed.fr/discover/tags/habitabilite?src=hash" class="u-url hashtag" rel="nofollow noopener" target="_blank">#habitabilite</a> Superrural.fr

José A. AlonsoReadings shared March 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/30-readings_shared_03-30-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/30-readings_shared_03-30-25</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Maxima" class="mention hashtag" rel="nofollow noopener" target="_blank">#Maxima</a>

Atlas the Explorer 🦋More Qud sprites! More variety in character species this time hehe (though per game standards they'd all be Mutants!)<a href="https://mastodon.art/tags/pixelart" class="mention hashtag" rel="nofollow noopener" target="_blank">#pixelart</a> <a href="https://mastodon.art/tags/furryart" class="mention hashtag" rel="nofollow noopener" target="_blank">#furryart</a> <a href="https://mastodon.art/tags/cavesofqud" class="mention hashtag" rel="nofollow noopener" target="_blank">#cavesofqud</a> <a href="https://mastodon.art/tags/coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#coq</a> <a href="https://mastodon.art/tags/fanart" class="mention hashtag" rel="nofollow noopener" target="_blank">#fanart</a> <a href="https://mastodon.art/tags/mastoart" class="mention hashtag" rel="nofollow noopener" target="_blank">#mastoart</a>

José A. AlonsoTowards mechanized verification of Verilog equivalence checking. ~ Michalis Pardalos, Laura Pozzi, John Wickerson. <a href="https://johnwickerson.github.io/papers/vera_LATTE25.pdf" rel="nofollow noopener" translate="no" target="_blank">https://johnwickerson.github.io/papers/vera_LATTE25.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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a>

Atlas the Explorer 🦋I've been playing a ton of Caves of Qud recently, so I thought I'd do a few player tiles for folks in my server and get some pixel art practice while at it c: This first batch is all moths!!<a href="https://mastodon.art/tags/pixelart" class="mention hashtag" rel="nofollow noopener" target="_blank">#pixelart</a> <a href="https://mastodon.art/tags/furryart" class="mention hashtag" rel="nofollow noopener" target="_blank">#furryart</a> <a href="https://mastodon.art/tags/moth" class="mention hashtag" rel="nofollow noopener" target="_blank">#moth</a> <a href="https://mastodon.art/tags/bug" class="mention hashtag" rel="nofollow noopener" target="_blank">#bug</a> <a href="https://mastodon.art/tags/cavesofqud" class="mention hashtag" rel="nofollow noopener" target="_blank">#cavesofqud</a> <a href="https://mastodon.art/tags/coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#coq</a> <a href="https://mastodon.art/tags/fanart" class="mention hashtag" rel="nofollow noopener" target="_blank">#fanart</a> <a href="https://mastodon.art/tags/mastoart" class="mention hashtag" rel="nofollow noopener" target="_blank">#mastoart</a>

José A. AlonsoReadings shared March 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/27-readings_shared_03-27-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/27-readings_shared_03-27-25</a> <a href="https://mathstodon.xyz/tags/CLP" class="mention hashtag" rel="nofollow noopener" target="_blank">#CLP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</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/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#LogicProgramming</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Programaci%C3%B3nFuncional" class="mention hashtag" rel="nofollow noopener" target="_blank">#ProgramaciónFuncional</a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener" target="_blank">#Prolog</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/TeXLaTeX" class="mention hashtag" rel="nofollow noopener" target="_blank">#TeXLaTeX</a>

José A. AlonsoBi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. <a href="https://arxiv.org/abs/2503.17159" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2503.17159</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Rocq</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener" target="_blank">#Logic</a>

José A. AlonsoReadings shared March 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-23-25" rel="nofollow noopener" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/03/23-readings_shared_03-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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="nofollow noopener" target="_blank">#HOL_Light</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/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="nofollow noopener" target="_blank">#Mizar</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

:rss: Qiita - 人気の記事PHOASでshift/resetのCPS変換 in Rocq(旧Coq) <a href="https://qiita.com/mrkbc/items/89b034dadc69df2ad274?utm_campaign=popular_items&utm_medium=feed&utm_source=popular_items" rel="nofollow noopener" translate="no" target="_blank">https://qiita.com/mrkbc/items/89b034dadc69df2ad274?utm_campaign=popular_items&utm_medium=feed&utm_source=popular_items</a><a href="https://rss-mstdn.studiofreesia.com/tags/qiita" class="mention hashtag" rel="nofollow noopener" target="_blank">#qiita</a> <a href="https://rss-mstdn.studiofreesia.com/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://rss-mstdn.studiofreesia.com/tags/%E9%99%90%E5%AE%9A%E7%B6%99%E7%B6%9A" class="mention hashtag" rel="nofollow noopener" target="_blank">#限定継続</a> <a href="https://rss-mstdn.studiofreesia.com/tags/rocq" class="mention hashtag" rel="nofollow noopener" target="_blank">#rocq</a>

José A. AlonsoImplementation of Bourbaki’s elements of mathematics in Coq: Part two, ordered sets, cardinals, integers. ~ José Grimm (2018). <a href="https://inria.hal.science/inria-00440786/file/RR-7150-v10.pdf" rel="nofollow noopener" translate="no" target="_blank">https://inria.hal.science/inria-00440786/file/RR-7150-v10.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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoImplementation of Bourbaki's elements of mathematics in Coq: Part one, theory of sets. ~ José Grimm (2009). <a href="https://www-sop.inria.fr/marelle/gaia/RR-6999-v6.pdf" rel="nofollow noopener" translate="no" target="_blank">https://www-sop.inria.fr/marelle/gaia/RR-6999-v6.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/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

José A. AlonsoFormalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). <a href="https://arxiv.org/abs/2407.06222" rel="nofollow noopener" translate="no" target="_blank">https://arxiv.org/abs/2407.06222</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/SetTheory" class="mention hashtag" rel="nofollow noopener" target="_blank">#SetTheory</a>

José A. AlonsoFormalizing calculus without limit theory in Coq. ~ Yaoshun Fu, Wensheng Yu (2021). <a href="https://www.mdpi.com/2227-7390/9/12/1377" rel="nofollow noopener" translate="no" target="_blank">https://www.mdpi.com/2227-7390/9/12/1377</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

José A. AlonsoFormalization of the equivalence among completeness theorems of real number in Coq. ~ Yaoshun Fu, Wensheng Yu (2020). <a href="https://www.mdpi.com/2227-7390/9/1/38" rel="nofollow noopener" translate="no" target="_blank">https://www.mdpi.com/2227-7390/9/1/38</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#Math</a>

Recent searches

Search options

Administered by:

Server stats:

#coq