Mathematical Methodology and Algorithmic Problem Solving

Books

• Program Construction: Calculating Implementations from Specifications, Roland Backhouse
  ( Publisher link , E-book link, Amazon link , ACM link )

• On the Shape of Mathematical Arguments, Antonetta J.M. van Gasteren
  ( Publisher Link , E-book link ; Amazon link , ACM link )

• Predicate Calculus and Program Semantics, Edsger W. Dijkstra and Carel S. Scholten
  ( ACM link , Amazon link )

• A Discipline of Programming, Edsger W. Dijkstra
  ( ACM link , E-book link , Amazon link )

• Logical Approach To Discrete Math, David Gries and Fred B. Schneider
  ( Author link , Publisher link , ACM link , Amazon link )

• The Science of Programming, David Gries
  ( ACM link , Amazon link )

• Program Construction (International Summer School), Edsger W. Dijkstra and David Gries, LNCS Springer
  E-book link

Articles and Notes

Documents named EWDxxx, where xxx is a positive natural number, are notes written by Edsger W. Dijkstra. Similarly:

• JAWxxx - Jeremy Weissmann
• JFFxxx - Joao Fernando Ferreira
• WFxxx - Wim Feijen

Still to sort

• 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

• A Calculational Presentation of Impartial Two-Person Games, Roland Backhouse and Diethard Michaelis, Abstract presented at RelMiCS8?

• 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

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

• 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 Calculation Approach to Mathematical Induction, Henk Doornbos, Roland Backhouse and Jaap van der Woude, In Theoretical Computer Science 179 (1997) 103--10

Mathematical Methodology

Introductory documents

The following documents introduce our line of thought.

• 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.
• EWD619 - Essays on the nature and role of mathematical elegance (1) (HTML, PDF)
• EWD641 - On the interplay between mathematics and programming (HTML, PDF)
• EWD655 - Essays on the nature and role of mathematical elegance (3): On notation (A sequel to EWD619) (HTML, PDF)
• EWD1059 - 0 Preface (Mathematical Methodology) (HTML, PDF)
• EWD1063 - An introductory example (Mathematical Methodology) (PDF)
• EWD1067 - A very first introductory example (Mathematical Methodology) (HTML, PDF)
• The Calculational Method, Information Processing Letters, Volume 53, Issue 3, 10 February 1995, Page 121

Notation and Proof Formats

• EWD1068 - On the quality criteria for mathematical writing (Mathematical Methodology) (HTML, PDF)
• EWD999 - Our proof format (PDF)
• EWD1070 - For brevity's sake (Mathematical Methodology) (HTML, PDF)
• EWD1300 - The notational conventions I adopted, and why (HTML, PDF)

Monotonicity

• JAW44 - Different types of symbol dynamics for Leibniz and monotonicity (PDF)

Algorithmic Problem Solving

• Lecture notes on Algorithmic Problem Solving, Roland Backhouse
• Find (Refined), Roland Backhouse, Unpublished
• Proving Program Correctness, Apurva Mehta, Undergraduate project
• 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, 199
• Recounting the Rationals: Twice!, Roland Backhouse and Joao Ferreira

People (alphabetical order of surname)

List of people interested in mathematical methodology and in particular, in the calculational method.

• Roland Backhouse
• Lex Bilsma
• Edsger Dijkstra (1930 - 2002)
• Wim Feijen
• Joao Ferreira
• Eric Hehner
• David Gries
• Eric Macaulay
• Apurva Mehta
• Arjan Mooij
• Tom Verhoeff
• Jeremy Weissmann

Tools

• MathSpad

Other websites

• mathmeth.com
• funmath.be

-- JoaoFerreira - 30 May 2007

50 Recent Changes in TWiki Web retrieved at 18:01 (GMT)

See also: RSS feed, recent changes with 50, 100, 200, 500, 1000 topics, all changes

See also the faster WebTopicList

• TWikiGuest - example@your.company

Web Changes Notification Service

Each TWiki web has an automatic e-mail notification service that sends you an e-mail with links to all of the topics modified since the last alert.

Users subscribe to email notifications using their WikiName or an alternative email address, and can specify the webs/topics they wish to track using one of these bullet list formats:

three spaces * [ webname . ] wikiName - SMTP mail address
three spaces * [ webName . ] wikiName
three spaces * SMTP mail address
three spaces * SMTP mail address : topics
three spaces * [ webname . ] wikiName : topics

In the above examples, topics is a space-separated list of topic names. The user may further customize the specific content they will receive using the following formats:

• Specify topics without a Web. prefix
• Topics must exist in this web.
• Topics may be specified using * wildcards
• Each topic may optionally be preceded by a '+' or '-' sign. The '+' sign means "subscribe to this topic" (the same as not putting anything). The '-' sign means "unsubscribe" or "don't send notifications regarding this topic". This allows users to elect to filter out certain topics (and their children, to an arbitrary depth). Topic filters ('-') take precedence over topic includes ('+').
• Each topic may optionally be followed by an integer in parentheses, indicating the depth of the tree of children below that topic. Changes in all these children will be detected and reported along with changes to the topic itself. Note This uses the TWiki "Topic parent" feature.
• Each topic may optionally be immediately followed by an exclamation mark ! or a question mark ? with no intervening spaces, indicating that the topic (and children if there is a tree depth specifier as well) should be mailed out as complete topics instead of change summaries. ! causes the topic to be mailed every time even if there have been no changes, ? will mail the topic only if there have been changes to it. This only makes sense for subscriptions.

For example: Subscribe Daisy to all changes to topics in this web.

   * daisy.cutter@flowers.com

   * daisy.cutter@flowers.com: Web*

   * TWiki.DaisyCutter: Petal* (1) TWiki.WeedKillers (3) Pretty*Flowers

   * TWiki.StarTrekFan: Star* - *Wars - *sInTheirEyes - *shipTroopers

   * daisy@flowers.com: TWiki.NewsLetter?

   * buttercup@flowers.com: TWiki.NewsLetter! (1)

   * TWiki.GardenGroup: TWiki.AllNewsLetters? (3)
   * petunia@flowers.com: - TWiki.ManureNewsLetter

If a TWiki group is listed for notification, the group will be recursively expanded to the e-mail addresses of all members.

Tip: List names in alphabetical order to make it easier to find the names.

Note for System Administrators: Notification is supported by an add-on to the TWiki kernel called the MailerContrib. See the MailerContrib topic for details of how to set up this service.

Note: If you prefer a news feed, point your reader to WebRss (for RSS 1.0 feeds) or WebAtom (for ATOM 1.0 feeds). Learn more at WebRssBase and WebAtomBase, respectively.

Related topics: WebChangesAlert, TWikiUsers, TWikiRegistration

Warning

Can't INCLUDE TWiki.WebSearchAdvanced repeatedly, topic is already included.

Create New Topic in Personal/JFF Web

Once you have created the topic, consider adding links in related topics to the new topic so that there are more ways people can discover it.