| 00DB01 (1991) |
N. Doggaz ; C. Kirchner | Completion for unification |
| 006180 (2005) |
Clara Bertolissi [France] | The Graph Rewriting Calculus: Confluence and Expressiveness |
| 006222 (2005) |
Alessandro Armando [Italie] ; Maria Paola Bonacina [Italie] ; Silvio Ranise [France] ; Stephan Schulz [Italie] | On a Rewriting Approach to Satisfiability Procedures: Extension, Combination of Theories and an Experimental Appraisal |
| 007A08 (2003) |
Eric Deplagne ; Claude Kirchner ; Hélène Kirchner [France] ; Quang Huy Nguyen | Proof Search and Proof Check for Equational and Inductive Theorems |
| 00DB00 (1991) |
M. Hermann ; C. Kirchner ; H. Kirchner | Implementations of term rewriting systems |
| 003171 (2010) |
Guillaume Burel [France] ; Claude Kirchner [France] | Regaining cut admissibility in deduction modulo using abstract completion |
| 005613 (2006) |
Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Deciding extensions of the theory of arrays by integrating decision procedures and instantiation strategies |
| 005614 (2006) |
Maria Paola Bonacina [Italie] ; Silvio Ghilardi [Italie] ; Enrica Nicolini [Italie] ; Silvio Ranise [Italie, France] ; Daniele Zucchelli [Italie, France] | Decidability and undecidability results for nelson-oppen and rewrite-based decision procedures |
| 006271 (2005) |
Frédéric Blanqui [France] | Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations |
| 006B49 (2004) |
Francis Alexandre [France] ; Khaled Bsaïes [Tunisie] ; Moussa Demba [Tunisie] | Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures |
| 006C22 (2004) |
Dominique Larchey-Wendling [France] | Counter-Model Search in Gödel-Dummett Logics |
| 007A33 (2003) |
Christophe Ringeissen [France] | Matching in a Class of Combined Non-disjoint Theories |
| 007B71 (2003) |
J. Y. Marion [France] | Analysing the implicit complexity of programs |
| 008789 (2002) |
L. Habert [France] ; J.-M. Notin [France] ; D. Galmiche [France] | LINK: A Proof Environment Based on Proof Nets |
| 008815 (2002) |
Eric Deplagne [France] ; Claude Kirchner [France] | Deduction versus Computation: The Case of Induction |
| 009E47 (2000) |
Gregory Kucherov [France] ; Michaël Rusinowitch [France] | Patterns in Words versus Patterns in Trees: A Brief Survey and New Results |
| 00A956 (1999) |
Philippe De Groote [France] | On the Strong Normalization of Natural Deduction with Permutation-Conversions |
| 00A992 (1999) |
Gilles Dowek [France] ; Thérèse Hardin [France] ; Claude Kirchner [France] | HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic |
| 00B385 (1998) |
Christopher Lynch [États-Unis] ; Christelle Scharff [France] | Basic Completion with E-cycle Simplification |
| 00BC21 (1997) |
Christophe Ringeissen [France] | Prototyping combination of unification algorithms with the ELAN rule-based programming language |
| 00BC30 (1997) |
Miki Hermann [France] ; Phokion G. Kolaitis [États-Unis] | On the complexity of unification and disunification in commutative idempotent semigroups |
| 00C090 (1996) |
Narjes Berregeb [France] ; Adel Bouhoula [France] ; Michaël Rusinowitch [États-Unis, France] | Automated verification by induction with associative-commutative operators |
| 002721 (2011) |
Mouhebeddine Berrima ; Narjes Ben Rajeb [Tunisie] ; Véronique Cortier [France] | Deciding knowledge in security protocols under some e-voting theories |
| 002805 (2011) |
Isabelle Gnaedig [France] ; Hélène Kirchner [France] | Proving weak properties of rewriting |
| 002D71 (2010-04) |
Siva Anantharaman [France] ; Hai Lin ; Christopher Lynch ; Paliath Narendran ; Michael Rusinowitch [France] | Cap Unification: Application to Protocol Security modulo Homomorphic Encryption |
| 003002 (2010) |
Siva Anantharaman [France] ; Hai Lin [États-Unis] ; Christopher Lynch [États-Unis] ; Paliath Narendran [États-Unis] ; Michael Rusinowitch [France] | Unification Modulo Homomorphic Encryption |
| 004456 (2008) |
Jérome Besombes [France] ; Jean-Yves Marion [France] | LEARNING DISCRETE CATEGORIAL GRAMMARS FROM STRUCTURES |
| 005375 (2006) |
Mathieu Turuani [France] | The CL-Atse Protocol Analyser |
| 005407 (2006) |
Olivier Bournez [France] ; Florent Garnier [France] | Proving Positive Almost Sure Termination Under Strategies |
| 005416 (2006) |
Johanne Cohen [France] ; Fedor Fomin [Norvège] ; Pinar Heggernes [Norvège] ; Dieter Kratsch [France] ; Gregory Kucherov [France] | Optimal Linear Arrangement of Interval Graphs |
| 005471 (2006) |
Yannick Chevalier [France] ; Michaël Rusinowitch [France] | Hierarchical Combination of Intruder Theories |
| 005586 (2006) |
Florent Jacquemard [France] ; Michael Rusinowitch [France] ; Laurent Vigneron [France] | Tree automata with equality constraints modulo equational theories |
| 005600 (2006) |
Olivier Bournez [France] ; Felipe Cucker [Hong Kong] ; Paulin Jacobe De Naurois [France] ; Jean-Yves Marion [France] | Implicit complexity over an arbitrary structure : Quantifier alternations |
| 005612 (2006) |
Manin Abadi [États-Unis] ; Véronique Cortier [France] | Deciding knowledge in security protocols under equational thoories |
| 005623 (2006) |
Nachum Dershowitz [Israël] ; Claude Kirchner [France] | Abstract canonical presentations |
| 006192 (2005) |
Tomasz Truderung [Pologne] | Selecting Theories and Recursive Protocols |
| 006199 (2005) |
Tomasz Truderung [Pologne] | Regular Protocols and Attacks with Regular Knowledge |
| 006205 (2005) |
Guillaume Bonfante [France] ; Jean-Yves Marion [France] ; Jean-Yves Moyen [France] | Quasi-interpretations and Small Space Bounds |
| 006206 (2005) |
Olivier Bournez [France] ; Florent Garnier [France] | Proving Positive Almost-Sure Termination |
| 006279 (2005) |
Véronique Cortier [France] ; Bogdan Warinschi [États-Unis] | Computationally Sound, Automated Proofs for Security Protocols |
| 006376 (2005) |
Siva Anantharaman [France] ; Paliath Narendran [États-Unis] ; Michael Rusinowitch [France] | Closure properties and decision problems of dag automata |
| 006B40 (2004) |
Horatiu Cirstea [France] ; Luigi Liquori [France] ; Benjamin Wack [France] | Rewriting Calculus with Fixpoints: Untyped and First-Order Systems |
| 006C49 (2004) |
Frédéric Blanqui [France] | A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems |
| 006C91 (2004) |
Yves Lafont [France] | Soft linear logic and polynomial time |
| 006C99 (2004) |
L. Kristiansen [Norvège] ; K.-H. Niggl [Allemagne] | On the computational complexity of imperative programming languages |
| 006D02 (2004) |
N. Danner [États-Unis] ; C. Pollett [États-Unis] | Minimization and NP multifunctions |
| 006D23 (2004) |
Klaus Aehlig [Allemagne] ; Ulrich Berger [Royaume-Uni] ; Martin Hofinann [Allemagne] ; Helmut Schwichtenberg [Allemagne] | An arithmetic for non-size-increasing polynomial-time computation |
| 007969 (2003) |
Siva Anantharaman [France] ; Paliath Narendran [États-Unis] ; Michael Rusinowitch [France] | Unification Modulo ACUI Plus Homomorphisms/Distributivity |
| 007999 (2003) |
Olivier Bournez [France] ; Mathieu Hoyrup [France] | Rewriting Logic and Probabilities |
| 007A65 (2003) |
Mark Van Den Brand [Pays-Bas] ; Pierre-Etienne Moreau [France] ; Jurgen Vinju [Pays-Bas] | Environments for Term Rewriting Engines for Free! |
| 007A89 (2003) |
Jean-Raymond Abrial [France] ; Dominique Cansell [France] | Click’n Prove: Interactive Proofs within Set Theory |
| 007A93 (2003) |
Olivier Bournez [France] ; Guy-Marie Côme [France] ; Valérie Conraud [France] ; Hélène Kirchner [France] ; Liliana Ib Nescu [France] | Automated Generation of Kinetic Chemical Mechanisms Using Rewriting |
| 007B10 (2003) |
Nicolas Biri [France] ; Didier Galmiche [France] | A Separation Logic for Resource Distribution |
| 007B15 (2003) |
Olivier Bournez [France] ; Guy-Marie Côme [France] ; Valérie Conraud [France] ; Hélène Kirchner [France] ; Liliana Ib Nescu [France] | A Rule-Based Approach for Automated Generation of Kinetic Chemical Mechanisms |
| 007B50 (2003) |
Michaël Rusinowitch [France] ; Mathieu Turuani [France] | Protocol insecurity with a finite number of sessions and composed keys is NP-complete |
| 007B76 (2003) |
Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | A rewriting approach to satisfiability procedures |
| 008808 (2002) |
Germain Faure [France] ; Claude Kirchner [France] | Exceptions in the Rewriting Calculus |
| 008825 (2002) |
Silvio Ranise [France] | Combining Generic and Domain Specific Reasoning by Using Contexts |
| 008889 (2002) |
Abdessamad Imine [Tunisie] ; Yahya Slimani [Tunisie] ; Sorin Stratulat [France] | Using automated induction-based theorem provers for reasoning about concurrent systems |
| 009256 (2001) |
Alessandro Armando [Italie] ; Silvio Ranise [Italie, France] ; Michaël Rusinowitch [France] | Uniform Derivation of Decision Procedures by Superposition |
| 009279 (2001) |
Horatiu Cirstea [France] | Specifying Authentication Protocols Using Rewriting and Strategies |
| 009330 (2001) |
Christophe Ringeissen [France] | Matching with Free Function Symbols — A Simple Extension of Matching? |
| 009366 (2001) |
Hubert Comon [France] ; Claude Kirchner [France] | Constraint Solving on Terms |
| 009441 (2001) |
Horatiu Cirstea [France] ; Claude Kirchner [France] ; Luigi Liquori [France] | Matching power |
| 009D50 (2000) |
Iliano Cervesato [États-Unis] ; Joshua S. Hodas [États-Unis] ; Frank Pfenning [États-Unis] | Efficient resource management for linear logic proof search |
| 009E04 (2000) |
Miki Hermann [France] ; Phokion G. Kolaitis | Unification Algorithms Cannot Be Combined in Polynomial Time |
| 009E72 (2000) |
Philippe De Groote [France] | Linear Higher-Order Matching Is NP-Complete |
| 009F13 (2000) |
L. Bachmair [États-Unis] ; I. V. Ramakrishnan [États-Unis] ; A. Tiwari [États-Unis] ; L. Vigneron [France] | Congruence Closure Modulo Associativity and Commutativity |
| 009F49 (2000) |
Carlos Castro [France] ; Eric Monfroy [Pays-Bas] | A Control Language for Designing Constraint Solvers |
| 00A919 (1999) |
Philippe De Groote [France] | The Non-associative Lambek Calculus with Product in Polynomial Time |
| 00A932 (1999) |
Didier Galmiche [France] ; Dominique Larchey-Wendling | Structural Sharing and Efficient Proof-Search in Propositional Intuitionistic Logic |
| 00A946 (1999) |
Paliath Narendran [États-Unis] ; Michael Rusinowitch [France] ; Rakesh Verma [États-Unis] | RPO Constraint Solving Is in NP |
| 00A965 (1999) |
Hélèene Kirchner [France] ; Pierre-Etienne Moreau [France] | Non-deterministic Computations in ELAN |
| 00AA17 (1999) |
Veronique Cortier [France] ; Harald Ganzinger [Allemagne] ; Margus Veanes [Allemagne] ; Florent Jacquemard [France] | Decidable Fragments of Simultaneous Rigid Reachability |
| 00AA29 (1999) |
G. Bonfante [France] ; A. Cichon [France] ; J. Y. Marion [France] ; H. Touzet [France] | Complexity Classes and Rewrite Systems with Polynomial Interpretation |
| 00AB02 (1999) |
H. Kirchner [France] ; P. D. Mosses [États-Unis] | Algebraic specifications, higher-order types, and set-theoretic models |
| 00B239 (1998) |
E. A. Cichon [France] ; E. Tahhan Bittar [France] | Ordinal recursive bounds for Higman's theorem |
| 00B321 (1998) |
Eric Monfroy [Pays-Bas] ; Christophe Ringeissen [France] | SoleX: A domain-independent scheme for constraint solver extension |
| 00B336 (1998) |
Miki Hermann [France] ; Gernot Salzer [Autriche] | On the word, subsumption, and complement problem for recurrent term schematizations |
| 00B338 (1998) |
Narjes Berregeb [France] ; Adel Bouhoula [France] ; Michaël Rusinowitch [France] | Observational proofs with critical contexts |
| 00B346 (1998) |
Bernhard Gramlich [France] | Modular aspects of rewrite-based specifications |
| 00B372 (1998) |
Hélène Touzet [France] | Encoding the hydra battle as a rewrite system |
| 00B377 (1998) |
Thomas Genet [France] | Decidable approximations of sets of descendants and sets of normal forms |
| 00B401 (1998) |
Hélène Touzet [France] | A complex example of a simplifying rewrite system |
| 00B858 (1997) |
Christophe Ringeissen | Prototyping combination of unification algorithms with the ELAN rule-based programming language |
| 00BC06 (1997) |
Thomas Genet [France] ; Isabelle Gnaedig [France] | Termination proofs using gpo ordering constraints |
| 00BC15 (1997) |
Ali Amaniss [France] ; Miki Hermann [France] ; Denis Lugiez [France] | Set operations for recurrent term schematizations |
| 00BC24 (1997) |
Christian Retoré [France] | Pomset logic: A non-commutative extension of classical linear logic |
| 00BC45 (1997) |
Claude Kirchner [France] ; Christophe Ringeissen [France] | Higher-order equational unification via explicit substitutions |
| 00BF30 (1996) |
Adel Bouhoula [France] | Using induction and rewriting to verify and complete parameterized specifications |
| 00C004 (1996) |
Miki Hermann [France] ; Phokion G. Kolaitis [États-Unis] | Unification algorithms cannot be combined in polynomial time |
| 00C113 (1996) |
Marian Vittek [France] | A compiler for nondeterministic term rewriting systems |
| 00DA98 (1991) |
M. Rusinowitch [France] | Theorem-proving with resolution and superposition |
| 00E638 (1987) |
| Proceedings/2nd. International conference on rewriting techniques and applications, Bordeaux, France, May 25-27, 1987 |
| 000065 (2016-02-22) |
Walid Belkhir [France] ; Nicolas Ratier [France] ; Duy Duc Nguyen [France] ; Michel Lenczner [France] | Closed combination of context-embedding iterative strategies |
| 000664 (2015-01-01) |
Hugo Férée [France] ; Emmanuel Hainry [France] ; Mathieu Hoyrup [France] ; Romain Péchoux [France] | Characterizing polynomial time complexity of stream programs using interpretations |
| 000E42 (2014) |
Hans Van Ditmarsch [France] ; Sujata Ghosh [Inde] ; Rineke Verbrugge [Pays-Bas] ; YANJING WANG [République populaire de Chine] | Hidden protocols: Modifying our expectations in an evolving world |
| 001875 (2012-10-30) |
Karim Dahman [France] | Governance and Analysis of Business Processes Change Impact on Service Oriented Architectures: A Model-Driven Approach |
| 001E88 (2012) |
A. Bellanger [France] ; A. Janiak [Pologne] ; M. Y. Kovalyov [Biélorussie] ; A. Oulamara [France] | Scheduling an unbounded batching machine with job processing time compatibilities |
| 001E89 (2012) |
Vincent Boudht [France] ; Johanne Cohhn [France] ; Rodolphe Giroudeau [France] ; Jean-Clalide Könic [France] | SCHEDULING IN THE PRESENCE OF PROCESSOR NETWORKS: COMPLEXITY AND APPROXIMATION |
