- [Alv00]
-
C. Alvarado.
Reflection for rewriting in the Calculus of Inductive
Constructions.
In workshop TYPES'2000, Durham, UK, Dec 2000.
- [AN]
-
Cuihtlauac Alvarado and Quang-Huy Nguyen.
Elan for equational reasoning in coq.
Workshop on Logical Frameworks and Meta-languages, LICS'2000.
- [BBF+01]
-
B. Bérard, M. Bidoit, A. Finkel, A. Petit, L. Petrucci, and Ph. Schnoebelen.
System and Software Verification, Model-Checking Techniques and
Tools.
Springer, 2001.
- [BDFP00]
-
P. Bouyer, C. Dufourd, E. Fleury, and A. Petit.
Are timed automata updatable ?
In Proc. 12th Int. Conf.Computer Aided Verification (CAV'2000),
volume 1855 of Lecture Notes in Computer Science, Chicago, IL, USA,
July 2000. Springer.
- [BFKM01]
-
B. Bérard, L. Fribourg, F. Klay, and J.-F. Monin.
A compared study of two correctness proofs for the standardized
algorithm of abr conformance.
Formal Methods in System Design, 2001.
to appear, http://www.lsv.ens-cachan.fr/ berard/publis.html.
- [BJO01]
-
F. Blanqui, J.-P. Jouannaud, and M Okada.
Inductive Data Type Systems.
Theoretical Computer Science, (277), 2001.
- [Bla01]
-
F. Blanqui.
Definitions by rewriting in the Calculus of Constructions.
In IEEE Symposium on Logic in Computer Science, 2001.
- [BPT01]
-
P. Bouyer, A. Petit, and D. Thérien.
An algebraic characterization of data and timed languages.
In Proc. 12th Int. Conf. Concurrency Theory (CONCUR'2001),
volume 2154 of Lecture Notes in Computer Science, pages 248--261,
Aalborg, Denmark, Aug 2001. Springer.
- [Chr00]
-
J. Chrzaszcz.
Modular rewriting in the Calculus of Constructions.
In workshop TYPES'2000, Durham, UK, Dec 2000.
- [CL00]
-
F. Cassez and F. Laroussinie.
Model-checking for hybrid systems by quotienting and constraints
solving.
In Proc. 12th Int. Conf. Computer Aided Verification
(CAV'2000), Chicago, IL, USA, July 2000, volume 1855 of Lecture Notes
in Computer Science, pages 373--388. Springer, 2000.
- [CN98]
-
H. Comon and R. Nieuwenhuis.
Induction = i-axiomatization + first-order consistency.
Research report LSV-98-9, LSV, October 1998.
To appear in Information and Computation, special issue on RTA'98.
- [Cou]
-
J. Courant.
A Module Calculus for Pure Type Systems.
submitted to Journal of Functional Programming.
- [CR00]
-
Pierre Castéran and Davy Rouillard.
Reasoning about parametrized automata.
In RTS'2000, Paris, 2000.
- [DHK98]
-
Gilles Dowek, Thérèse Hardin, and Claude Kirchner.
Theorem proving modulo.
Rapport de Recherche 3400, Institut National de Recherche en
Informatique et en Automatique, April 1998.
ftp://ftp.inria.fr/INRIA/publication/RR/RR-3400.ps.gz.
- [DK]
-
Eric Deplagne and Claude Kirchner.
Induction as deduction modulo.
- [dT]
-
The Coq development Team.
The Proof Assistant Coq V7.1.
http://coq.inria.fr.
- [LL98]
-
F. Laroussinie and K. G. Larsen.
CMC: A tool for compositional model-checking of real-time
systems.
In Proc. IFIP Joint Int. Conf. Formal Description
Techniques & Protocol Specification, Testing, and Verification
(FORTE-PSTV'98), Paris, France, Nov. 1998, pages 439--456. Kluwer Academic,
1998.
- [Mon00]
-
Jean-François Monin.
Proving the Correctness of the Standardized Algorithm for ABR
Conformance.
Formal Methods in System Design, 17(3):221--243, december
2000.
- [Ngu01a]
-
Q-H. Nguyen.
Certifying term rewriting in ELAN.
In Mark van den Brand and Rakesh Verma, editors, Proc. second
RULE workshop, volume 59. Elsevier Science Publishers, September 2001.
- [Ngu01b]
-
Q-H. Nguyen.
Compact normalisation trace via lazy rewriting.
In S. Lucas and B. Gramlich, editors, Proc. 12th Int. Workshop
on Reduction Strategies and Programming (WRS 2001), volume 2359, pages
79--96. Servicio de Publicaciones, Universidad Politécnica de Valencía, May
2001.
- [RCCF00]
-
Davy Rouillard, R. Castanet, P. Castéran, and P. Félix.
Preparing Testing by Proving Critical Systems.
In 15th World Conference on Non-Destructive Testing, Roma, Sept
2000.
- [Stu01]
-
Jürgen Stuber.
A Model-based Completeness Proof of Extended Narrowing And
Resolution.
In 1st Int. Joint Conf. on Automated Reasoning (IJCAR-2001),
Siena, Italy, volume 2083 of LNCS, pages 195--210. Springer, June
2001.
- [Wal]
-
D. Walukiewicz.
Termination of rewriting in the calculus of constructions.
submitted to Journal of Functional Programming.