Person: Claude Kirchner

DBLP: Kirchner:Claude

Facilitated 5 volumes:

Ed

Ed

Ed

Ed

Ed

Contributed to:

2012

2008

2007

2007

2007

2006

2005

2005

2007

2003

2003

2003

2002

2002

2001

2001

2000

1999

1998

2001

1998

1997

1997

1997

1996

1996

1996

1996

2002

1995

1994

1990

1990

1990

1988

1988

1987

1986

1985

1984

1983

Wrote 43 papers:

RTA-2012-Kirchner #calculus #logic

Rho-Calculi for Computation and Logic (CK), pp. 2–4.

LATA-2008-KirchnerKM #pattern matching

Anti-pattern Matching Modulo (CK, RK, PEM), pp. 275–286.

ESOP-2007-KirchnerKM #pattern matching

Anti-pattern Matching (CK, RK, PEM), pp. 110–124.

FoSSaCS-2007-BertolissiK #calculus #combinator #reduction

The Rewriting Calculus as a Combinatory Reduction System (CB, CK), pp. 78–92.

LICS-2007-BraunerHK #deduction

Principles of Superdeduction (PB, CH, CK), pp. 41–50.

FoSSaCS-2006-BlanquiKR #confluence #on the #λ-calculus

On the Confluence of λ-Calculus with Conditional Rewriting (FB, CK, CR), pp. 382–397.

PPDP-2005-KirchnerMR #pattern matching #validation

Formal validation of pattern matching code (CK, PEM, AR), pp. 187–197.

WRLA-2004-CirsteaFK05 #calculus #constraints

A rho-Calculus of Explicit Constraint Application (HC, GF, CK), pp. 51–67.

WRLA-J-2004-CirsteaFK07 #calculus #constraints

A rho-calculus of explicit constraint application (HC, GF, CK), pp. 37–72.

CADE-2003-DeplagneKKN #equation #induction #proving #theorem

Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.

LICS-2003-DershowitzK

Abstract Saturation-Based Inference (ND, CK), pp. 65–74.

POPL-2003-BartheCKL #type system

Pure patterns type systems (GB, HC, CK, LL), pp. 250–261.

RTA-2002-BournezK #probability

Probabilistic Rewrite Strategies. Applications to ELAN (OB, CK), pp. 252–266.

RTA-2002-FaureK #calculus #exception

Exceptions in the Rewriting Calculus (GF, CK), pp. 66–82.

WRLA-2002-CirsteaKL #calculus

Rewriting Calculus with(out) Types (HC, CK, LL), pp. 3–19.

FoSSaCS-2001-CirsteaKL

The Rho Cube (HC, CK, LL), pp. 168–183.

RTA-2001-CirsteaKL

Matching Power (HC, CK, LL), pp. 77–92.

WRLA-2000-CirsteaK #calculus

The simply typed rewriting calculus (HC, CK), pp. 24–42.

RTA-1999-DowekHK #first-order #higher-order #logic #named

HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.

FLOPS-1998-BorovanskyKK #functional #semantics

A Functional View of Rewriting and Strategies for a Semantics of ELAN (PB, CK, HK), pp. 143–166.

FLOPS-J1-1998-BorovanskyKKR01 #functional #semantics

Rewriting with Strategies in ELAN: A Functional Semantics (PB, CK, HK, CR), pp. 69–95.

WRLA-1998-BorovanskyKKMR #overview

An overview of ELAN (PB, CK, HK, PEM, CR), pp. 55–70.

ALP-1997-KirchnerR #equation #higher-order #unification

Higher-Order Equational Unification via Explicit Substitutions (CK, CR), pp. 61–75.

ASF+SDF-1997-BorovanskyKK #logic #specification

Rewriting as a unified specification tool for logic and control: the ELAN language (PB, CK, HK), p. 3.

ICLP-1997-AjiliK #composition #constraints #framework #unification

A Modular Framework for the Combination of Unification and Built-In Constraints (FA, CK), pp. 331–345.

ALP-1996-AlouiniK #concurrent #implementation #towards

Toward the Concurrent Implementation of Computational Systems (IA, CK), pp. 1–31.

JICSLP-1996-DowekHKP #higher-order #unification

Unification via Explicit Substitutions: The Case of Higher-Order Patterns (GD, TH, CK, FP), pp. 259–273.

RTA-1996-KirchnerLS #concurrent #fine-grained

Fine-Grained Concurrent Completion (CK, CL, CS), pp. 3–17.

RWLW-1996-BorovanskyKK

Controlling rewriting by rewriting (PB, CK, HK), pp. 169–189.

RWLW-1996-BorovanskyKKMV #framework #logic #named

ELAN: A logical framework based on computational systems (PB, CK, HK, PEM, MV), pp. 35–50.

WRLA-J-1996-BorovanskyKKM02 #logic #perspective

ELAN from a rewriting logic point of view (PB, CK, HK, PEM), pp. 155–185.

LICS-1995-DowekHK #higher-order #unification

Higher-Order Unification via Explicit Substitutions (GD, TH, CK), pp. 366–374.

ICALP-1994-HintermeierKK #dynamic typing #equation #order

Dynamically-Typed Computations for Order-Sorted Equational Presentations (CH, CK, HK), pp. 450–461.

CADE-1990-Kirchner #equation #tutorial #unification

Tutorial on Equational Unification (CK), p. 682.

LICS-1990-KirchnerK #unification

Syntactic Theories and Unification (CK, FK), pp. 270–277.

PLILP-1990-KirchnerV #implementation #parallel

Implementing Parallel Rewriting (CK, PV), pp. 1–15.

ALP-1988-JouannaudKKM #named #programming

OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization (JPJ, CK, HK, AM), pp. 41–52.

ICALP-1988-KirchnerKM #semantics

Operational Semantics of OBJ-3 (CK, HK, JM), pp. 287–301.

LICS-1987-KirchnerL #equation

Solving Disequations (CK, PL), pp. 347–352.

LICS-1986-Kirchner #algorithm #unification

Computing Unification Algorithms (CK), pp. 206–216.

RTA-1985-RetyKKL #algorithm #logic programming #named #unification

NARROWER: A New Algorithm for Unification and Its Application to Logic Programming (PR, CK, HK, PL), pp. 141–157.

CADE-1984-Kirchner #algorithm #equation #unification

A New Equational Unification Method: A Generalization of Martelli-Montanari’s Algorithm (CK), pp. 224–247.

ICALP-1983-JouannaudKK #algorithm #equation #incremental #unification

Incremental Construction of Unification Algorithms in Equational Theories (JPJ, CK, HK), pp. 361–373.