scientific article; zbMATH DE number 7566073
From MaRDI portal
Publication:5094147
Dominik Kirst, Dominique Larchey-Wendling
Publication date: 2 August 2022
Full work available at URL: https://arxiv.org/abs/2104.14445
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On the almighty wand
- Elements of finite model theory.
- Categoricity results for second-order ZF in dependent type theory
- Verification of PCP-related computational reductions in Coq
- Completeness theorems for first-order logic analysed in constructive type theory
- Categoricity results and large model constructions for second-order ZF in dependent type theory
- Hereditarily Finite Sets in Constructive Type Theory
- HOCore in Coq
- Completeness theorems for first-order logic analysed in constructive type theory
- Trakhtenbrot’s Theorem in Coq
- Hilbert's Tenth Problem in Coq
- BI as an assertion language for mutable data structures
- Pragmatic Quotient Types in Coq
- Some elementary results in intuitionistic model theory
- An Efficient Coq Tactic for Deciding Kleene Algebras
- [https://portal.mardi4nfdi.de/wiki/Publication:5875425 A certifying extraction with time bounds from Coq to call-by-value $\lambda$-calculus]
