Mathematics of Program Construction

Diagonal
Diagonals and Block-Ordered Relations
Roland Backhouse and Ed Voermans
Submitted for publication.
See here for the abstract.

Thins
The Thins Ordering on Relations
Ed Voermans, Jules Desharnais and Roland Backhouse
Submitted for publication.
See here for the abstract.


BGW2023
An example of goal-directed proof
Roland Backhouse, Walter Guttmann and Michael Winter
Submitted for publication.
See here for the abstract.

IndicesAndCores
The Index and Core of a Relation, With Applications to the Axiomatics of Relation Algebra
Roland Backhouse and Ed Voermans
Submitted for publication.
See here for the abstract.

OnDifunctions
On Difunctions
Roland Backhouse and José Nuno Oliveira
Journal of Logical and Algebraic Methods in Programming 134 (2023) 100878
See here for the abstract.

indices
The Index and Core of a Relation, With Applications to the Axiomatics of Relation Algebra and Block-Ordered Relations
Roland Backhouse and Ed Voermans
Working Document
See here for the abstract.


DifunBlockOrderedAndStaircase
Difunctions and Block-Ordered Relations
Roland Backhouse
Working Document
See here for the abstract.

BasicGraphTheory
Elements of Algorithmic Graph Theory. An Exercise in Combining Precision with Concision
Roland Backhouse, with contributions by Henk Doornbos, Roland Glueck and Jaap van der Woude
Working Document
See here for the abstract.


ComponentsAndAcyclicityJLAMP
Components and Acyclicity of Graphs. An Exercise in Combining Precision with Concision
Roland Backhouse, Henk Doornbos, Roland Glueck, Jaap van der Woude
J. Logical and Algebraic Methods in Programming, Vol. 124, January 2022, 100730, DOI:10.1016/jlamp.2021.100730
See here for the abstract.

Delegates
An analysis of repeated graph search
Roland Backhouse
In G.Hutton (Ed.): MPC2019, LNCS 11825, pp.1--31, 2019. DOI:10.13140/RG2.2.28481.81761
See here for the abstract.

FactorTheory
Factor Theory Made Calculational
Roland Backhouse
Draft. Comments welcome. DOI: 10.13140/RG.2.2.25718.40009
See here for the abstract.

UnityOfOpposites
Factor Theory and the Unity of Opposites
Roland Backhouse
J. Logical and Algebraic Methods in Programming, Vol.85, No. 5, Pp.824--826 (2016)
See here for the abstract.

PermutationInversion
In-situ Inversion of a Permutation
Roland Backhouse
Unpublished
See here for the abstract.


TorchProblem
The Capacity-C Torch Problem
Roland Backhouse and Hai Truong
Science of Computer Programming, 1 May 2015, Vol.102:76-107, doi:10.1016/j.scisco.2015.01.003
See here for the abstract.


FPtP
First-past-the-post Games
Roland Backhouse
Science of Computer Programming 85, Part B (1 June 2014), pp. 166-203, Selected Papers from Mathematics of Program Construction 2012, Jeremy Gibbons and Pablo Nogueira (Eds.). Available online 13-Aug-2013, Science of Computer Programming (2013), http://authors.elsevier.com/sd/article/S0167642313001640, DOI 10.1016/j.scico.2013.07.007.
See here for the abstract.

SCP11Solitaire
The Algorithmics of Solitaire-Like Game
Roland Backhouse, Wei Chen and Joao Ferreira
Science of Computer Programming 78 (2013), pp. 2029--2046, DOI: 10.1016/j.scico.2012.07.007
See here for the abstract.

AlgorithmDesignExercises
Exercises in Algorithm Design
Roland Backhouse
Unpublished Lecture Notes
See here for the abstract.


sum-two-squares
Designing an algorithmic proof of the two-squares theorem
Joao Ferreira
Mathematics of Program Construction. 10th International Conference, June 2010. Lecture Notes In Computer Science vol. 6120, Claude Bolduc, Jules Desharnais, Bechir Ktari (Eds.) pages 140--156. © Springer-Verlag 2010.
See here for the abstract.

