[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, Évelyne 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]
|
Évelyne 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 ]
|