|
[5]
|
Delia Kesner.
Confluence of extensional and non-extensional λ-calculi with
explicit substitutions.
Theoretical Computer Science, 238(1--2):183--220, 2000.
[ bib |
.ps.gz ]
|
|
[4]
|
Gabriel Ciobanu and Mihai Rotaru.
A pi-calculus machine.
Electronical Journal of Universal Computer Science, 6(1), 2000.
[ bib |
http ]
|
|
[3]
|
Alexandre Boudet.
Unification of higher-order patterns modulo simple syntactic
equational theories.
Discrete Mathematics and Theoretical Computer Science,
4(1):11--30, 2000.
[ bib ]
|
|
[2]
|
A. Bouhoula, J.-P. Jouannaud, and J. Meseguer.
Specification and proof in membership equational logic.
Theoretical Computer Science, 236:35--132, 2000.
[ bib ]
|
|
[1]
|
Joachim Niehren, Sophie Tison, and Ralf Treinen.
On rewrite constraints and context unification.
Information Processing Letters, 74(1--2):35--40, 2000.
[ bib |
.ps.gz |
Abstract ]
|
|
[11]
|
François Pottier and Sylvain Conchon.
Information flow inference for free.
In Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming (ICFP'00), pages 46--57, Montréal,
Canada, September 2000.
[ bib |
.ps.gz ]
|
|
[10]
|
J.-P. Jouannaud.
Model checking versus theorem proving for verifying protocols.
In In Proc. Distributed Systems Verification and Validation,
April 2000.
[ bib ]
|
|
[9]
|
Eduardo Bonelli, Delia Kesner, and Alejandro Ríos.
A de bruijn notation for higher-order rewriting.
In Leo Bachmair, editor, 11th International Conference on
Rewriting Techniques and Applications, volume 1833 of Lecture Notes in
Computer Science, pages 62--79, Norwich, UK, July 2000. Springer.
[ bib ]
|
|
[8]
|
Roberto Di Cosmo, Delia Kesner, and Emmanuel Polonovski.
Proof nets and explicit substitutions.
In Jerzy Tiuryn, editor, Foundations of Software Science and
Computation Structures, volume 1784 of Lecture Notes in Computer
Science, Berlin, Germany, March 2000. Springer.
[ bib ]
|
|
[7]
|
F. Blanqui.
Termination and confluence of higher-order rewrite systems.
In Leo Bachmair, editor, 11th International Conference on
Rewriting Techniques and Applications, volume 1833 of Lecture Notes in
Computer Science, Norwich, UK, July 2000. Springer.
[ bib ]
|
|
[6]
|
Pierre Letouzey and Laurent Théry.
Formalizing Stålmarck's algorithm in Coq.
In J. Harrison and M. Aagaard, editors, Theorem Proving in
Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869
of Lecture Notes in Computer Science, pages 387--404. Springer, 2000.
[ bib |
.ps.gz ]
|
|
[5]
|
Évelyne Contejean, Antoine Coste, and Benjamin Monate.
Rewriting techniques in theoretical physics.
In Leo Bachmair, editor, 11th International Conference on
Rewriting Techniques and Applications, volume 1833 of Lecture Notes in
Computer Science, pages 80--94, Norwich, UK, July 2000. Springer.
[ bib |
DOI |
Abstract ]
|
|
[4]
|
Enno Ohlebusch, Claus Claves, and Claude Marché.
TALP: A tool for the termination analysis of logic programs.
In Leo Bachmair, editor, 11th International Conference on
Rewriting Techniques and Applications, volume 1833 of Lecture Notes in
Computer Science, pages 270--273, Norwich, UK, July 2000. Springer.
Available at http://bibiserv.techfak.uni-bielefeld.de/talp/.
[ bib |
http ]
|
|
[3]
|
Frédéric Prost.
A static calculus of dependencies for the λ-cube.
In Martin Abadi, editor, Fiveteenth Annual IEEE Symposium on
Logic in Computer Science, Santa Barbara, California, June 2000. IEEE
Comp. Soc. Press.
[ bib ]
|
|
[2]
|
Ralf Treinen.
Predicate logic and tree automata with tests.
In Jerzy Tiuryn, editor, Foundations of Software Science and
Computation Structures, volume 1784 of Lecture Notes in Computer
Science, pages 329--343, Berlin, Germany, March 2000. Springer.
[ bib |
.ps.gz |
Abstract ]
|
|
[1]
|
Daria Walukiewicz-Chrząszcz.
Termination of rewriting in the Calculus of Constructions.
In Proceedings of the Workshop on Logical Frameworks and
Meta-languages, Santa Barbara, California, 2000.
Part of the LICS'2000.
[ bib ]
|
|
[4]
|
Jean-Christophe Filliâtre.
Design of a proof assistant: Coq version 7.
Research Report 1369, LRI, Université Paris Sud, October 2000.
[ bib |
full text on HAL |
.ps.gz ]
|
|
[3]
|
Jean-Christophe Filliâtre.
Hash consing in an ML framework.
Research Report 1368, LRI, Université Paris Sud, September
2000.
[ bib |
.ps.gz ]
|
|
[2]
|
B. Bérard, P. Castéran, E. Fleury, L. Fribourg, J.-F. Monin, C. Paulin,
A. Petit, and D. Rouillard.
Automates temporisés calife.
Fourniture F1.1, Calife, 2000.
[ bib ]
|
|
[1]
|
P. Castéran, E. Freund, C. Paulin, and D. Rouillard.
Bibliothèques coq et isabelle-hol pour les systèmes de
transitions et les p-automates.
Fourniture F5.4, Calife, 2000.
[ bib ]
|