BackhouseFerreiraSCP09
On Euclid's Algorithm and Elementary Number Theory
Roland Backhouse and Joao Ferreira
Science of Computer Programming, vol.76, no.3, pages 160 -- 180, 2011
See here for the abstract.

FerreiraThesis-a4-colour
Principles of Algorithmic Problem Solving
Joao Ferreira
PhD Thesis, School of Computer Science, University of Nottingham, 2010
See here for the abstract.

DynamicProgramming
The Elements of Dynamic Programming
Roland Backhouse
Unpublished Lecture Notes
See here for the abstract.



Solitaire
The Algorithmics of Solitaire-Like Game
Roland Backhouse, Wei Chen and Joao Ferreira
Mathematics of Program Construction. 10th International Conference, June 2010. Lecture Notes In Computer Science vol. 6120, Claude Bolduc, Jules Desharnais, Bechir Ktari (Eds.) pages 1--18. © Springer-Verlag 2010.
See here for the abstract.


which-mathis
Which Mathematics for the Information Society?
Joao F. Ferreira, Alexandra Mendes, Roland Backhouse and Luis S. Barbosa
Teaching Formal Methods, 2nd International Conference, November 2009. Lecture Notes In Computer Science vol. 5846, Jeremy Gibbons and Jose Nuno Oliveira (Eds.) pages 39--56. © Springer-Verlag 2009.
See here for the abstract.

PenneyGame
First-past-the-post Games
Roland Backhouse
J. Gibbons and P. Nogueira (Eds.), MPC 2012, LNCS 7342, pp.157-176, 2012. © Springer-Verlag
See here for the abstract.


FanClub
Meeting a Fanclub: A Lattice of Generic Shape Selectors
Roland Backhouse, Richard Bird and Paul Hoogendijk
Accepted for publication in Workshop on Generic Programming WGP09, 30th August 2009. This is the authors' version of the work. It is published here with the permission of ACM for your personal use. Not for redistribution. The definitive version of the article was published in WGP'09, Proceedings of the 2009 ACM SIGPLAN Workshop on Generic Programming, August 30, 2009, pp. 73--83, ISBN: 978-1-60558-510-9/09/08.
See here for the abstract.



mpcGeneralTorchProblem
The Capacity C Torch Problem
Roland Backhouse
In Mathematics of Program Construction 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008, pages 57-78 © Springer-Verlag
See here for the abstract.

GenericTermination
Datatype-Generic Termination Proofs
Roland Backhouse and Henk Doornbos
In Theory of Computing Systems (2008) 43: 362--393, DOI: 10.1007/s00224-007-9056-z © Springer-Verlag
See here for the abstract.


RecountingRationalsTwice
Recounting the Rationals. Twice!
Roland Backhouse and Joao Ferreira
In Mathematics of Program Construction 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008, pages 79-91. © Springer-Verlag
See here for the abstract.

GenericReasoning
Datatype-generic Reasoning
Roland Backhouse
In Logical Approaches to Computational Barriers, Arnold Beckmann, Ulrich Berger, Benedikt L\"owe, John V. Tucker (Eds.), Springer-Verlag, LNCS 3988, pp. 21--34 © Springer-Verlag
See here for the abstract.

CalculationalCombinatorics
Calculational Combinatorics
Roland Backhouse and Arjan Mooij
Unpublished
See here for the abstract.


QuantifierExercises
Exercises in Quantifier Manipulation
Roland Backhouse and Diethard Michaelis
In Mathematics of Program Construction 2006, Tarmo Uustalu (Ed.), Springer-Verlag, LNCS 4014, pp. 70--81 © Springer-Verlag
See here for the abstract.

IncreasingSequences
A De Morgan-like Theorem for Increasing Sequences
Roland Backhouse and Diethard Michaelis
Unpublished. (Shortened version included in "Exercises in Quantifier Manipulation", MPC 2006.)
See here for the abstract.

AbsoluteDifferences
A Problem of Absolute Differences
Roland Backhouse and Diethard Michaelis
Unpublished. (Included in "Exercises in Quantifier Manipulation", MPC 2006.)
See here for the abstract.


