Uniqueness types for efficient and verifiable aliasing-free embedded systems programming

DOI10.1007/978-3-030-34968-4_3zbMATH Open1540.68056MaRDI QIDQ6536347FDOQ6536347

Authors: Tuur Benoit, Bart Jacobs 

Publication date: 19 April 2024

Recommendations

• Alias burying: Unique variables without destructive reads
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Cogent: uniqueness types and certifying compilation
• A formally-verified alias analysis
• Uniqueness logic

zbMATH Keywords

formal verificationuniqueness types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Idris, a general-purpose dependently typed programming language: Design and implementation
• Practical affine types
• Title not available (Why is that?)
• Linear logic
• Title not available (Why is that?)
• Building high integrity applications with SPARK

This page was built for publication: Uniqueness types for efficient and verifiable aliasing-free embedded systems programming

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536347)