Coq is an interactive theorem prover based on the calculus of constructions (CoC) which is a constructive logic based on the Curry-Howard correspondence.

Notes related to Coq theorem prover

CompCert compiler, Dependent type, NOVA hypervisor, RustBelt verifier

Papers related to Coq theorem prover

• The meaning of memory safety [azevedo:post:2018]
• Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
• Constructions: A higher order proof system for mechanizing mathematics [coquand:eurocal:1985]
• CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
• RustBelt: Securing the foundations of the Rust programming language [jung:popl:2017]
• Stacked borrows: An aliasing model for Rust [jung:popl:2020]
• Coq: The world's best macro assembler? [kennedy:ppdp:2013]
• Formal verification of a realistic compiler [leroy:cacm:2009]
• A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
• Lem: Reusable engineering of real-world semantics [mulligan:icfp:2014]
• Software foundations [pierce:book:2016]
• RefinedC: Automating the foundational verification of C code with refined ownership types [sammler:pldi:2021]
• SpaceSearch: A library for building and verifying solver-aided tools [weitz:icfp:2017]
• GhostCell: Separating permissions from data in Rust [yanovski:unknown:2021]