\textsf{LOGIC}: a Coq library for logics
From MaRDI portal
Publication:6168989
DOI10.1007/978-3-031-21213-0_13zbMath1528.68397MaRDI QIDQ6168989
Publication date: 10 August 2023
Published in: Dependable Software Engineering. Theories, Tools, and Applications (Search for Journal in Brave)
Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle. A generic theorem prover
- VST-Floyd: a separation logic tool to verify correctness of C programs
- Iris
- Formalizing Cut Elimination of Coalgebraic Logics in Coq
- ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages
- Verified Software Toolchain
- Interacting with Modal Logics in the Coq Proof Assistant
- First-Class Type Classes
- Completeness theorems for first-order logic analysed in constructive type theory
- Bringing Order to the Separation Logic Jungle
- Proceedings Fourth Workshop on Proof eXchange for Theorem Proving
This page was built for publication: \textsf{LOGIC}: a Coq library for logics
