
 Lambda Calculus with patterns
 The lambda phicalculus is an extension of the lambdacalculus with a pattern matching facility. The form of the argument of a function can be specified and hence lambda phicalculus is more convenient than ordinary lambdacalculus. We explore the basic theory of lambdacalculus, investigating properties such as confluence. In doing so, we find some requirements for patterns that guarantee confluence. Our work can be seen as giving some foundations for implementations of functional programming languages.
 Pure Pattern Calculus
 The pure pattern calculus generalises the pure lambdacal culus by basing computation on patternmatching instead of betareduc tion. The simplicity and power of the calculus derive from allowing any term to be a pattern. As well as supporting a uniform approach to func tions, it supports a uniform approach to data structures which underpins two new forms of polymorphism. Path polymorphism supports searches or queries along all paths through an arbitrary data structure. Pattern polymorphism supports the dynamic creation and evaluation of patterns, so that queries can be customised in reaction to new information about the structures to be encountered. In combination, these features provide a natural account of tasks such as programming with XML paths. As the variables used in matching can now be eliminated by reduction it is necessary to separate them from the binding variables used to con trol scope. Then standard techniques suffice to ensure that reduction
 Typed Pattern Calculi
 We present a typed pattern calculus with explicit pattern matching and explicit substitutions, where both the typing rules and the reduction rules are modeled on the same logical proof system, namely Gentzen sequent calculus for minimal logic. Our calculus is inspired by the CurryHoward Isomorphism, in the sense that types, both for patterns and terms, correspond to propositions, terms correspond to proofs, and term reduction corresponds to sequent proof normalization performed by cut elimination. The calculus enjoys subject reduction, confluence, preservation of strong normalization w.r.t a system with metalevel substitutions and strong normalization for welltyped terms. As a consequence, it can be seen as an implementation calculus for functional formalisms defined with metalevel operations for pattern matching and substitutions.
 Basic Pattern Matching Calculi
 The pattern matching calculus is a refinement of lambdacalculus that integrates mechanisms appropriate for finegrained modelling of nonstrict pattern matching. In comparison with the functional rewriting strategy that is usually employed to define the operational semantics of patternmatching in nonstrict 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. 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.
 Rewriting Logic
 Rewriting logic (RL) is a natural model of computation and an expressive semantic framework for concurrency, parallelism, communication and interaction. It can be used for specifying a wide range of systems and languages in various application fields. It also has good properties as a framework for representing logics. Several languages based on RL (ASF+SDF, CafeOBJ, ELAN, Maude, etc.) have been designed and implemented.