We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.PL

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Programming Languages

Title: Tutorial on implementing Hoare logic for imperative programs in Haskell

Abstract: Using the programming language Haskell, we introduce an implementation of propositional calculus, number theory, and a simple imperative language that can evaluate arithmetic and boolean expressions. Finally, we provide an implementation of Hoare's logic which will allow us to deduce facts about programs without the need for a full evaluation.
Comments: Added sample implementation for H-Consequence, H-While, and another example; Added CoI section, tweaks to labels for 'boptimize'; Improved Hoare logic implementation by relying on actual Propositional calculus and Number theory systems, rather than toy optimization functions; improve formula printer; small tweak updates. Associated files are available at this https URL
Subjects: Programming Languages (cs.PL); Logic in Computer Science (cs.LO)
Cite as: arXiv:2101.11320 [cs.PL]
  (or arXiv:2101.11320v9 [cs.PL] for this version)

Submission history

From: Boro Sitnikovski [view email]
[v1] Wed, 27 Jan 2021 11:14:37 GMT (20kb)
[v2] Wed, 17 Feb 2021 15:50:23 GMT (20kb)
[v3] Thu, 4 Mar 2021 23:14:03 GMT (21kb)
[v4] Sun, 25 Apr 2021 10:34:11 GMT (24kb)
[v5] Wed, 28 Apr 2021 20:42:29 GMT (24kb)
[v6] Tue, 4 May 2021 18:19:11 GMT (24kb)
[v7] Tue, 11 May 2021 06:50:03 GMT (24kb)
[v8] Wed, 2 Jun 2021 10:36:34 GMT (25kb)
[v9] Sun, 6 Jun 2021 20:19:52 GMT (25kb)

Link back to: arXiv, form interface, contact.