|
[5]
|
Martin Müller, Joachim Niehren, and Ralf Treinen.
The first-order theory of ordering constraints over feature trees.
Discrete Mathematics and Theoretical Computer Science,
4(2):193--234, September 2001.
[ bib |
.ps.gz ]
|
|
[4]
|
Franck Seynhaeve, Sophie Tison, Marc Tommasi, and Ralf Treinen.
Grid structures and undecidable constraint theories.
Theoretical Computer Science, 258(1--2):453--490, May 2001.
[ bib ]
|
|
[3]
|
Eduardo Bonelli.
Perpetuality in a named lambda calculus with explicit substitutions.
Mathematical Structures in Computer Science, 11(1), 2001.
[ bib ]
|
|
[2]
|
Adel Bouhoula and Jean-Pierre Jouannaud.
Automata-driven automated induction.
Information and Computation, 169(1), 2001.
[ bib |
.ps.gz |
Abstract ]
|
|
[1]
|
R. David and B. Guillaume.
A λ-calculus with explicit weakening and explicit
substitution.
Mathematical Structures in Computer Science, 11(1), 2001.
[ bib ]
|
|
[11]
|
Évelyne Contejean and Ana Paula Tomas.
On Symmetries in Systems Coming from AC-Unification of Higher-Order
Patterns.
In Pierre Flener and Justin Pearson, editors, SymCon'01,
Symmetry in Constraints, Paphos, Cyprus, December 2001.
[ bib ]
|
|
[10]
|
Eduardo Bonelli, Delia Kesner, and Alejandrio Ríos.
From higher-order to first-order rewriting (extended abstract).
In Aart Middeldorp, editor, 12th International Conference on
Rewriting Techniques and Applications, volume 2051 of Lecture Notes in
Computer Science, Utrecht, The Netherlands, May 2001. Springer.
[ bib ]
|
|
[9]
|
Alexandre Boudet and Evelyne Contejean.
Combining Pattern E-unification Algorithms.
In Aart Middeldorp, editor, 12th International Conference on
Rewriting Techniques and Applications, volume 2051 of Lecture Notes in
Computer Science, pages 63--76, Utrecht, The Netherlands, May 2001.
Springer.
[ bib |
DOI |
Abstract ]
|
|
[8]
|
Gabriel Ciobanu and Mihai Rotaru.
JC-Nets.
volume 2055 of Lecture Notes in Computer Science, pages
190--201, Chisinau, Moldova, May 2001. Springer.
[ bib ]
|
|
[7]
|
Sylvain Conchon and François Pottier.
JOIN(X): Constraint-based type inference for the join-calculus.
In David Sands, editor, Proceedings of the 10th European
Symposium on Programming (ESOP'01), volume 2028 of Lecture Notes in
Computer Science, pages 221--236, Genova, Italy, April 2001. Springer.
[ bib |
.ps.gz ]
|
|
[6]
|
Frédéric Blanqui.
Definitions by rewriting in the calculus of constructions.
In Sixteenth Annual IEEE Symposium on Logic in Computer
Science. IEEE Comp. Soc. Press, 2001.
[ bib ]
|
|
[5]
|
Pierre Courtieu.
Normalized Types.
In Laurent Fribourg, editor, Proceedings of the Annual
Conference of the European Association for Computer Science Logic, volume
2142 of Lecture Notes in Computer Science, pages 554--569, Paris,
France, September 2001. Springer.
[ bib ]
|
|
[4]
|
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, and Natarajan
Shankar.
ICS: Integrated Canonization and Solving (Tool presentation).
In G. Berry, H. Comon, and A. Finkel, editors, Proceedings of
CAV'2001, volume 2102 of Lecture Notes in Computer Science, pages
246--249. Springer, 2001.
[ bib ]
|
|
[3]
|
Christine Paulin-Mohring.
Modelisation of timed automata in Coq.
In N. Kobayashi and B. Pierce, editors, Theoretical Aspects of
Computer Software (TACS'2001), volume 2215 of Lecture Notes in Computer
Science, pages 298--315. Springer-Verlag, 2001.
[ bib ]
|
|
[2]
|
Alexander Koller, Joachim Niehren, and Ralf Treinen.
Dominance constraints: Algorithms and complexity.
In Michael Moortgat, editor, Logical Aspects of Computational
Linguistics 1998, volume 2014 of Lecture Notes in Artificial
Intelligence, pages 106--125, Grenoble, France, 2001. Springer.
[ bib |
.ps.gz ]
|
|
[1]
|
Xavier Urbain.
Automated incremental termination proofs for hierarchically defined
term rewriting systems.
In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors,
First International Joint Conference on Automated Reasoning, volume
2083 of Lecture Notes in Artificial Intelligence, pages 485--498,
Siena, Italy, June 2001. Springer.
[ bib |
.ps.gz ]
|
|
[5]
|
Eduardo Bonelli.
Substitutions explicites et réécriture de termes.
Thèse de doctorat, Université Paris-Sud, Orsay, France,
November 2001.
[ bib ]
|
|
[4]
|
Xavier Urbain.
Approche incrémentale des preuves automatiques de
terminaison.
Thèse de doctorat, Université Paris-Sud, Orsay, France,
October 2001.
http://www.lri.fr/~urbain/textes/these.ps.gz.
[ bib |
.ps.gz ]
|
|
[3]
|
F. Blanqui.
Théorie des Types et Récriture.
PhD thesis, Université Paris XI, Orsay, France, 2001.
[ bib ]
|
|
[2]
|
Pierre Courtieu.
Représentation d'algèbres non libres en théorie des
types.
PhD thesis, Université Paris-Sud, 2001.
[ bib ]
|
|
[1]
|
Delia Kesner.
Un parcours de la réécriture d'ordre supérieur à
la réécriture du premier ordre.
Thèse d'habilitation à diriger des recherches, Université
Paris-Sud XI, 2001.
[ bib ]
|
|
[4]
|
G. Huet, G. Kahn, and Ch. Paulin-Mohring.
The Coq Proof Assistant - A tutorial - Version 7.1,
October 2001.
[ bib |
http ]
|
|
[3]
|
Judicaël Courant.
MC2: A Module Calculus for Pure Type Systems.
Research Report 1292, LRI, September 2001.
[ bib |
.ps ]
|
|
[2]
|
Franz Baader, Volker Diekert, Cesare Tinelli, and Ralf Treinen.
Unif 2001 - 15th international workshop on unification.
Technical Report DII 09/01, Università degli Studi di Siena,
Dipartimento di Ingegneria dell'Informazione, Siena, Italy, June 2001.
[ bib ]
|
|
[1]
|
Pierre Courtieu.
Normalized types.
Research Report 1277, LRI, 2001.
[ bib ]
|