Effective interactive proofs for higher-order imperative programs
From MaRDI portal
Publication:2936804
DOI10.1145/1596550.1596565zbMath1302.68087OpenAlexW2129671708MaRDI QIDQ2936804
Greg Morrisett, Avraham Shinnar, Ryan Wisnesky, Gregory Malecha, Adam Chlipala
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
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Symbolic execution proofs for higher order store programs, A Program Construction and Verification Tool for Separation Logic, Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, Trace-based verification of imperative programs with I/O, Proof tactics for assertions in separation logic, Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language, Reasoning about memory layouts, Verified Characteristic Formulae for CakeML, Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits, From Proposition to Program, Specifying Imperative ML-Like Programs Using Dynamic Logic, CoqPIE: An IDE Aimed at Improving Proof Development Productivity, Mechanizing the Metatheory of mini-XQuery
Uses Software