icalp77_paper
Factor Graphs, Failure Functions and Bi-Trees
R.C. Backhouse and R.K. Lutz
In Fourth Colloquium on Automata, Languages and Programming, A. Salomaa and M. Steinby (Eds.), Springer-Verlag, LNCS 52, 1977, pp. 61--75
See here for the abstract.

ClosureAlgorithms
Closure Algorithms and the Star-Height Problem of Regular Algorithms
Roland Backhouse
PhD thesis, University of London, 1975.
See here for the abstract.


FactorGraphs
Factor Graphs and Factor Matrices
Roland Backhouse
Extract from Closure Algorithms and the Star Height Problem of Regular Languages, PhD thesis, University of London, 1975.
See here for the abstract.


MEXnos
A Calculational Presentation of Impartial Two-Person Games
Roland Backhouse and Diethard Michaelis
Abstract presented at RelMiCS8
See here for the abstract.

Path-findingProblems
Regular Algebra Applied to Path-Finding Problems
R.C. Backhouse and B.A.Carré
J.Inst.Maths.Applics (1975) 15, 161--186. Reproduced with the permission of Oxford University Press.
See here for the abstract.


GaussGaussJordanComparison
A Comparison of Gaussian and Gauss-Jordan Elimination in Regular Algebra
R.C. Backhouse and B.A.Carré
International Journal of Computer Mathematics 10, 3--4, 311--325, doi: 10.1080/00207168208803290
See here for the abstract.

RegAlgLangProblems
Regular Algebra Applied to Language Problems
Roland Backhouse
Journal of Logic and Algebraic Programming. 66 (2006) 71--111. © Elsevier Science Direct.
See here for the abstract.

WinningStrategies
Fixed-Point Characterisation of Winning Strategies in Impartial Games
Roland Backhouse and Diethard Michaelis
Abridged version (omitting proofs) in LNCS 3051, Relational and Kleene-Algebraic Methods in Computer Science, Rudolf Berghammer, Bernhard Möller and Georg Struth (Eds.), pp 34--47, 2004 © Springer-Verlag)
See here for the abstract.

SafetyForFree
Safety of Abstract Interpretations for Free,via Logical Relations and Galois Connections
Kevin Backhouse and Roland Backhouse
In Science of Computer Programming, vol. 15, nos. 1--2, pp. 153--196, 2004.
See here for the abstract.

GPschool
Generic Properties of Datatypes
Roland Backhouse and Paul Hoogendijk
Presented at Summer School on Generic Programming, Oxford, August 2002 © Springer-Verlag.
See here for the abstract.

GCsAndLRs
Galois Connections and Logical Relations
Kevin Backhouse and Roland Backhouse
Int. Conf. on Mathematics of Program Construction, Dagstuhl, Germany, July 2002. Springer Verlag LNCS 2386, pp. 23--39. © Springer-Verlag
See here for the abstract.

Inaugural
Mathematics and Programming. A Revolution in the Art of Effective Reasoning
Roland Backhouse
Inaugural lecture, School of Computer Science and IT, University of Nottingham, 24th October 2001.
See here for the abstract.


RecurProgConstr
Mathematics of Recursive Program Construction
Henk Doornbos and Roland Backhouse
Unpublished.
See here for the abstract.

Find
Find (Refined)
Roland Backhouse
Unpublished.
See here for the abstract.

FusionESOP
Fusion on Languages
Roland Backhouse
10th European Symposium on Programming, ESOP 2001. Springer LNCS 2028, pp. 107--121. © Springer-Verlag
See here for the abstract.

Hanoi
The Associativity of Equivalence and the Towers of Hanoi Problem
Roland Backhouse and Maarten Fokkinga
Information Processing Letters, 77 (Feb. 2001) pp 71--76.
See here for the abstract.

FPandGC
Galois Connections and Fixed Point Calculus
Roland Backhouse
Lecture Notes for module Programming Algebra, Nottingham, 2001
See here for the abstract.


acmmpc
Fixed Point Calculus
Roland Backhouse
Presented at the Summer School and Workshop on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Oxford, April 11--14, 2000.

