Polymorphic DHOL is formalized with syntax, semantics, and a HOL translation, implemented in a logic-embedding tool and evaluated on TPTP formalizations to support automated proving.
Competing inheritance paths in dependent type theory: A case study in functional analysis
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
citation-role summary
background 1
citation-polarity summary
fields
cs.LO 3verdicts
UNVERDICTED 3roles
background 1polarities
background 1representative citing papers
A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
citing papers explorer
-
Polymorphism Meets DHOL
Polymorphic DHOL is formalized with syntax, semantics, and a HOL translation, implemented in a logic-embedding tool and evaluated on TPTP formalizations to support automated proving.
-
A Rocq Formalization of Simplicial Lagrange Finite Elements
A Rocq formalization defines simplicial Lagrange finite elements as records with geometric data, polynomial approximations, and unisolvence proofs for any dimension and polynomial degree.
-
Proving Confluence in the Confluence Framework with CONFident
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.