A Hoare Logic for Call-by-Value Functional Programs

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

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

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

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 (10)

• Title not available (Why is that?)
• Program logics for sequential higher-order control
• Extended call-by-push-value: reasoning about effectful programs and evaluation order
• Theorem Proving in Higher Order Logics
• Roles, stacks, histories: a triple for Hoare
• A formal equational theory for call-by-push-value
• Title not available (Why is that?)
• Specifying imperative ML-like programs using dynamic logic
• 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)