| 2022 | ICTAC | Local XOR Unification: Definitions, Algorithms and Application to Cryptography. | Hai Lin, Christopher Lynch |
| 2021 | CADE | Equational Theorem Proving Modulo. | Dohan Kim, Christopher Lynch |
| 2021 | FSCD | An RPO-Based Ordering Modulo Permutation Equations and Its Applications to Rewrite Systems. | Dohan Kim, Christopher Lynch |
| 2013 | CADE | Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2012 | CADE | Unification Modulo Synchronous Distributivity. | Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran, Michal Rusinowitch |
| 2012 | ESORICS | Effective Symbolic Protocol Analysis via Equational Irreducibility Conditions. | Serdar Erbatur, Santiago Escobar, Deepak Kapur, Zhiqiang Liu, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Sonia Santiago, Ralf Sasse |
| 2011 | CADE | Efficient General Unification for XOR with Homomorphism. | Zhiqiang Liu, Christopher Lynch |
| 2011 | PPDP | Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. | Santiago Escobar, Deepak Kapur, Christopher Lynch, Catherine Meadows, Jos Meseguer, Paliath Narendran, Ralf Sasse |
| 2011 | TABLEAUX | Unification in a Theory of Blind Signatures. | Serdar Erbatur, Christopher Lynch, Paliath Narendran |
| 2010 | CCS | Cap unification: application to protocol security modulo homomorphic encryption. | Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran, Michal Rusinowitch |
| 2009 | CADE | On Deciding Satisfiability by DPLL(G+ | Maria Paola Bonacina, Christopher Lynch, Leonardo Mendona de Moura |
| 2008 | ATVA | Interpolants for Linear Arithmetic in SMT. | Christopher Lynch, Yuefeng Tang |
| 2008 | ATVA | SMELS: Satisfiability Modulo Equality with Lazy Superposition. | Christopher Lynch, Duc-Khanh Tran |
| 2007 | CADE | Encoding First Order Proofs in SAT. | Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor |
| 2007 | CADE | Automatic Decidability and Combinability Revisited. | Christopher Lynch, Duc-Khanh Tran |
| 2007 | LPAR | Protocol Verification Via Rigid/Flexible Resolution. | Stphanie Delaune, Hai Lin, Christopher Lynch |
| 2004 | CSL | Unsound Theorem Proving. | Christopher Lynch |
| 2004 | ICICS | Sound Approximations to Diffie-Hellman Using Rewrite Rules. | Christopher Lynch, Catherine Meadows |
| 2003 | CADE | Schematic Saturation for Decision and Unification Problems. | Christopher Lynch |
| 2002 | CADE | Basic Syntactic Mutation. | Christopher Lynch, Barbara Morawska |
| 2002 | LICS | Automatic Decidability. | Christopher Lynch, Barbara Morawska |
| 2001 | CADE | Decidability and Complexity of Finitely Closable Linear Equational Theories. | Christopher Lynch, Barbara Morawska |
| 2001 | LPAR | Complexity of Linear Standard Theories. | Christopher Lynch, Barbara Morawska |
| 1998 | AISC | The Unification Problem for One Relation Thue Systems. | Christopher Lynch |
| 1998 | AISC | Basic Completion with E-cycle Simplification. | Christopher Lynch, Christelle Scharff |
| 1996 | AISC | PATCH Graphs: An Efficient Data Structure for Completion of Finitely Presented Groups. | Christopher Lynch, Polina Strogova |
| 1995 | LICS | Paramodulation without Duplication | Christopher Lynch |
| 1992 | CADE | Basic Paramodulation and Superposition. | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder |