Low-level liquid types

DOI10.1145/1706299.1706316MaRDI QIDQ5255068zbMATH OpenOpenAlexFDO

Authors Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala

Publication date 11 June 2015

Published in Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/1706299.1706316

zbMATH Keywords

Cdependent typesliquid typestype inference

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Liquid types for array invariant synthesis
• Dependent Types for Low-Level Programming
• Extending liquid types to arrays
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• Types, bytes, and separation logic

Cited in

(18)

• Reasoning in the theory of heap: satisfiability and interpolation
• Lightweight shape analysis based on physical types
• Invariants synthesis over a combined domain for automated program verification
• Horn clause solvers for program verification
• Modular verification of higher-order functional programs
• Predicate abstraction for program verification
• Combining Model Checking and Deduction
• ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
• A Nonstandard Functional Programming Language
• Liquid types for array invariant synthesis
• Extending liquid types to arrays
• CCured, type-safe retrofitting of legacy code
• Unifying type checking and property checking for low-level code
• ICE-based refinement type discovery for higher-order functional programs
• Parameterized recursive refinement types for automated program verification
• Embedded domain specific verifiers
• On higher-order reachability games vs may reachability
• Bddl: A Type System for Binary Decision Diagrams

This page was built for publication: Low-level liquid types

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