Pith. sign in

REVIEW 3 cited by

Dedukti: a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2311.07185 v1 pith:CXKSHIU4 submitted 2023-11-13 cs.LO

Ali Assaf , Guillaume Burel (ENSIIE) , Raphaël Cauderlier , David Delahaye (CNAM) , Gilles Dowek , Catherine Dubois (ENSIIE) , Frédéric Gilbert , Pierre Halmagrand
show 2 more authors
Olivier Hermant Ronan Saillard
This is my paper
classification cs.LO
keywords calculusdeduktitheoryframeworklambdalogicalmodulosystems
verification ladder T0 review T1 audit T2 compute T3 formal
0 comments
abstract

Dedukti is a Logical Framework based on the $\lambda$$\Pi$-Calculus Modulo Theory. We show that many theories can be expressed in Dedukti: constructive and classical predicate logic, Simple type theory, programming languages, Pure type systems, the Calculus of inductive constructions with universes, etc. and that permits to used it to check large libraries of proofs developed in other proof systems: Zenon, iProver, FoCaLiZe, HOL Light, and Matita.

Discussion (0). Sign in to comment.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. Exploiting Instantiations from Paramodulation Proofs in Isabelle/HOL

    cs.LO 2025-08 conditional novelty 7.0 of 10

    A new Isabelle/HOL extension infers variable instantiations from Metis proofs; the instantiated lemmas speed up proof reconstruction and increase Sledgehammer's success rate.

  2. Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

    cs.LO 2026-07 conditional novelty 6.0 of 10

    An interactive sequent prover for Event-B was built by encoding over 600 proof rules in Prolog inside ProB.

  3. The Vampire Diary

    cs.LO 2025-06 conditional novelty 5.0 of 10

    Vampire, now open source, integrates superposition with ALASCA arithmetic, induction schemata, and polymorphism, and the paper demonstrates a combined proof that the authors say CVC5 and Z3 cannot yet produce.

Pith tools