José A. Alonso
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
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the trusted computing base, and in principle eases proof reconstruction in other proof-checking systems. Existing theory is adapted to deal with Vampire's internal logic and inference system. Implementation experience is reported, encouraging adoption of verified proofs in other automated systems.
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
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the trusted computing base, and in principle eases proof reconstruction in other proof-checking systems. Existing theory is adapted to deal with Vampire's internal logic and inference system. Implementation experience is reported, encouraging adoption of verified proofs in other automated systems.
@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
Csepp 🌢#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
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