A shortened version of this paper appears in the published proceedings of the Summer School Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS 2297, 2002, pp. 89--148. © Springer-Verlag.
See here for the abstract.

AlgebraOfProgramTermination
Algebra of Program Termination
Henk Doornbos and Roland Backhouse
Presented at the Summer School and Workshop on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Oxford, April 11--14, 2000.

Proceedings of the Summer School Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS 2297, 2002, pp. 89--148. © Springer-Verlag.
See here for the abstract.


MathSpadFM99
Towards Tool Support for Program Verification and Construction
Richard Verhoeven and Roland Backhouse
FM '99 -- Formal Methods, Jeanette Wing, Jim Woodcock and Jim Davies (Eds.), LNCS 1709, pp. 1128--1146, September 1999
See here for the abstract.

VoermansThesis
Inductive Datatypes with Laws and Subtyping --- A Relational Model
Ed Voermans
Ph.D.thesis, Eindhoven University of Technology, January 1999
See here for the abstract.

FiCS99
Final Dialgebras: From Categories to Allegories
Roland Backhouse and Paul Hoogendijk
Theoretical Informatics, Vol. 33, Nos. 4/5, 1999, pp. 401 --426
See here for the abstract.

AFP-Portugal
Generic Programming. An Introduction
Roland Backhouse, Patrik Jansson, Johan Jeuring, Lambert Meertens
Presented at the 3rd International Summer School on Advanced Functional Programming, Braga, Portugal, 12th-19th September, 1998
See here for the abstract.


UITP98
Extracting Proofs from Documents
Roland Backhouse and Richard Verhoeven
Presented at Workshop on User Interfaces for Theorem Provers UITP'98, Eindhoven, The Netherlands.
See here for the abstract.

PairAlgebras
Pair Algebras and Galois Connections
Roland Backhouse
Information Processing Letters, Vol.67, No.4, 31 August 1998, pp.169--176
See here for the abstract.

RoundRobin
Calculating a Round-Robin Scheduler
Matteo Vaccari and Roland Backhouse
International Conference on Mathematics of Program Construction, Marstrand, Sweden, June 1998, LNCS 1422, pp.365--382
See here for the abstract.

http://matteo.vaccari.name/tesi
Calculational Derivation of Circuits
Matteo Vaccari
Ph.D. Thesis, Universita degli Studi di Milano, Italy, May 1998
See here for the abstract.

MathSpad
MathSpad: A System for On-Line Preparation of Mathematical Documents
Roland Backhouse and Richard Verhoeven
Software--Concepts and Tools (1997) 18: 80--89
See here for the abstract.

commute
When do datatypes commute?
Paul Hoogendijk and Roland Backhouse
Category Theory and Computer Science, LNCS 1290, September 1997, pp. 242--260.
See here for the abstract.

HoogendijkThesis
A Generic Theory of Data Types
Paul Hoogendijk
Ph.D. Thesis, Eindhoven University of Technology, 1997.
See here for the abstract.


regpaper
Deriving a systolic regular language recognizer
Matteo Vaccari and Roland Backhouse
IFIP TC2 Working Conference on Algorithmic Languages and Calculi, February 1997.
See here for the abstract.

reductivity
Reductivity.
Henk Doornbos and Roland Backhouse.
Science of Computer Programming, 26, pp. 217--236, 1996.
See here for the abstract.

CatTheory
Category Theory As Coherently Constructive Lattice Theory
Roland Backhouse, Marcel Bijsterveld, Rik van Geldrop and Jaap van der Woude.
Working Document, July 1994. Latest version, December 1996.
See here for the abstract.

whatsdt
What is a data type?
Paul Hoogendijk and Oege de Moor
CS report 96-16, Eindhoven University of Technology. November 1996
See here for the abstract.

redargprogcons
Reductivity Arguments and Program Construction
Henk Doornbos
Ph.D. Thesis, Eindhoven University of Technology, 1996.
See here for the abstract.

CalcWithMathSpad
MathSpad, Tool Support for the Calculational Method
Roland Backhouse and Richard Verhoeven
February 1996
See here for the abstract.

