An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality. - Wayne Snyder; Christopher Lynch (CTRS, 1990)

Goal Directed Strategies for Paramodulation. - Wayne Snyder; Christopher Lynch (RTA, 1991)

Basic Paramodulation and Superposition. - Leo Bachmair; Harald Ganzinger; Christopher Lynch; Wayne Snyder (CADE, 1992)

Paramodulation without Duplication - Christopher Lynch (LICS, 1995)

Redundancy Criteria for Constrained Completion. - Christopher Lynch; Wayne Snyder (Theor. Comput. Sci., 1995)

Basic Paramodulation - Leo Bachmair; Harald Ganzinger; Christopher Lynch; Wayne Snyder (Inf. Comput., 1995)

PATCH Graphs: An Efficient Data Structure for Completion of Finitely Presented Groups. - Christopher Lynch; Polina Strogova (AISMC, 1996)

Fine-Grained Concurrent Completion. - Claude Kirchner; Christopher Lynch; Christelle Scharff (RTA, 1996)

Goal-Directed Completion Using SOUR Graphs. - Christopher Lynch (RTA, 1997)

Oriented Equational Logic Programming is Complete. - Christopher Lynch (J. Symb. Comput., 1997)

The Unification Problem for One Relation Thue Systems. - Christopher Lynch (AISC, 1998)

SOUR graphs for efficient completion. - Christopher Lynch; Polina Strogova (Discret. Math. Theor. Comput. Sci., 1998)

Local Simplification. - Christopher Lynch (Inf. Comput., 1998)

Basic Completion with E-cycle Simplification. - Christopher Lynch; Christelle Scharff (Fundam. Informaticae, 1999)

Decidability and Complexity of Finitely Closable Linear Equational Theories. - Christopher Lynch; Barbara Morawska 001 (IJCAR, 2001)

Complexity of Linear Standard Theories. - Christopher Lynch; Barbara Morawska 001 (LPAR, 2001)

Goal-Directed E-Unification. - Christopher Lynch; Barbara Morawska 001 (RTA, 2001)

Basic Syntactic Mutation. - Christopher Lynch; Barbara Morawska 001 (CADE, 2002)

Automatic Decidability. - Christopher Lynch; Barbara Morawska 001 (LICS, 2002)

Schematic Saturation for Decision and Unification Problems. - Christopher Lynch (CADE, 2003)

Unsound Theorem Proving. - Christopher Lynch (CSL, 2004)

Sound Approximations to Diffie-Hellman Using Rewrite Rules. - Christopher Lynch; Catherine Meadows 001 (ICICS, 2004)

On the Relative Soundness of the Free Algebra Model for Public Key Encryption. - Christopher Lynch; Catherine Meadows 001 (ARSPA@IJCAR, 2004)

Embedded Type-2 FLC for Real-Time Speed Control of Marine and Traction Diesel Engines. - Christopher Lynch; Hani Hagras; Victor Callaghan (FUZZ-IEEE, 2005)

Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories. - Christopher Lynch; Barbara Morawska 001 (RTA, 2005)

Using Uncertainty Bounds in the Design of an Embedded Real-Time Type-2 Neuro-Fuzzy Speed Controller for Marine Diesel Engines. - Christopher Lynch; Hani Hagras; Victor Callaghan (FUZZ-IEEE, 2006)

Encoding First Order Proofs in SAT. - Todd Deshane; Wenjin Hu; Patty Jablonski; Hai Lin 005; Christopher Lynch; Ralph Eric McGregor (CADE, 2007)

Automatic Decidability and Combinability Revisited. - Christopher Lynch; Duc-Khanh Tran (CADE, 2007)

Parallel Type-2 Fuzzy Logic Co-Processors for Engine Management. - Christopher Lynch; Hani Hagras; Victor Callaghan (FUZZ-IEEE, 2007)

Protocol Verification Via Rigid/Flexible Resolution. - Stéphanie Delaune; Hai Lin 005; Christopher Lynch (LPAR, 2007)

Encoding First Order Proofs in SMT. - Jeremy Bongio; Cyrus Katrak; Hai Lin 005; Christopher Lynch; Ralph Eric McGregor (SMT@CAV, 2007)

Interpolants for Linear Arithmetic in SMT. - Christopher Lynch; Yuefeng Tang (ATVA, 2008)

SMELS: Satisfiability Modulo Equality with Lazy Superposition. - Christopher Lynch; Duc-Khanh Tran (ATVA, 2008)

Unification modulo Homomorphic Encryption is Decidable. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (UNIF, 2008)

Rewriting Interpolants. - Christopher Lynch; Yuefeng Tang (FICS, 2008)

