José A. Alonso<p>Readings shared April 2, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/04/02-readings_shared_04-02-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/04/02-readings_shared_04-02-25</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Mathlib" class="mention hashtag" rel="tag">#<span>Mathlib</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#<span>Prolog</span></a></p>
Recent searches
No recent searches
Search options
Only available when logged in.
mathstodon.xyz is one of the many independent Mastodon servers you can use to participate in the fediverse.
A Mastodon instance for maths people. We have LaTeX rendering in the web interface!
Administered by:
Server stats:
2.8Kactive users
mathstodon.xyz: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.3.7
#hol4
0 posts · 0 participants · 0 posts today
José A. Alonso<p>GOL in GOL in HOL: Verified circuits in Conway's game of life. ~ Magnus O. Myreen, Mario Carneiro. <a href="https://arxiv.org/abs/2504.00263" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2504.00263</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
José A. Alonso<p>Readings shared January 13, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/01/13-readings_shared_01-13-25" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2025/01/13-readings_shared_01-13-25</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="tag">#<span>Rocq</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="tag">#<span>CommonLisp</span></a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="tag">#<span>Programming</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>Proof recommendation system for the HOL4 theorem prover. ~ Nour Dekhil, Adnan Rashid, Sofiene Tahar. <a href="https://arxiv.org/abs/2501.05463" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2501.05463</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
Rob Sison<p>There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:</p><p><a href="https://youtu.be/7wcFx6OTEL4" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">youtu.be/7wcFx6OTEL4</span><span class="invisible"></span></a></p><p><a href="https://aus.social/tags/sel4summit" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>sel4summit</span></a> <a href="https://aus.social/tags/seL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>seL4</span></a> <a href="https://aus.social/tags/verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>verification</span></a> <a href="https://aus.social/tags/operatingsystems" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>operatingsystems</span></a> <a href="https://aus.social/tags/microkernel" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>microkernel</span></a> <a href="https://aus.social/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://aus.social/tags/HOL4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://aus.social/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>ITP</span></a> <a href="https://aus.social/tags/modelchecking" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>modelchecking</span></a> <a href="https://aus.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> <a href="https://aus.social/tags/formalverification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalverification</span></a> <a href="https://aus.social/tags/formal_methods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_methods</span></a> <a href="https://aus.social/tags/formal_verification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formal_verification</span></a></p>
José A. Alonso<p>Readings shared September 6, 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/09/06-readings_shared_09-06-24" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/09/06-readings_shared_09-06-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="tag">#<span>Agda</span></a> <a href="https://mathstodon.xyz/tags/PVS" class="mention hashtag" rel="tag">#<span>PVS</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Lisa" class="mention hashtag" rel="tag">#<span>Lisa</span></a> <a href="https://mathstodon.xyz/tags/Mizar" class="mention hashtag" rel="tag">#<span>Mizar</span></a> <a href="https://mathstodon.xyz/tags/ACL2" class="mention hashtag" rel="tag">#<span>ACL2</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/MachineLearning" class="mention hashtag" rel="tag">#<span>MachineLearning</span></a></p>
José A. Alonso<p>A formal proof of R(4,5)=25. ~ Thibault Gauthier & Chad E. Brown. <a href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.16/LIPIcs.ITP.2024.16.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">drops.dagstuhl.de/storage/00li</span><span class="invisible">pics/lipics-vol309-itp2024/LIPIcs.ITP.2024.16/LIPIcs.ITP.2024.16.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>Lecturas compartidas el 9 de agosto de 2024. <a href="https://jaalonso.github.io/vestigium/posts/2024/08/10-lecturas_compartidas_el_09-ago-24" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/vestigium/p</span><span class="invisible">osts/2024/08/10-lecturas_compartidas_el_09-ago-24</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="tag">#<span>FunctionalProgramming</span></a> <a href="https://mathstodon.xyz/tags/IA" class="mention hashtag" rel="tag">#<span>IA</span></a></p>
José A. Alonso<p>Validation of HOL4's formal floating-point model. ~ Hugo Eidmann. <a href="https://www.diva-portal.org/smash/get/diva2:1879248/FULLTEXT01.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://www.</span><span class="ellipsis">diva-portal.org/smash/get/diva</span><span class="invisible">2:1879248/FULLTEXT01.pdf</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
José A. Alonso<p>Lecturas compartidas el 8 de mayo de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-8-de-mayo" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-8-de-mayo</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/Lean4" class="mention hashtag" rel="tag">#<span>Lean4</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/HOL_Light" class="mention hashtag" rel="tag">#<span>HOL_Light</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
José A. Alonso<p>HOL4P4: Mechanized small-step semantics for P4. ~ Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam. <a href="https://dl.acm.org/doi/pdf/10.1145/3649819" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">dl.acm.org/doi/pdf/10.1145/364</span><span class="invisible">9819</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
José A. Alonso<p>Lecturas compartidas el 3 de abril de 2024. <a href="https://jalonso.substack.com/lecturas-compartidas-el-3-de-abril" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">jalonso.substack.com/lecturas-</span><span class="invisible">compartidas-el-3-de-abril</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="tag">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="tag">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="tag">#<span>Coq</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="tag">#<span>Haskell</span></a> <a href="https://mathstodon.xyz/tags/LogicProgramming" class="mention hashtag" rel="tag">#<span>LogicProgramming</span></a> <a href="https://mathstodon.xyz/tags/Prolog" class="mention hashtag" rel="tag">#<span>Prolog</span></a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="tag">#<span>Python</span></a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="tag">#<span>Logic</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="tag">#<span>AI</span></a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="tag">#<span>LLMs</span></a> <a href="https://mathstodon.xyz/tags/Autoformalization" class="mention hashtag" rel="tag">#<span>Autoformalization</span></a></p>
José A. Alonso<p>A formal proof of R(4,5)=25. ~ Thibault Gauthier, Chad E. Brown. <a href="https://arxiv.org/abs/2404.01761" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="">arxiv.org/abs/2404.01761</span><span class="invisible"></span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="tag">#<span>Math</span></a></p>
Alex Nelson<p>Can <a href="https://mathstodon.xyz/tags/CakeML" class="mention hashtag" rel="tag">#<span>CakeML</span></a> be used to build itself yet? Will it ever decouple from <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a>?</p>
José A. Alonso<p>PureCake: A verified compiler for a lazy functional language. ~ Hrutvik Kanabar et als. <a href="https://dl.acm.org/doi/pdf/10.1145/3591259" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">dl.acm.org/doi/pdf/10.1145/359</span><span class="invisible">1259</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
José A. Alonso<p>A verified theorem prover for higher-order logic. ~ Oskar Abrahamsson. <a href="https://research.chalmers.se/publication/532951/file/532951_Fulltext.pdf" target="_blank" rel="nofollow noopener noreferrer" translate="no"><span class="invisible">https://</span><span class="ellipsis">research.chalmers.se/publicati</span><span class="invisible">on/532951/file/532951_Fulltext.pdf</span></a> <a href="https://mathstodon.xyz/tags/PhDThesis" class="mention hashtag" rel="tag">#<span>PhDThesis</span></a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="tag">#<span>ITP</span></a> <a href="https://mathstodon.xyz/tags/HOL4" class="mention hashtag" rel="tag">#<span>HOL4</span></a></p>
hannes<p>This year, we published a <a href="https://mastodon.social/tags/formalmethods" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>formalmethods</span></a> paper "Engineering with Logic: Rigorous Test-Oracle Specification<br>and Validation for TCP/IP and the Sockets API" <a href="https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://www.</span><span class="ellipsis">cl.cam.ac.uk/~pes20/Netsem/pap</span><span class="invisible">er3.pdf</span></a> in the Journal of the ACM! :) <a href="https://www.cl.cam.ac.uk/~pes20/rems/" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://www.</span><span class="">cl.cam.ac.uk/~pes20/rems/</span><span class="invisible"></span></a> <a href="https://mastodon.social/tags/hol4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>hol4</span></a> <a href="https://mastodon.social/tags/tcpip" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>tcpip</span></a> <a href="https://mastodon.social/tags/network" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>network</span></a> so glad that this is finally out :D (happy to hear your thoughts on that, still working on a TCP/IP stack based on that work)</p>
hannes<p>yay, our JACM paper is finally in print (see <a href="https://dl.acm.org/citation.cfm?id=3299993" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">https://</span><span class="ellipsis">dl.acm.org/citation.cfm?id=329</span><span class="invisible">9993</span></a>). FWIW, here's a direct link to a copy (powered by sci-hub <a href="http://sci-hub.is/10.1145/3243650" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">http://</span><span class="">sci-hub.is/10.1145/3243650</span><span class="invisible"></span></a>) <a href="https://mastodon.social/tags/tcp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TCP</span></a> <a href="https://mastodon.social/tags/hol4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> <a href="https://mastodon.social/tags/dtrace" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DTrace</span></a> <a href="https://mastodon.social/tags/semantics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Semantics</span></a></p>
hannes<p>I am happy to inform you that the final version of your manuscript<br>submission (Document not available) is now accepted to the Journal of the<br>ACM. (see <a href="http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf" rel="nofollow noopener noreferrer" target="_blank"><span class="invisible">http://www.</span><span class="ellipsis">cl.cam.ac.uk/~pes20/Netsem/pap</span><span class="invisible">er3.pdf</span></a>) <a href="https://mastodon.social/tags/tcp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>TCP</span></a> <a href="https://mastodon.social/tags/hol4" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>HOL4</span></a> \o/ :D <a href="https://mastodon.social/tags/dtrace" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>DTrace</span></a></p>
SearchLive 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