Refinement through restraint: bringing down the cost of verification
From MaRDI portal
Publication:2982005
DOI10.1145/2951913.2951940zbMath1361.68045MaRDI QIDQ2982005
Liam O'Connor, Yutaka Nagashima, Christine Rizkallah, Thomas D. Sewell, Toby Murray, Japheth Lim, Zilin Chen, Gerwin Klein, Sidney Amani
Publication date: 10 May 2017
Published in: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/2951913.2951940
68N15: Theory of programming languages
68N18: Functional programming and lambda calculus
68Q55: Semantics in the theory of computing
68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Related Items
The verified CakeML compiler backend, Ready,Set, Verify! Applyinghs-to-coqto real-world Haskell code, Cogent: uniqueness types and certifying compilation, Flashix: modular verification of a concurrent and crash-safe flash file system, A Framework for the Automatic Formal Verification of Refinement from Cogent to C, Verified Characteristic Formulae for CakeML
Uses Software