catfixpnt
Categorical Fixed Point Rules
Roland Backhouse, Marcel Bijsterveld, Rik van Geldrop and Jaap van der Woude
D. Pitt and D.E. Rydeheard and P. Johnstone, editors, Category Theory and Computer Science, 6th International Conference, volume 953 of LNCS, pages 159--179. Springer-Verlag, 1995.
See here for the abstract.

mpc
Induction and Recursion on Datatypes
Henk Doornbos and Roland Backhouse
B. Moller, editor, Mathematics of Program Construction, 3rd Internatinal Conference, volume 947 of LNCS, pages 242-256. Springer-Verslag, July 1995.
See here for the abstract.

dbpl
A database calculus based on strong monads and partial functions.
Eerke Boiten and Paul Hoogendijk.
March 1995.
See here for the abstract.

MPCarticle95
Mathematics of Program Construction
Roland Backhouse
Science of Computer Programming
See here for the abstract.


MathSpad
MathSpad: A system for on-line preparation of mathematical documents
Roland Backhouse, Richard Verhoeven and Olaf Weber
Eindhoven University of Technology, Computing Science Report 95/10, March 1995.
See here for the abstract.


BeautifulTheorem
Category Theory as Coherently Constructive Lattice Theory: An Illustration
Roland Backhouse and Marcel Bijsterveld
CS report 94-43, Eindhoven University of Technology. November 1994.
See here for the abstract.

MadeCalculational
A Calculation Approach to Mathematical Induction
Henk Doornbos, Roland Backhouse and Jaap van der Woude
In Theoretical Computer Science 179 (1997) 103--105
See here for the abstract.

CalculatingPathAlgorithms
Calculating path algorithms
Roland C. Backhouse, J.P.H.W. van den Eijnde, A.J.M. van Gasteren
Science of Computer Programming 22 (1994) 3--19, doi: 10.1016/0167-6423(94)90005-1 © 1994 Elsevier Science B.V.
See here for the abstract.

RelationalProgrammingLaws
Relational programming laws in the tree, list, bag, set hierarchy.
Paul F. Hoogendijk and Roland C. Backhouse
Science of Computer Programming 22 (1994) 1--2, pages 67--105
See here for the abstract.

SchroederBernstein
The Schröder-Bernstein Theorem
Roland C. Backhouse
Unpublished. 16th Decembere 1993
See here for the abstract.


path-algor
Calculating a Path Algorithm.
Roland C. Backhouse and A.J.M. van Gasteren.
R.S. Bird, C.C. Morgan, and J.C.P. Woodcock, editors, Mathematics of Program Construction. 2nd International Conference, June/July 1992, volume 669 of Lecture Notes in Computer Science, pages 32--44. Springer Verlag, 1993. For extended version see " Calculating Path Algorithms. Roland C. Backhouse and J.P.H.W. van den Eijnde and A.J.M. van Gasteren".
See here for the abstract.

brazilschool
Elements of a Relational Theory of Datatypes.
Roland Backhouse and Paul Hoogendijk.
In B. Moller, H.A. Partsch, and S.A. Schuman, editors, Formal Program Development. Proc. IFIP TC2/WG 2.1 State of the Art Seminar, Rio de Janeiro, Jan. 1992, volume 755 of LNCS, pages 7-42. Springer-Verlag, 1993.
See here for the abstract.

skel
Transformational development of (parallel) programs using skeletons.
E.A. Boiten, A.M. Geerling & H.A. Partsch.
Computing Science in the Netherlands 1993. pages 97--108, 1993.
See here for the abstract.

boom
(Relational) Programming Laws in the Boom Hierarchy of Types.
Paul F. Hoogendijk.
Mathematics of Program Construction. 2nd International Conference, June/July 1992. Lecture Notes In Computer Science vol. 669, pages 163--190. Springer Verlag, 1993. For extended version see "Relational Programmig Laws in the Tree, List, Bag and Set Hierarchy. Paul F. Hoogendijk and Roland C. Backhouse."
See here for the abstract.

