Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Publications 2000

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports

Books and book chapters

[1] J. A. Goguen, T. Winkler, José Meseguer, Kokichi Futatsugi, and Jean-Pierre Jouannaud. Software Engineering with OBJ: Algebraic Specification in Action, chapter Introducing OBJ*. Kluwers Academic Publishers, 2000. [ bib ]

Journals

[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 ]

Conferences

[11] François Pottier and Sylvain Conchon. Information flow inference for free. In Proceedings of the 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 ]

PhD theses

[1] Mina Abdiche. π-calcul et sous-typage: inférence de types et codages du λ-calcul dans le π-calcul. PhD thesis, Université Paris-Sud, July 2000. [ bib ]

Misc.

[2] Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain. CiME version 2, 2000. Available at http://cime.lri.fr/. [ bib | http ]
[1] Pierre Letouzey. Exécution de termes de preuves: une nouvelle méthode d'extraction pour le Calcul des Constructions Inductives. Université Paris VI, 2000. [ bib | http ]

Reports

[4] Jean-Christophe Filliâtre. Design of a proof assistant: Coq version 7. Research Report 1369, LRI, Université Paris Sud, October 2000. [ bib | .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 ]

Back

Books / Journals / Conferences / PhD theses / Misc. / Reports


This page was generated by bibtex2html.