Confluence of the Pattern Matching Calculus

A mechanised confluence proof for the Pattern Matching Calculus (PMC) has been performed in Isabelle-2003.

This proof is largely based on the confluence proof for lambda-calculus performed in Isabelle-1999 by James Brotherston and René Vestergaard.

The formalisation consists of the following theories:

<theory dependency graph>

Among these, the central new theories are:

Only relatively minor adaptations of Brotherston and Vestergaard's proof were required to obtain the final confluence result:

The Isabelle-generated output for these theories is here.



Wolfram Kahl