@Unpublished{Mul+Wel:TAS-2000,
  author =       {Robert Muller} # and # Wells,
  title =        {Two Applications of Standardization and Evaluation
                  in {C}ombinatory {R}eduction {S}ystems},
  note =         {Submitted for publication},
  year =         2000,
  abstract =     {This paper presents two worked applications of a
                  general framework that can be used to support
                  reasoning about the operational equality relation
                  defined by a programming language semantics.  The
                  framework, based on Combinatory Reduction Systems,
                  facilitates the proof of standardization theorems
                  for programming calculi.  The importance of
                  standardization theorems to programming language
                  semantics was shown by Plotkin: standardization
                  together with confluence guarantee that two terms
                  equated in the calculus are semantically equal.  The
                  framework is applied to the
                  $\lambda_{\mathrm{v}}$-calculus and to an untyped
                  version of the
                  $\lambda^{\mathrm{CIL}}$-calculus.  The latter is a
                  basis for an intermediate language being used in a
                  compiler.},
}