Cogent: uniqueness types and certifying compilation
From MaRDI portal
Recommendations
- Refinement through restraint: bringing down the cost of verification
- A type system for certified binaries
- scientific article; zbMATH DE number 1980940
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
Cites work
- scientific article; zbMATH DE number 3485174 (Why is no real title available?)
- scientific article; zbMATH DE number 3574936 (Why is no real title available?)
- scientific article; zbMATH DE number 1538025 (Why is no real title available?)
- scientific article; zbMATH DE number 1552508 (Why is no real title available?)
- scientific article; zbMATH DE number 3349775 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- scientific article; zbMATH DE number 7649976 (Why is no real title available?)
- A certified framework for compiling and executing garbage-collected languages
- A formally verified compiler back-end
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- A framework for the verification of certifying computations
- Abstract state machines, Alloy, B, TLA, VDM, and Z. 4th international conference, ABZ 2014, Toulouse, France, June 2--6, 2014. Proceedings
- An axiomatic proof technique for parallel programs
- Balancing the load. Leveraging a semantics stack for systems verification
- Bridging the Gap: Automatic Verified Abstraction of C
- CakeML
- Certifying algorithms
- Characteristic formulae for the verification of imperative programs
- Dafny: an automatic program verifier for functional correctness
- Data Refinement
- Deep specifications and certified abstraction layers
- Designing programs that check their work
- Formalizing a hierarchical file system
- Formalizing the LLVM intermediate representation for verified program transformations
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Isabelle/HOL. A proof assistant for higher-order logic
- Logic for Programming, Artificial Intelligence, and Reasoning
- Program verification through characteristic formulae
- Programming Languages and Systems
- Ready, set, verify! Applying hs-to-coq to real-world Haskell code
- Refinement through restraint: bringing down the cost of verification
- Secure Microkernels, State Monads and Scalable Refinement
- Specification of the UNIX Filing System
- The meaning of memory safety
- Types, bytes, and separation logic
- Uniqueness Typing Redefined
Cited in
(11)- Towards a trustworthy semantics-based language framework via proof generation
- Safe functional systems through integrity types and verified assembly
- scientific article; zbMATH DE number 1231477 (Why is no real title available?)
- A language-based approach to functionally correct imperative programming
- Refinement through restraint: bringing down the cost of verification
- A framework for the automatic formal verification of refinement from \textsc{Cogent} to C
- Translation certification for smart contracts
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Linearity and uniqueness: an entente cordiale
- Formally understanding Rust's ownership and borrowing system at the memory level
- Uniqueness types for efficient and verifiable aliasing-free embedded systems programming
This page was built for publication: Cogent: uniqueness types and certifying compilation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5019022)
