BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Japan
1 × Spain
1 × The Netherlands
1 × United Kingdom
2 × Canada
2 × Germany
2 × Italy
2 × Poland
3 × Denmark
5 × USA
Collaborated with:
B.Morawska ∅ W.Snyder Z.Liu D.Tran P.Narendran H.Lin R.E.McGregor M.P.Bonacina L.M.d.Moura C.Kirchner C.Scharff S.Erbatur L.Bachmair H.Ganzinger S.Escobar D.Kapur C.Meadows J.Meseguer R.Sasse S.Anantharaman M.Rusinowitch J.Bongio C.Katrak T.Deshane W.Hu P.Jablonski S.Santiago
Talks about:
unif (7) decid (4) paramodul (3) complet (3) direct (3) basic (3) goal (3) homomorph (2) protocol (2) unsound (2)

Person: Christopher Lynch

DBLP DBLP: Lynch:Christopher

Facilitated 1 volumes:

RTA 2010Ed

Contributed to:

CADE 20132013
IJCAR 20122012
CADE 20112011
PPDP 20112011
CADE 20092009
CADE 20072007
SMT 20072008
RTA 20052005
CSL 20042004
CADE 20032003
CADE 20022002
LICS 20022002
IJCAR 20012001
RTA 20012001
RTA 19971997
RTA 19961996
LICS 19951995
RTA 19931993
CADE 19921992
RTA 19911991

Wrote 21 papers:

CADE-2013-ErbaturEKLLMMNSS #analysis #encryption #paradigm #protocol #symmetry #unification
Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis (SE, SE, DK, ZL, CL, CM, JM, PN, SS, RS), pp. 231–248.
IJCAR-2012-AnantharamanELNR #unification
Unification Modulo Synchronous Distributivity (SA, SE, CL, PN, MR), pp. 14–29.
CADE-2011-LiuL #morphism #performance #unification
Efficient General Unification for XOR with Homomorphism (ZL, CL), pp. 407–421.
PPDP-2011-EscobarKLMMNS #analysis #encryption #protocol #unification #using
Protocol analysis in Maude-NPA using unification modulo homomorphic encryption (SE, DK, CL, CM, JM, PN, RS), pp. 65–76.
CADE-2009-BonacinaLM #on the #proving #satisfiability #theorem proving
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADE-2007-DeshaneHJLLM #encoding #first-order #proving #satisfiability
Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CADE-2007-LynchT #automation #decidability #revisited
Automatic Decidability and Combinability Revisited (CL, DKT), pp. 328–344.
SMT-2007-BongioKLLM08 #encoding #first-order #proving #smt
Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.
RTA-2005-LynchM #equation #performance
Faster Basic Syntactic Mutation with Sorts for Some Separable Equational Theories (CL, BM), pp. 90–104.
CSL-2004-Lynch #proving #theorem proving
Unsound Theorem Proving (CL), pp. 473–487.
CADE-2003-Lynch #problem #unification
Schematic Saturation for Decision and Unification Problems (CL), pp. 427–441.
CADE-2002-LynchM
Basic Syntactic Mutation (CL, BM), pp. 471–485.
LICS-2002-LynchM #automation #decidability
Automatic Decidability (CL, BM), p. 7–?.
IJCAR-2001-LynchM #complexity #decidability #equation #linear
Decidability and Complexity of Finitely Closable Linear Equational Theories (CL, BM), pp. 499–513.
RTA-2001-LynchM
Goal-Directed E-Unification (CL, BM), pp. 231–245.
RTA-1997-Lynch #graph #using
Goal-Directed Completion Using SOUR Graphs (CL), pp. 8–22.
RTA-1996-KirchnerLS #concurrent #fine-grained
Fine-Grained Concurrent Completion (CK, CL, CS), pp. 3–17.
LICS-1995-Lynch
Paramodulation without Duplication (CL), pp. 167–177.
RTA-1993-LynchS
Redundancy Criteria for Constrained Completion (CL, WS), pp. 2–16.
CADE-1992-BachmairGLS
Basic Paramodulation and Superposition (LB, HG, CL, WS), pp. 462–476.
RTA-1991-SnyderL
Goal Directed Strategies for Paramodulation (WS, CL), pp. 150–161.
Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.