Lingolol

José A. AlonsoA verified reduction algorithm from MLSSmf to MLSS. ~ Yiran Duan, Lukas Stevens. <a href="https://www.isa-afp.org/entries/MLSSmf_to_MLSS.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/MLSSmf_to_MLSS.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoFaithful logic embeddings in HOL — Deep and shallow (Isabelle/HOL dataset). ~ Christoph Benzmüller. <a href="https://www.isa-afp.org/entries/FaithfulPMLinHOL.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/FaithfulPMLinHOL.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared June 3, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/06/03-readings_shared_06-03-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/06/03-readings_shared_06-03-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/ATP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ATP</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Emacs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/SAT_Solvers" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#SAT_Solvers</a>

José A. AlonsoRestriction spaces: a fixed-point theory (in Isabelle/HOL). ~ Benoît Ballenghienm, Benjamin Puyobro, Burkhart Wolff. <a href="https://www.isa-afp.org/entries/Restriction_Spaces.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/Restriction_Spaces.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared May 29, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/29-readings_shared_05-29-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/29-readings_shared_05-29-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/Agda" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Agda</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/Emacs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Emacs</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Lisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Lisp</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoA formal analysis of algorithms for matroids and greedoids. ~ Mohammad Abdulaziz, Thomas Ammer, Shriya Meenakshisundaram, Adem Rimpapa. <a href="https://arxiv.org/abs/2505.19816" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2505.19816</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoContext-free grammars and languages (in Isabelle/HOL). ~ Tobias Nipkow et als. <a href="https://www.isa-afp.org/entries/Context_Free_Grammar.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/Context_Free_Grammar.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared May 28, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/28-readings_shared_05-28-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/28-readings_shared_05-28-25</a> <a href="https://mathstodon.xyz/tags/AI" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AI</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoFaithful logic embeddings in HOL (Deep and shallow). ~ Christoph Benzmüller. <a href="https://arxiv.org/abs/2502.19311" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2502.19311</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/TheoremProving" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#TheoremProving</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Logic" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Logic</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoReadings shared May 25, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/25-readings_shared_05-25-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/25-readings_shared_05-25-25</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/OrgMode" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#OrgMode</a>

José A. AlonsoShallow expressions (in Isabelle/HOL). ~ Simon Foster. <a href="https://www.isa-afp.org/entries/Shallow_Expressions.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/Shallow_Expressions.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared May 24, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/24-readings_shared_05-24-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/24-readings_shared_05-24-25</a> <a href="https://mathstodon.xyz/tags/AIforCode" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AIforCode</a> <a href="https://mathstodon.xyz/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#FunctionalProgramming</a> <a href="https://mathstodon.xyz/tags/Haskell" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Haskell</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Physics" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Physics</a>

José A. AlonsoMunta: A verified model checker for timed automata (in Isabelle/HOL). ~ Simon Wimmer. <a href="https://www.isa-afp.org/entries/Munta_Model_Checker.html" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://www.isa-afp.org/entries/Munta_Model_Checker.html</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoA formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. <a href="https://arxiv.org/abs/2505.16963" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://arxiv.org/abs/2505.16963</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a>

José A. AlonsoReadings shared May 23, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/23-readings_shared_05-23-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/23-readings_shared_05-23-25</a> <a href="https://mathstodon.xyz/tags/AIforCode" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#AIforCode</a> <a href="https://mathstodon.xyz/tags/CategoryTheory" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CategoryTheory</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LLMs" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LLMs</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/RocqProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#RocqProver</a>

José A. AlonsoFormalisation of fairness notions in assignment problem. ~ Duc Minh Do. <a href="https://people.eng.unimelb.edu.au/rizkallahc/theses/minh-do-undergrad-project-report.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://people.eng.unimelb.edu.au/rizkallahc/theses/minh-do-undergrad-project-report.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoReadings shared May 19, 2025. <a href="https://jaalonso.github.io/vestigium/posts/2025/05/19-readings_shared_05-19-25" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://jaalonso.github.io/vestigium/posts/2025/05/19-readings_shared_05-19-25</a> <a href="https://mathstodon.xyz/tags/CommonLisp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#CommonLisp</a> <a href="https://mathstodon.xyz/tags/Coq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Coq</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#LeanProver</a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Math</a> <a href="https://mathstodon.xyz/tags/Programming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Programming</a> <a href="https://mathstodon.xyz/tags/Python" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Python</a> <a href="https://mathstodon.xyz/tags/Rocq" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#Rocq</a>

José A. AlonsoVerifying smart contract transformations using bisimulations. ~ Kegan McIlwaine, James Caldwell. <a href="https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.9/OASIcs.FMBC.2025.9.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.9/OASIcs.FMBC.2025.9.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

José A. AlonsoFormal verification of a fail-safe cross-chain bridge. ~ Filip Marić, Bernhard Scholz, Pavle Subotić. <a href="https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.8/OASIcs.FMBC.2025.8.pdf" rel="nofollow noopener noreferrer" translate="no" target="_blank">https://drops.dagstuhl.de/storage/01oasics/oasics-vol129-fmbc2025/OASIcs.FMBC.2025.8/OASIcs.FMBC.2025.8.pdf</a> <a href="https://mathstodon.xyz/tags/ITP" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#ITP</a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#IsabelleHOL</a>

Recent searches

Search options

Administered by:

Server stats:

#IsabelleHOL