Papers and technical reports about ELAN


Applications -- Proving

- [48] C. Alvarado and Q-H. Nguyen:
ELAN for equational reasoning in Coq - Proceeding of 2nd Workshop on Logical Frameworks and Metalanguages, Santa Barbara, California, USA, June 2000.

- [44] H. Cirstea:
Specifying Authentication Protocols Using ELAN - Workshop on Modelling and Verification, Besancon, France, December 1999.

- [39] C. Scharff:
Déduction avec contraintes et simplification dans les théories équationnelles - In French. Thèse de Doctorat d'Université, Université Henri Poincaré - Nancy I, September 1999.

- [25] T. Genet:
Decidable Approximation of Sets of Descendants and Sets of Normal Forms - In Proceedings 9th Conference on Rewriting Technics and Applications, Tsukuba (Japan), volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer-Verlag, 1998.

- [43] H. Cirstea and C. Kirchner:
Using Rewriting and Strategies for Describing the B Predicate Prover - Proceedings of the Workshop on Strategies in Automated Deduction, CADE-15, Lindau, Germany, July, 1998.

- [24] H. Kirchner, P.E. Moreau:
Prototyping Completion with Constraints using Computational Systems - Technical Report, 1994 , also in RTA'95 system demos.
A description using computational systems of the completion procedure with constraints.

- [57] O. Fissore:
Terminaison de la réécriture sous stratégies - In French. Thèse de Doctorat d'Université, Université Henri Poincaré - Nancy I, December 2003.