[11]
|
Sava Krstić and Sylvain Conchon.
Canonization for disjoint unions of theories.
In Franz Baader, editor, Proceedings of the 19th International
Conference on Automated Deduction (CADE-19), volume 2741 of Lecture
Notes in Computer Science, Miami Beach, FL, USA, July 2003. Springer.
[ bib |
.ps.gz ]
|
[10]
|
Sylvain Conchon and Sava Krstić.
Strategies for combining decision procedures.
In Proceedings of the 9th Tools and Algorithms for the
Construction and Analysis of Systems (TACAS'03), volume 2619 of Lecture
Notes in Computer Science, pages 537--553, Warsaw, Poland, April 2003.
Springer.
[ bib |
.ps.gz ]
|
[9]
|
Julien Forest and Delia Kesner.
Expression reduction systems with patterns.
In Roberto Nieuwenhuis, editor, 14th International Conference on
Rewriting Techniques and Applications, volume 2706 of Lecture Notes in
Computer Science, pages 107--122, Valencia, Spain, June 2003. Springer.
[ bib |
.ps ]
|
[8]
|
Vincent Cremet, Koji Hasebe, Jean-Pierre Jouannaud, Antoine Kremer, and
Mitsuhiro Okada.
Fatalis : Real time processes as linear logic specifications.
In International Workshop on Automated Verification of
Infinite-State Systems, Varsaw, 2003.
[ bib ]
|
[7]
|
Pierre Letouzey.
A new extraction for Coq.
In Herman Geuvers and Freek Wiedijk, editors, TYPES 2002,
volume 2646 of Lecture Notes in Computer Science. Springer, 2003.
[ bib |
.ps.gz ]
|
[6]
|
Évelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain.
Proving termination of rewriting with cime.
In Albert Rubio, editor, Extended Abstracts of the 6th
International Workshop on Termination, WST'03, pages 71--73, June 2003.
Technical Report DSIC II/15/03, Universidad Politécnica de
Valencia, Spain.
[ bib |
http ]
|
[5]
|
Nicolas Oury.
Observational equivalence and program extraction in the Coq Proof
Assistant.
In Martin Hofmann, editor, TLCA, volume 2701 of Lecture
Notes in Computer Science, pages 271--285. Springer, 2003.
[ bib ]
|
[4]
|
Alexandre Miquel.
A strongly normalising Curry-Howard correspondence for IZF set
theory.
In Computer Science Logic, CSL'03, Lecture Notes in Computer
Science. Springer, 2003.
[ bib ]
|
[3]
|
Alexandre Miquel and Benjamin Werner.
The not so simple proof-irrelevant model of CC.
In Herman Geuvers and Freek Wiedijk, editors, TYPES 2002,
volume 2646 of Lecture Notes in Computer Science, pages 240--258.
Springer, 2003.
[ bib ]
|
[2]
|
Enno Ohlebusch, Claus Claves, and Claude Marché.
The talp tool for termination analysis of logic programs.
In Albert Rubio, editor, Extended Abstracts of the 6th
International Workshop on Termination, WST'03, June 2003.
http://bibiserv.techfak.uni-bielefeld.de/talp/.
[ bib |
http ]
|
[1]
|
Julien Signoles.
Calcul statique des applications de modules paramétrés.
In Journées Francophones des Langages Applicatifs, January
2003.
[ bib ]
|
[5]
|
Pierre Corbineau.
First-order reasoning in the Calculus of Inductive Constructions.
Research Report 1380, LRI, December 2003.
[ bib ]
|
[4]
|
Jean-Christophe Filliâtre.
Why: a multi-language multi-prover verification tool.
Research Report 1366, LRI, Université Paris Sud, March 2003.
https://usr.lmf.cnrs.fr/~jcf/publis/why-tool.ps.gz.
[ bib |
.ps.gz ]
|
[3]
|
Coq development team.
The Coq Proof Assistant Reference Manual -- Version V7.4,
February 2003.
http://coq.inria.fr/doc/main.html.
[ bib |
Abstract ]
|
[2]
|
Néstor Cataño, Marek Gawkowski, Marieke Huisman, Bart Jacobs, Claude
Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain.
Logical techniques for applet verification.
Deliverable 5.2, IST VerifiCard Project, 2003.
http://www.cs.kun.nl/VerifiCard/files/deliverables/deliverable_5_2.pdf.
[ bib |
.pdf ]
|
[1]
|
Néstor Cataño, M. Gawlowski, Marieke Huisman, Bart Jacobs, Claude
Marché, Christine Paulin, Erik Poll, Nicole Rauch, and Xavier Urbain.
Logical techniques for applet verification.
Deliverable 5.2, IST VerifiCard project, 2003.
[ bib ]
|