On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (CADE, 2009)

Combining Instance Generation and Resolution. - Christopher Lynch; Ralph Eric McGregor (FroCoS, 2009)

Cap unification: application to protocol security modulo homomorphic encryption. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (AsiaCCS, 2010)

Frontmatter (Titlepage, Table of Contents, Author List, PC List, Reviewer List). - Christopher Lynch (RTA, 2010)

Preface. - Christopher Lynch (RTA, 2010)

Efficient General Unification for XOR with Homomorphism. - Zhiqiang Liu; Christopher Lynch (CADE, 2011)

Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. - Santiago Escobar 001; Deepak Kapur; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (PPDP, 2011)

Unification in a Theory of Blind Signatures. - Serdar Erbatur; Christopher Lynch; Paliath Narendran (TABLEAUX (Workshops, Tutorials, and Short Papers), 2011)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Ralf Sasse (UNIF, 2011)

Invited talk: Unification in Cryptographic Protocol Analysis. - Christopher Lynch (UNIF, 2011)

Automatic decidability and combinability. - Christopher Lynch; Silvio Ranise; Christophe Ringeissen; Duc-Khanh Tran (Inf. Comput., 2011)

On Deciding Satisfiability by Theorem Proving with Speculative Inferences. - Maria Paola Bonacina; Christopher Lynch; Leonardo Mendonça de Moura (J. Autom. Reason., 2011)

Unification Modulo Synchronous Distributivity. - Siva Anantharaman; Serdar Erbatur; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (IJCAR, 2012)

Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (ESORICS, 2012)

Unification Modulo Homomorphic Encryption. - Siva Anantharaman; Hai Lin 005; Christopher Lynch; Paliath Narendran; Michaël Rusinowitch (J. Autom. Reason., 2012)

Constructing Bachmair-Ganzinger Models. - Christopher Lynch (Programming Logics, 2013)

Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. - Serdar Erbatur; Santiago Escobar 001; Deepak Kapur; Zhiqiang Liu; Christopher Lynch; Catherine Meadows 001; José Meseguer 001; Paliath Narendran; Sonia Santiago; Ralf Sasse (CADE, 2013)

On Forward Closure and the Finite Variant Property. - Christopher Bouchard; Kimberly A. Gero; Christopher Lynch; Paliath Narendran (FroCos, 2013)

SMELS: Satisfiability Modulo Equality with Lazy Superposition. - Christopher Lynch; Quang-Trung Ta; Duc-Khanh Tran (J. Autom. Reason., 2013)

Efficient general AGH-unification. - Zhiqiang Liu; Christopher Lynch (Inf. Comput., 2014)

Finding Intruder Knowledge with Cap-Matching. - Erin Hanna; Christopher Lynch; David Jaz Myers; Corey Richardson (Foundations of Security, Protocols, and Equational Reasoning, 2019)

Reviving Basic Narrowing Modulo. - Dohan Kim 001; Christopher Lynch; Paliath Narendran (FroCos, 2019)

On Asymmetric Unification for the Theory of XOR with a Homomorphism. - Christopher Lynch; Andrew M. Marshall; Catherine Meadows 001; Paliath Narendran; Veena Ravishankar (FroCos, 2019)

Local XOR Unification: Definitions, Algorithms and Application to Cryptography. - Hai Lin 005; Christopher Lynch (IACR Cryptol. ePrint Arch., 2020)

Bounded ACh unification. - Ajay Kumar Eeralla; Christopher Lynch (Math. Struct. Comput. Sci., 2020)

Equational Theorem Proving Modulo. - Dohan Kim 001; Christopher Lynch (CADE, 2021)

Formal Analysis of Symbolic Authenticity. - Hai Lin 005; Christopher Lynch (FroCoS, 2021)

Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems. - Hai Lin 005; Christopher Lynch; Andrew M. Marshall; Catherine A. Meadows; Paliath Narendran; Veena Ravishankar; Brandon Rozek (FroCoS, 2021)

An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. - Dohan Kim 001; Christopher Lynch (FSCD, 2021)

Congruence Closure Modulo Permutation Equations. - Dohan Kim 001; Christopher Lynch (SCSS, 2021)

CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms. - Dalton Chichester; Wei Du; Raymond Kauffman; Hai Lin 005; Christopher Lynch; Andrew M. Marshall; Catherine A. Meadows; Paliath Narendran; Veena Ravishankar; Luis Rovira; Brandon Rozek (GandALF, 2022)

Complete Trigger Selection in Satisfiability Modulo First-Order Theories. - Christopher Lynch; Stephen Miner (SMT, 2023)