| 004117 (1987) |
J. Goguen ; C. Kirchner ; H. Kirchner ; A. Mégrelis ; J. Meseguer ; T. Winkler | An Introduction to OBJ3 |
| 003668 (1992) |
J.-P. Jouannaud ; C. Kirchner ; H. Kirchner ; A. Mégrelis | Programming with Equalities, Subsorts, Overloading, and Parametrization in OBJ |
| 003F33 (1988) |
J.-P. Jouannaud ; C. Kirchner ; H. Kirchner ; A. Mégrelis | OBJ : Programming with Equalities, Subsorts, Overloading and Parameterization |
| 002A44 (1995) |
C. Kirchner ; H. Kirchner ; M. Vittek | ELAN User Manual |
| 002B08 (1995) |
C. Kirchner ; H. Kirchner ; M. Vittek | Designing Constraint Logic Programming Languages using Computational Systems |
| 002D30 (1995) |
C. Hintermeier ; C. Kirchner ; H. Kirchner | Sort Inheritance for Order-Sorted Equational Presentations |
| 003006 (1994) |
C. Hintermeier ; C. Kirchner ; H. Kirchner | Dynamically-Typed Computations for Order-Sorted Equational Presentations - Extended Abstract |
| 003307 (1993) |
C. Kirchner ; H. Kirchner ; M. Vittek | Designing Constraint Logic Programming Languages using Computational Systems |
| 003377 (1993) |
C. Hintermeier ; C. Kirchner ; H. Kirchner | Dynamically-Typed Computations for Order-Sorted Equational Presentations |
| 003379 (1993) |
C. Kirchner ; H. Kirchner ; M. Vittek | Implementing Computational Systems with Constraints |
| 003672 (1992) |
C. Hintermeier ; C. Kirchner ; H. Kirchner | Strict Matchings and Unifications in {G}-algebras |
| 003F77 (1988) |
C. Kirchner ; H. Kirchner ; J. Meseguer | Operational semantics of OBJ3 - Extended abstract - |
| 004042 (1987) |
C. Kirchner ; H. Kirchner ; A. Mégrelis | OBJ for OBJ |
| 004108 (1987) |
J. Goguen ; C. Kirchner ; J. Meseguer | Concurrent Term Rewriting as a Model of Computation |
| 004109 (1987) |
J. Goguen ; C. Kirchner ; J. Meseguer ; T. Winkler | OBJ as a language for concurrent programming |
| 004164 (1986) |
J. Goguen ; C. Kirchner ; S. Leinwand ; J. Meseguer ; T. Winkler | Progress report on the rewrite rule machine |
| 002B83 (1995) |
C. Hintermeier ; H. Kirchner ; P.-D. Mosses | Combining Algebraic and Set-Theoretic Specifications |
| 002D71 (1995) |
C. Hintermeier ; H. Kirchner ; P.-D. Mosses | {R}^n- and {G}^n-logics |
| 003944 (1991) |
J.-P. Jouannaud ; C. Kirchner | Solving Equations in Abstract Algebras : A Rule-based Survey of Unification |
| 003977 (1991) |
C. Kirchner ; H. Kirchner | Order-Sorted Rewriting and Completion in G-Algebra - Extended Abstract |
| 003A34 (1991) |
M. Hermann ; C. Kirchner ; H. Kirchner | Implementations of Term Rewriting Systems |
| 003A45 (1991) |
C. Kirchner ; H. Kirchner | Order-Sorted Computations in G-Algebra |
| 003B97 (1990) |
C. Kirchner ; H. Kirchner ; M. Rusinowitch | Deduction with Symbolic Constraints |
| 003C36 (1990) |
I. Gnaedig ; C. Kirchner ; H. Kirchner | Equational Completion in Orded-sorted Algebras |
| 003D68 (1989) |
C. Kirchner ; H. Kirchner | Constrained Equational Reasoning |
| 003D94 (1989) |
C. Kirchner ; H. Kirchner | Rewriting : Theory and Applications |
| 003F54 (1988) |
I. Gnaedig ; C. Kirchner ; H. Kirchner | Equational completion in order-sorted algebras - Extended abstract - |
| 004089 (1987) |
C. Kirchner ; H. Kirchner | REVEUR-3 : the implementation of a general completion procedure parameterized by built-in theories and strategies |
| 004218 (1986) |
P. Réty ; C. Kirchner ; H. Kirchner ; Pierre Lescanne [France] | An algorithm for unification based on narrowing |
| 004278 (1986) |
J.-P. Jouannaud ; H. Kirchner | Completion of a set of rules modulo a set of equations |
| 004337 (1985) |
P. Réty ; C. Kirchner ; H. Kirchner ; Pierre Lescanne [France] | NARROWER : a new algorithm for unification and its application to logic programming |
| 004345 (1985) |
K. Futatsugi ; J. A. Goguen ; J.-P. Jouannaud ; J. Meseguer | Principles of OBJ2 |
| 004357 (1985) |
C. Kirchner ; H. Kirchner | Implementation of a general completion procedure parameterized by built-in theories and strategies |
| 004397 (1985) |
J. A. Goguen ; J.-P. Jouannaud ; J. Meseguer | Operational Semantics for Order-Sorted Algebra |
| 004466 (1984) |
J.-P. Jouannaud ; H. Kirchner | Completion of a set of rules modulo a set of equations : full paper |
| 004524 (1984) |
H. Kirchner ; J.-P. Jouannaud | Completion of a set of rules modulo a set of equations |
| 002A15 (1995) |
C. Kirchner | Selected Papers of RTA-93 |
| 002A46 (1995) |
C. Hintermeier | Déduction avec sortes ordonnées et égalités |
| 002B24 (1995) |
H. Kirchner ; P.-E. Moreau | Prototyping Completion with Constraints using Computational Systems |
| 002C37 (1995) |
G. Dowek ; T. Hardin ; C. Kirchner | Higher-Order Unification via Explicit Substitutions - Extended Abstract |
| 002D37 (1995) |
H. Kirchner | Some Extensions of Rewriting |
| 002F28 (1994) |
H. Kirchner ; C. Ringeissen | Constraint Solving by Narrowing in Combined Algebraic Domains |
| 002F44 (1994) |
H. Kirchner ; P.-E. Moreau | Prototyping Completion with Constraints using Computational Systems - Extended version |
| 002F45 (1994) |
H. Kirchner ; C. Ringeissen | Combining Symbolic Constraint Solvers on Algebraic Domains |
| 002F50 (1994) |
C. Hintermeier | How to Transform Canonical Decreasing CTRSs into Equivalent Canonical TRSs |
| 003037 (1994) |
G. Dowek ; T. Hardin ; C. Kirchner | High-Order Unification via Explicit Substitutions |
| 003046 (1994) |
H. Kirchner | On the Use of Constraints in Automated Deduction |
| 003074 (1994) |
M. Vittek | ELAN : Un cadre logique pour le prototypage de langages de programmation avec contraintes |
| 003209 (1993) |
F. Klay ; E. Domenjoud ; C. Kirchner | Vérification sémantique de spécifications métallurgiques |
| 003458 (1993) |
D. Galmiche ; H. Kirchner | Les langages fonctionnels et logiques |
| 003534 (1992) |
A. Mégrelis | Calculer = transformer une forme |
| 003586 (1992) |
A. Mégrelis | Partial Algebra + Order-sorted Algebra = Galactic Algebra |
| 003594 (1992) |
H. Kirchner ; Ch. Ringeissen | A Constraint Solver in Finite Algebras and its Combination with Unification Algorithms |
| 003632 (1992) |
M. Vittek | A Combinatory Logic Rewriting Relation which Supports Narrowing |
| 003640 (1992) |
M. Adi ; C. Kirchner | AC-Unification Race : The System Solving Approach, Implementation and Benchmarks |
| 003698 (1992) |
A. Mégrelis | An Introduction to Galactic Algebra |
| 003724 (1992) |
J. Hsiang ; H. Kirchner ; Pierre Lescanne [France] ; M. Rusinowitch | The Term Rewriting Approach to Automated Theorem Proving |
| 003735 (1992) |
C. Kirchner ; P. Viry | Implementing Parallel Rewriting |
| 003887 (1991) |
H. Kirchner ; Ch. Ringeissen | Combining Unification Problems with Constraint Solving in Finite Algebras |
| 003958 (1991) |
N. Doggaz ; C. Kirchner | Completion for Unification |
| 003A08 (1991) |
H. Kirchner | Proofs in Parameterized Specifications - Extended Version |
| 003A49 (1991) |
A. Mégrelis | '1/0' is not nonsense |
| 003B03 (1990) |
H. Kirchner ; M. Hermann | Meta-rules Synthesis from Crossed Rewrite Systems |
| 003B04 (1990) |
A. Mégrelis | Modéliser un logiciel à l'aide de VDM : une expérience |
| 003B24 (1990) |
A. Mégrelis | Algèbre galactique - Un procédé de calcul formel, relatif aux semi-fonctions, à l'inclusion et à l'égalité |
| 003B44 (1990) |
M. Adi ; C. Kirchner | AC-Unification Race : the System Solving Approach and its Implementation |
| 003B83 (1990) |
A. Mégrelis | Partial Algebra +order-sorted Algebra = G Algebra |
| 003C41 (1990) |
C. Kirchner ; P. Viry | Implementing Parallel Rewriting |
| 003D55 (1989) |
A. Mégrelis | A Logic of Semi-functions, Inclusion and Equality. The setting |
| 003D67 (1989) |
N. Doggaz ; C. Kirchner | Completion for Unification |
| 003D73 (1989) |
H. Kirchner | Schematization of Infinite Sets of Rewrite Rules Generated by Divergent Completion Processes |
| 004036 (1987) |
C. Kirchner | From unification in combination of equational theories to a new AC-unification algorithm |
| 004078 (1987) |
H. Kirchner | Schematization of infinite sets of rewrite rules. Application to the divergence of completion processes - Extended version - |
| 004087 (1987) |
H. Kirchner | Schematization of infinite sets of rewrite rules. Application to the divergence of completion processes |
| 004098 (1987) |
C. Kirchner | Methods and tools for equational unification |
| 004144 (1987) |
C. Kirchner ; Pierre Lescanne [France] | Solving disequations |
| 004182 (1986) |
J.-P. Jouannaud ; Pierre Lescanne [France] ; J. Mzali ; J.-L. Rémy | Présentation de l'équipe de recherche EURECA |
| 004188 (1986) |
J.-P. Jouannaud ; Pierre Lescanne [France] | La réécriture |
| 004205 (1986) |
J.-P. Jouannaud ; B. Waldmann | Reductive conditional rewrite rules |
| 004234 (1986) |
C. Kirchner | Computing unification algorithms |
| 004241 (1986) |
J.-P. Jouannaud ; E. Kounalis | Proofs by induction in equational theories without constructors |
| 004265 (1986) |
J.-P. Jouannaud ; B. Waldmann | Reductive conditional term rewriting systems |
| 004292 (1985) |
C. Kirchner | Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationnelles |
| 004301 (1985) |
C. Kirchner | Etude comparative des formateurs MINT, GROFF, NROFF associés aux éditeurs EMACS, VI, EMIN |
| 004305 (1985) |
H. Kirchner | Preuves par complétion dans les variétés d'algèbres |
| 004471 (1984) |
C. Kirchner | A new equational unification method : a generalisation of MARTELLI--MONTANARI'S algorithm |
| 004475 (1984) |
H. Kirchner | A general inductive completion algorithm and application to abstract data types |
| 004481 (1984) |
C. Kirchner | Standardization of equational unification : abstract and examples |
| 004516 (1984) |
M. Munoz ; J.-P. Jouannaud | Termination of a set of rules modulo a set of equations |
