[12]	Mina Abdiche. A type inference algorithm for the polyadic pi-calculus with a sub-sort relation. In Journées du pôle programmation fonctionnelle, Orléans, November 1996. PRC/GDR Programmation du CNRS. [ bib ]
[11]	Ralf Treinen. The first-order theory of one-step rewriting by a linear term rewriting system is undecidable (extended abstract). In Klaus Schulz and Stephan Kepser, editors, Extended Abstracts of the Tenth International Workshop on Unification, Herrsching, Germany, June 1996. Published as CIS-Bericht-96-91, Universität München. [ bib ]
[10]	Delia Kesner. Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 184-199, New Brunswick, NJ, USA, July 1996. Springer. [ bib ]
[9]	Alexandre Boudet and Hubert Comon. Diophantine equations, Presburger arithmetic and finite automata. In H. Kirchner, editor, Proc. Coll. on Trees in Algebra and Programming (CAAP'96), Lecture Notes in Computer Science, pages 30-43, 1996. [ bib ]
[8]	Alexandre Boudet, Evelyne Contejean, and Claude Marché. AC-complete unification and its application to theorem proving. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 18-32, New Brunswick, NJ, USA, July 1996. Springer. [ bib | DOI | PDF | Abstract ]
[7]	Evelyne Contejean and Claude Marché. CiME: Completion Modulo E. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 416-419, New Brunswick, NJ, USA, July 1996. Springer. System Description available at http://cime.lri.fr/. [ bib | DOI | PDF | http | Abstract ]
[6]	Maria C.F. Ferreira, Delia Kesner, and Laurence Puel. λ-calculi with explicit substitutions and composition which preserve β-strong normalization (extended abstract). In Michael Hanus and Mario Rodríguez-Artalejo, editors, 5th International Conference on Algebraic and Logic Programming, volume 1139 of Lecture Notes in Computer Science, pages 284-298, Aachen, Germany, September 1996. Springer. [ bib ]
[5]	Jean-Pierre Jouannaud and Albert Rubio. A recursive path ordering for higher-order terms in η-long β-normal form. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 108-122, New Brunswick, NJ, USA, July 1996. Springer. [ bib | .ps.gz | Abstract ]
[4]	Florent Jacquemard. Decidable approximations of terms rewriting systems. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 362-376, New Brunswick, NJ, USA, July 1996. Springer. [ bib ]
[3]	Ralf Treinen. The first-order theory of one-step rewriting is undecidable. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 276-286, New Brunswick, NJ, USA, July 1996. Springer. [ bib ]
[2]	Judicaël Courant. Un calcul de modules pour coq. In Actes de la journée du Pôle Preuves et Spécifications Algébriques du GDR de programmation, Orléans, France, 1996. [ bib ]
[1]	Christine Paulin-Mohring. Circuits as streams in Coq : Verification of a sequential multiplier. In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, TYPES'95, volume 1158 of Lecture Notes in Computer Science. Springer, 1996. [ bib ]