A Hoare Logic for Call-by-Value Functional Programs

DOI10.1007/978-3-540-70594-9_17MaRDI QIDQ3521994zbMATH OpenOpenAlexFDO

Authors Yann Régis-Gianas, François Pottier

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

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

Recommendations

• scientific article; zbMATH DE number 2110621
• Program logics for sequential higher-order control
• Automata, Languages and Programming
• Theorem Proving in Higher Order Logics
• scientific article; zbMATH DE number 2154396

Cited in

(11)

• A formal equational theory for call-by-push-value
• Roles, stacks, histories: a triple for Hoare
• Specifying imperative ML-like programs using dynamic logic
• Program logics for sequential higher-order control
• scientific article; zbMATH DE number 2154396 (Why is no real title available?)
• scientific article; zbMATH DE number 2090132 (Why is no real title available?)
• On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
• Theorem Proving in Higher Order Logics
• Extended call-by-push-value: reasoning about effectful programs and evaluation order
• Specifying and verifying higher-order Rust iterators
• Dependent type refinements for futures

Describes a project that uses

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)