@article(ArSh1999b,
 author       = "Arvind and X. Shen",
 year         = "1999",
 title        = "{Using Term Rewriting Systems to Design and Verify Processors}",
 journal      = "IEEE Micro",
 volume       = "19",
 number       = "3",
 pages        = "36--46",
 doi          = "10.1109/40.768501",
)
@article(ARLaJaHa2006,
 author       = "M. Ayala-Rinc\'on and C. Llanos and R. P. Jacobi and R. W. Hartenstein",
 year         = "2006",
 title        = "{Prototyping Time and Space Efficient Computations of Algebraic Operations over Dynamically Reconfigurable Systems Modeled by Rewriting-Logic}",
 journal      = "ACM Trans. Design Autom. Electr. Syst. ",
 volume       = "11",
 number       = "2",
 pages        = "251--281",
 doi          = "10.1145/1142155.1142156",
)
@book(BaNi98,
 author       = "F. Baader and T. Nipkow",
 year         = "1998",
 title        = "{Term Rewriting and {\em All That}}",
 publisher    = "Cambridge University Press",
)
@book(Te2003,
 editor       = "M. Bezem and J.W. Klop and R. de Vrijer",
 year         = "2003",
 title        = "{Term Rewriting Systems by TeReSe}",
 series       = "Cambridge Tracts in Theoretical Computer Science",
 volume       = "55",
 publisher    = "Cambridge University Press",
)
@article(GaAR2008c,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2008",
 title        = "{A Formalization of Newman's and Yokouchi Lemmas in a Higher-Order Language}",
 journal      = "Journal of Formalized Reasoning",
 volume       = "1",
 number       = "1",
 pages        = "39--50",
)
@inproceedings(GaAR2008b,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2009",
 title        = "{A PVS \emph {Theory} for Term Rewriting Systems}",
 booktitle    = "Proceedings of the Third Workshop on Logical and Semantic Frameworks, with Applications - LSFA 2008",
 series       = "Electronic Notes in Theoretical Computer Science",
 volume       = "247",
 pages        = "67--83",
 doi          = "10.1016/j.entcs.2009.07.049",
)
@article(GaAR2010,
 author       = "A. L. Galdino and M. Ayala-Rinc{\'o}n",
 year         = "2010",
 title        = "{A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem}",
 journal      = "J. of Automated Reasoning",
 volume       = "45",
 number       = "3",
 pages        = "301--325",
 doi          = "10.1007/s10817-010-9165-2",
)
@article(Hu80,
 author       = "G. Huet",
 year         = "1980",
 title        = "{Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems}",
 journal      = "Journal of the Association for Computing Machinery",
 volume       = "27",
 number       = "4",
 pages        = "797--821",
 doi          = "10.1145/322217.322230",
)
@inbook(KnBe70,
 author       = "D. E. Knuth and P. B. Bendix",
 year         = "1970",
 title        = "{Computational Problems in Abstract Algebra}",
 chapter      = "Simple Words Problems in Universal Algebras",
 pages        = "263--297",
 publisher    = "J. Leech, ed. Pergamon Press, Oxford, U. K.",
)
@inproceedings(MBARH2005,
 author       = "C. Morra and J. Becker and M. Ayala-Rinc\'on and R. W. Hartenstein",
 year         = "2005",
 title        = "{FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations}",
 booktitle    = "15th Int. Conference on Field Programmable Logic and Applications - FPL 2005",
 publisher    = "IEEE CS",
 pages        = "25--30",
 doi          = "10.1109/FPL.2005.1515694",
)
@inproceedings(MorraBCB08,
 author       = "C. Morra and J. Bispo and J.M.P. Cardoso and J. Becker",
 year         = "2008",
 title        = "Combining Rewriting-Logic, Architecture Generation, and Simulation to Exploit Coarse-Grained Reconfigurable Architectures",
 editor       = "Kenneth L. Pocek and Duncan A. Buell",
 booktitle    = "FCCM",
 publisher    = "IEEE Computer Society",
 pages        = "320--321",
 doi          = "10.1109/FCCM.2008.37",
)
@article(Ro1973,
 author       = "B. K. Rosen",
 year         = "1973",
 title        = "Tree-Manipulating Systems and Church-Rosser Theorems",
 journal      = "J. of the ACM",
 volume       = "20",
 number       = "1",
 pages        = "160--187",
 doi          = "10.1145/321738.321750",
)
@inproceedings(Th2012,
 author       = "R. Thiemann",
 year         = "2012",
 title        = "Certification of Confluence Proofs using CeTA",
 booktitle    = "First International Workshop on Confluence (IWC 2012)",
 pages        = "45",
)
@misc(NASAPVSLib,
 author       = "Theory {\tt trs}",
 year         = "consulted January 2013",
 title        = "{Available in the NASA LaRC PVS library, \relax \fontsize {9}{11}\selectfont \abovedisplayskip 8\p@ plus2\p@ minus4\p@ \abovedisplayshortskip \z@ plus\p@ \belowdisplayshortskip 4\p@ plus2\p@ minus2\p@ \def \leftmargin \leftmargini \parsep 2.5\p@ plus1.5\p@ minus\p@ \topsep 5\p@ plus2\p@ minus5\p@ \itemsep 2.5\p@ plus1.5\p@ minus\p@ {\leftmargin \leftmargini \topsep 4\p@ plus2\p@ minus2\p@ \parsep 2\p@ plus\p@ minus\p@ \itemsep \parsep }\belowdisplayskip \abovedisplayskip {\tt http://shemesh.larc.nasa.gov/fm/ftp/larc/} {\tt PVS-library/pvslib.html}}",
)