A Hoare Logic for Call-by-Value Functional Programs

DOI10.1007/978-3-540-70594-9_17zbMath1157.68023OpenAlexW1590844387MaRDI QIDQ3521994

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

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

Related Items (3)

On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics ⋮ Roles, stacks, histories: A triple for Hoare ⋮ Specifying Imperative ML-Like Programs Using Dynamic Logic

Uses Software

• KRAKATOA
• JML
• ETPS
• ESC/Java

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