- Author:
- Roland Backhouse
From the Publisher:
The book covers the elements of logic and program correctness that form the foundations of further study - the logical connectives and their algebraic properties, induction, quantifiers and program construction rules. Substantial examples of program construction are included. Many exercises are provided, all with detailed solutions.
Cited By
Bahr P and Hutton G (2022). Monadic compiler calculation (functional pearl), Proceedings of the ACM on Programming Languages, 6:ICFP, (80-108), Online publication date: 29-Aug-2022.- Ettinger R Lessons of Formal Program Design in Dafny Formal Methods Teaching, (84-100)
- Boisseau G and Gibbons J (2018). What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl), Proceedings of the ACM on Programming Languages, 2:ICFP, (1-27), Online publication date: 30-Jul-2018.
- Chaudhari D and Damani O Introducing Formal Methods via Program Derivation Proceedings of the 2015 ACM Conference on Innovation and Technology in Computer Science Education, (266-271)
- Backhouse R First-Past-the-Post games Proceedings of the 11th international conference on Mathematics of Program Construction, (157-176)
- Mu S and Oliveira J Programming from galois connections Proceedings of the 12th international conference on Relational and algebraic methods in computer science, (294-313)
- Stewart A (2011). A programming model for BSP with partitioned synchronisation, Formal Aspects of Computing, 23:4, (421-432), Online publication date: 1-Jul-2011.
- Bohórquez V J (2010). An elementary and unified approach to program correctness, Formal Aspects of Computing, 22:5, (611-627), Online publication date: 1-Sep-2010.
- Morris J, Bunkenburg A and Tyrrell M (2009). Term transformers, ACM Transactions on Programming Languages and Systems (TOPLAS), 31:4, (1-42), Online publication date: 1-May-2009.
- Blanco J, Losano L, Aguirre N, Novaira M, Permigiani S and Scilingo G (2009). An introductory course on programming based on formal specification and program calculation, ACM SIGCSE Bulletin, 41:2, (31-37), Online publication date: 25-Jun-2009.
- Rocha C and Meseguer J Theorem proving modulo based on Boolean equational procedures Proceedings of the 10th international conference on Relational and kleene algebra methods in computer science, and 5th international conference on Applications of kleene algebra, (337-351)
- Backhouse R and Michaelis D Exercises in quantifier manipulation Proceedings of the 8th international conference on Mathematics of Program Construction, (69-81)
Recommendations
Completing Herbelin's programme
TLCA'07: Proceedings of the 8th international conference on Typed lambda calculi and applicationsIn 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent calculus into a variant of the λ-calculus, specifically a variant which manipulates ...
Building program construction and verification tools from algebraic principles
AbstractWe present a principled modular approach to the development of construction and verification tools for imperative programs, in which the control flow and the data flow are cleanly separated. Our simplest verification tool uses Kleene algebra with ...
Disjunctive Logic Program = Horn Program + Control Program
JELIA '98: Proceedings of the European Workshop on Logics in Artificial IntelligenceThis paper presents an alternative view on propositional disjunctive logic program: Disjunctive program = Control program + Horn program. For this we introduce a program transformation which transforms a disjunctive logic program into a Horn program and ...