Cogent: uniqueness types and certifying compilation

DOI10.1017/S095679682100023XOpenAlexW3210291382MaRDI QIDQ5019022

Liam O'Connor, Thomas D. Sewell, Christine Rizkallah, Gerwin Klein, Gabriele Keller, Toby Murray, Zilin Chen, Sidney Amani, Vincent Jackson

Publication date: 27 December 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s095679682100023x

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

Translation certification for smart contracts ⋮ Linearity and uniqueness: an entente cordiale

Uses Software

• Cogent

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Certifying algorithms
• Balancing the load. Leveraging a semantics stack for systems verification
• An axiomatic proof technique for parallel programs
• Isabelle/HOL. A proof assistant for higher-order logic
• The meaning of memory safety
• 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
• A formally verified compiler back-end
• Deep Specifications and Certified Abstraction Layers
• A Framework for the Automatic Formal Verification of Refinement from Cogent to C
• Bridging the Gap: Automatic Verified Abstraction of C
• Formalizing the LLVM intermediate representation for verified program transformations
• Refinement through restraint: bringing down the cost of verification
• Formalizing a Hierarchical File System
• Dafny: An Automatic Program Verifier for Functional Correctness
• Types, bytes, and separation logic
• Specification of the UNIX Filing System
• Secure Microkernels, State Monads and Scalable Refinement
• Uniqueness Typing Redefined
• Designing programs that check their work
• Data Refinement
• Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code
• A certified framework for compiling and executing garbage-collected languages
• Program verification through characteristic formulae
• Characteristic formulae for the verification of imperative programs
• Programming Languages and Systems
• Idris, a general-purpose dependently typed programming language: Design and implementation
• CakeML
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Cogent: uniqueness types and certifying compilation