A Hoare Logic for Call-by-Value Functional Programs

DOI10.1007/978-3-540-70594-9_17zbMATH Open1157.68023OpenAlexW1590844387MaRDI QIDQ3521994FDOQ3521994

François Pottier, Yann Régis-Gianas

Publication date: 28 August 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70594-9_17

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cited In (6)

• Specifying Imperative ML-Like Programs Using Dynamic Logic
• Extended call-by-push-value: reasoning about effectful programs and evaluation order
• A formal equational theory for call-by-push-value
• Roles, stacks, histories: A triple for Hoare
• Specifying and verifying higher-order Rust iterators
• On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

Uses Software

• KRAKATOA
• JML
• ETPS
• ESC/Java

This page was built for publication: A Hoare Logic for Call-by-Value Functional Programs

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