Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
bolha.us is one of the many independent Mastodon servers you can use to participate in the fediverse.
We're a Brazilian IT Community. We love IT/DevOps/Cloud, but we also love to talk about life, the universe, and more. | Nós somos uma comunidade de TI Brasileira, gostamos de Dev/DevOps/Cloud e mais!

Administered by:

Server stats:

252
active users

bolha.us: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.6

#coq

2 posts2 participants0 posts today
José A. Alonso<p>Readings shared March 30, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/30-readings_shared_03-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/03/30-readings_shared_03-30-25</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/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/Maxima" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Maxima</span></a></p>
José A. Alonso<p>Towards 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">johnwickerson.github.io/papers</span><span class="invisible">/vera_LATTE25.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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</span></a></p>
Atlas the Explorer 🦋<p>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:<br>This first batch is all moths!!</p><p><a href="https://mastodon.art/tags/pixelart" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>pixelart</span></a> <a href="https://mastodon.art/tags/furryart" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>furryart</span></a> <a href="https://mastodon.art/tags/moth" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>moth</span></a> <a href="https://mastodon.art/tags/bug" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>bug</span></a> <a href="https://mastodon.art/tags/cavesofqud" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>cavesofqud</span></a> <a href="https://mastodon.art/tags/coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>coq</span></a> <a href="https://mastodon.art/tags/fanart" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>fanart</span></a> <a href="https://mastodon.art/tags/mastoart" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>mastoart</span></a></p>
José A. Alonso<p>Readings shared March 27, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/03/27-readings_shared_03-27-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/27-readings_shared_03-27-25</span></a> <a href="https://mathstodon.xyz/tags/CLP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>CLP</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/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/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>LogicProgramming</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/Programaci%C3%B3nFuncional" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ProgramaciónFuncional</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Prolog</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/TeXLaTeX" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TeXLaTeX</span></a></p>
José A. Alonso<p>Bi-intuitionistic logics through the abstract algebraic logic lens. ~ Jonte Deakin, Ian Shillito. <a href="https://arxiv.org/abs/2503.17159" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2503.17159</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/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/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Logic</span></a></p>
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>Implementation 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">inria.hal.science/inria-004407</span><span class="invisible">86/file/RR-7150-v10.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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>Implementation 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">www-sop.inria.fr/marelle/gaia/</span><span class="invisible">RR-6999-v6.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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>Formalization of the filter extension principle (FEP) in Coq. ~ Guowei Dou, Wensheng Yu (2024). <a href="https://arxiv.org/abs/2407.06222" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/2407.06222</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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/SetTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SetTheory</span></a></p>
José A. Alonso<p>Formalizing 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">mdpi.com/2227-7390/9/12/1377</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>Formalization 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 noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="">mdpi.com/2227-7390/9/1/38</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>A formalization of properties of continuous functions on closed intervals. Yaoshun Fu, Wensheng Yu (2020). <a href="https://link.springer.com/content/pdf/10.1007/978-3-030-52200-1_27.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">link.springer.com/content/pdf/</span><span class="invisible">10.1007/978-3-030-52200-1_27.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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>A formal proof in Coq of Cantor-Bernstein-Schroeder’s theorem without axiom of choice (2019). <a href="https://www.researchgate.net/publication/339270363_A_Formal_Proof_in_Coq_of_Cantor-Bernstein-Schroeder's_Theorem_without_axiom_of_choice" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">researchgate.net/publication/3</span><span class="invisible">39270363_A_Formal_Proof_in_Coq_of_Cantor-Bernstein-Schroeder's_Theorem_without_axiom_of_choice</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>A formalization of topological spaces in Coq. ~ Sheng Yan, Yaoshun Fu, Dakai Guo, and Wensheng Yu (2022). <a href="https://link.springer.com/content/pdf/10.1007/978-981-19-2456-9_21.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">link.springer.com/content/pdf/</span><span class="invisible">10.1007/978-981-19-2456-9_21.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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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/SetTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SetTheory</span></a></p>
José A. Alonso<p>Formalization of the axiom of choice and its equivalent theorems. ~ Tianyu Sun, Wensheng Yu (2019). <a href="https://arxiv.org/abs/1906.03930v1" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">arxiv.org/abs/1906.03930v1</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>A formal system of axiomatic set theory in Coq. ~ Tianyu Sun, Wensheng Yu (2020). <a href="https://ieeexplore.ieee.org/document/8970457" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ieeexplore.ieee.org/document/8</span><span class="invisible">970457</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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>A review on mechanical proving and formalization of mathematical theorems. ~ Si Chen, Wensheng Yu, Guowei Dou, Qimeng Zhang. <a href="https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=10930874" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">ieeexplore.ieee.org/stamp/stam</span><span class="invisible">p.jsp?arnumber=10930874</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/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Coq</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/HOL_Light" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL_Light</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/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></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>A formalisation of addition chains. ~ Laurent Théry. <a href="https://hal.science/hal-04971933/document" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">hal.science/hal-04971933/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/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></p>
José A. Alonso<p>QED in context (An observation study of proof assistant users). ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head.<a href="https://jwshii.github.io/OOPSLA25.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">jwshii.github.io/OOPSLA25.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/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></p>
ExploreLive feeds
About