scientific article; zbMATH DE number 7566073

MaRDI QIDQ5094147zbMATH OpenFDO

Authors Dominik Kirst, Dominique Larchey-Wendling

Publication date 2 August 2022

Full work available at URL https://arxiv.org/abs/2104.14445, https://lmcs.episciences.org/9696

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Trakhtenbrot’s Theorem in Coq
• Model-theoretic applications of cofinality spectrum problems
• scientific article; zbMATH DE number 4047715
• A Coq formalization of finitely presented modules
• On the proof theory of Coquand's calculus of constructions
• Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}
• A finite model construction for coalgebraic modal logic
• Foundations of Software Science and Computation Structures
• Model theory and proof theory of coalgebraic predicate logic
• scientific article; zbMATH DE number 1302878

Cites work

• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 2081098 (Why is no real title available?)
• scientific article; zbMATH DE number 7561487 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 965572 (Why is no real title available?)
• scientific article; zbMATH DE number 3057871 (Why is no real title available?)
• A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus
• An efficient Coq tactic for deciding Kleene algebras
• BI as an assertion language for mutable data structures
• Categoricity results and large model constructions for second-order ZF in dependent type theory
• Categoricity results for second-order ZF in dependent type theory
• Completeness theorems for first-order logic analysed in constructive type theory
• Completeness theorems for first-order logic analysed in constructive type theory
• Elements of finite model theory.
• HOCore in Coq
• Hereditarily finite sets in constructive type theory
• Hilbert's Tenth Problem in Coq
• On the almighty wand
• Pragmatic quotient types in Coq
• Some elementary results in intuitionistic model theory
• Trakhtenbrot’s Theorem in Coq
• Verification of PCP-related computational reductions in Coq

Cited in

(1)

• Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens

Describes a project that uses

Uses Software

• Coq

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094147)