monad
Monad Decomposition.
Roland C. Backhouse.
Unpublished manuscript, April 1993.
See here for the abstract.

book
A Relational Theory of Datatypes
Chritiene Aarts, Roland C. Backhouse, Paul Hoogendijk, Ed Voermans and Jaap van der Woude.
Working document, December 1992.
See here for the abstract.

zip
A Class of Commuting Relators
Roland Backhouse, Henk Doornbos and Paul Hoogendijk.
Presented at STOP workshop, September 1992.
See here for the abstract.

perspective
A Relational Perspective on Types With Laws.
Jaap van der Woude and Ed Voermans.
Unpublished manuscript, January 1993.
See here for the abstract.

demon
Demonic Operators and Monotype Factors.
Roland Backhouse and Jaap van der Woude.
Final version in Mathematical Structures in Computer Science, 3(4): 417-433, December 1993.
See here for the abstract.

proginv
Relational programming, program inversion and the derivation of parsing algorithms.
Ed Knapen.
Graduating Disertation, Eindhoven University of Technology, November 1993.
See here for the abstract.

isos
Constructive Lattice Theory.
Roland Backhouse.
Unpublished manuscript. October 1993.
See here for the abstract.

perorder
Domain Operators and Domain Kinds.
Roland Backhouse and Jaap van der Woude.
Unpublished manuscript, September 1993.
See here for the abstract.

galois
Galois Connections Presented Calculationally
C.J. Aarts.
Graduating Disertation, Eindhoven University of Technology, July 1992.
(No abstract available.)

InitialAlgebraCongruences
Congruences on Initial Algebras
Roland C. Backhouse, Grant Malcolm and Jaap van der Woude
Technical Report, Technische Universiteit Eindhoven, 1991
See here for the abstract.


InducedCongruences
On Induced Congruences
Roland Backhouse and Grant Malcolm
Bulletin of the EATCS, vol. 40, pp. 201--206, 1990.
See here for the abstract.

RelationalCatamorphisms
Relational Catamorphisms
Backhouse, R.C. and Bruin, P. de and Malcolm, G. and Voermans, T.S. and Woude, J. van der"
In Proceedings of the IFIP TC2/WG2.1 Working Conference Constructing Programs from Specifications, 1991, M{\"o}ller B. (Ed.), Elsevier Science Publishers B.V., pp. 287--318
See here for the abstract.

ErgonomicsOfNotation
Some Ergonomics of Mathematical Notation
Roland C. Backhouse
Unpublished, September 1991
See here for the abstract.


texas
Constructive Type Theory. A Perspective from Computing Science
Roland C. Backhouse
In Formal Development of Programs and Proofs, Edited by Edsger W. Dijkstra, Addison-Wesley, 1990
See here for the abstract.


formality
Making Formality Work For Us.
R.C. Backhouse
EATCS Bulletin, vol. 38, June 1989, pages 219-249.
See here for the abstract.


DIYTypeTheory
Do-it-Yourself Type Theory
Roland Backhouse, Paul Chisholm, Grant Malcolm and Erik Saaman
Formal Aspects of Computing (1989) 1: 19--84. © 1989 BCS
See here for the abstract.

exploration
An Exploration of the Bird-Meertens Formalism.
Roland Backhouse.
Technical Report CS8810, Department of Mathematics and Computing Science, University of Groningen, 1988. This paper has been superceded by: "Elements of a relational theory of datatypes. Roland Backhouse and Paul Hoogendijk." and "Relational programming laws in the tree, list, bag and set hierarchy. Paul F. Hoogendijk and Roland C. Backhouse."
See here for the abstract.

NonRedundantRegularExpressions
Non-redundant regular expressions and real arithmetic: Proof of a lemma due to Tarjan
Roland C. Backhouse
Department of Computer Science, Heriot-Watt University, Technical Report no. 9, August 1980
See here for the abstract.

FactorGraphsFailureFunctionsBiTrees
Factor Graphs, Failure Functions and BiTrees
Roland C.\ Backhouse and Rüdiger K. Lutz
Department of Computer Science, Heriot-Watt University, Technical Report no. 4, October 1976
See here for the abstract.