@TechReport{Kahl-2003b,
  author = 	 {Wolfram Kahl},
  title = 	 {Basic Pattern Matching Calculi:
                  Syntax, Reduction, Confluence, and Normalisation},
  institution =  {Software Quality Research Laboratory, McMaster Univ.},
  year = 	 {2003},
  type = 	 {SQRL Report},
  number = 	 {16},
  note = {available from\\
          \textsf{http://www.cas.mcmaster.ca/sqrl/sqrl\_reports.html}},
  month = 	 OCT,
  abstract = {The pattern matching calculus is a refinement of
      $\lambda$-calculus that integrates mechanisms appropriate for
      fine-grained modelling of non-strict pattern matching.

      In comparison with the functional rewriting strategy that is
      usually employed to define the operational semantics of
      pattern-matching in non-strict functional programming languages
      like Haskell or Clean, the pattern matching calculus allows
      simpler and more local definitions to achieve the same effects.

      The main device of the calculus is to further emphasise the
      clear distinction between matching failure and undefinedness
      already discussed in the literature by embedding into
      expressions the separate syntactic category of matchings. This
      separation is also important to properly restrain the possible
      effects of the non-monotonicity that a na\"{\i}ve treatment of
      matching alternatives would exhibit. The language arising from
      that distinction turns out to naturally encompass the pattern
      guards of Peyton Jones and Erwig and conventional Boolean guards
      as special cases of the intermediate stages of matching reduction.

      By allowing a confluent reduction system and a normalising
      strategy, the pattern matching calculus provides a new basis for
      operational semantics of non-strict programming languages and
      also for implementations.}
}