A language-based approach to functionally correct imperative programming

DOI10.1145/1086365.1086400MaRDI QIDQ2936790zbMATH OpenOpenAlexFDO

Authors Edwin Westbrook, Aaron Stump, Ian Wehrman

Publication date 6 January 2015

Published in Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://openscholarship.wustl.edu/cse_research/951

zbMATH Keywords

dependent typesprogram verificationRSPRSP1

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Integrated approach to analysis and verification of imperative programs
• scientific article; zbMATH DE number 140007
• Cogent: uniqueness types and certifying compilation
• Language-based program verification via expressive types
• Imperative Functional Programming with Isabelle/HOL

Cited in

(9)

• Implementing hybrid semantics: from functional to imperative
• scientific article; zbMATH DE number 1615254 (Why is no real title available?)
• Type-level computation using narrowing in \(\Omega\)mega
• Language-based program verification via expressive types
• Imperative LF meta-programming
• Integrated approach to analysis and verification of imperative programs
• Hoare type theory, polymorphism and separation
• scientific article; zbMATH DE number 140007 (Why is no real title available?)
• The correctness of a code generator for a functional language

Describes a project that uses

Uses Software

• LEGO
• Cayenne
• Twelf
• Coq

This page was built for publication: A language-based approach to functionally correct imperative programming

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