Effective interactive proofs for higher-order imperative programs

DOI10.1145/1596550.1596565MaRDI QIDQ2936804zbMATH OpenOpenAlexFDO

Authors Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky

Publication date 6 January 2015

Published in Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL http://nrs.harvard.edu/urn-3:HUL.InstRepos:4686803

zbMATH Keywords

functional programmingdependent typesseparation logicinteractive proof assistants

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18)

Recommendations

• Ynot: dependent types for imperative programs
• Trace-based verification of imperative programs with I/O
• Efficient verification of imperative programs using auto2
• Imperative Functional Programming with Isabelle/HOL
• Verifying object-oriented programs with higher-order separation logic in Coq

Cited in

(25)

• Interactive proofs in higher-order concurrent separation logic
• Verification of non-functional programs using interpretations in type theory
• From proposition to program. Embedding the refinement calculus in Coq
• Verified characteristic formulae for CakeML
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• scientific article; zbMATH DE number 1420787 (Why is no real title available?)
• Symbolic execution proofs for higher order store programs
• Modular verification of programs with effects and effect handlers in Coq
• Refinement through restraint: bringing down the cost of verification
• Mechanized verification with sharing
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Trace-based verification of imperative programs with I/O
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• Modular development of certified program verifiers with a proof assistant,
• A program construction and verification tool for separation logic
• Reasoning about memory layouts
• Verifying object-oriented programs with higher-order separation logic in Coq
• Proof tactics for assertions in separation logic
• Specifying imperative ML-like programs using dynamic logic
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Specifying and verifying higher-order Rust iterators
• VeriML: typed computation of logical terms inside a language with effects
• Ynot: dependent types for imperative programs
• Coqpie: an IDE aimed at improving proof development productivity (rough diamond)
• Mechanizing the metatheory of mini-XQuery

Describes a project that uses

Uses Software

• Ynot
• Smallfoot
• Spec#
• Isabelle
• Coq

This page was built for publication: Effective interactive proofs for higher-order imperative programs

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