#dedukti — Public Fediverse posts

Readings shared February 19, 2026. https://jaalonso.github.io/vestigium/posts/2026/02/20-readings_shared_02-19-26 #AI4Math #ATP #CSLib #CompSci #Dedukti #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Math #Mizar #RocqProver #Vampire

Translating proofs from Lean to Dedukti. ~ Rishikesh Vaishnav. https://rish987.github.io/files/thesis.pdf #LeanProver #Dedukti #ITP

Readings shared September 18, 2025. https://jaalonso.github.io/vestigium/posts/2025/09/19-readings_shared_09-18-25 #AI #ATP #Dedukti #FunctionalProgramming #Haskell #ITP #LLMs #Vampire

Case study: Verified Vampire proofs in the lambdapi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suda. https://arxiv.org/abs/2503.15541 #ATP #Vampire #ITP #Dedukti

Readings shared March 21, 2025. https://jaalonso.github.io/vestigium/posts/2025/03/21-readings_shared_03-21-25 #AI #ATP #Dedukti #FunctionalProgramming #Haskell #IsabelleHOL #LLMs #LeanProver #Liquid #Logic #Math #Prolog #Reasoning #SMT #Vampire

Case study: Verified Vampire proofs in the LambdaPi-calculus modulo. ~ Anja Petković Komel, Michael Rawson, Martin Suad. https://arxiv.org/abs/2503.15541v1 #ATP #Vampire #Dedukti

@joaquimpuig Logipedia: a library of proofs expressed in Dedukti. http://logipedia.inria.fr/about/about.php #ITP #Dedukti #Math

Connecting Agda to other theorem provers via EuroProofNet (or, how to implement an Agda backend). ~ Jesper Cockx. https://jesper.sikanda.be/files/AIMXXXI-presentation.pdf #ITP #Agda #Dedukti

#TIL about #lambdaPi and #dedukti , they seem nifty.
https://github.com/Deducteam/lambdapi
https://github.com/Deducteam/Dedukti
Looks like there are translators for the latter from languages like #Coq and #HOL .
cc #typeTheory