Mathematics of Program Construction

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.


TorchProblem
The Capacity-C Torch Problem
Roland Backhouse and Hai Truong
Submitted for publication.
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.

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.



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.

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.


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.

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.

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.


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.


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. (Bound copies are available (while stocks last) by writing to the author or Roland Backhouse.)
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.

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.

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.)

formality
Making Formality Work For Us.
R.C. Backhouse
EATCS Bulletin, vol. 38, June 1989, pages 219-249.
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.