Wiki Agenda Contact Version française

Publications 2003

Back

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

Books and book chapters

[1] Laurence Puel. La sécurité sociale, chapter Rapport de la 6ème chambre de la Cour des Comptes: Le système d'information de la caisse nationale d'Assurance Vieillesse. édition des journaux officiels, September 2003. [ bib ]

Journals

[3] Jean-Christophe Filliâtre and F. Pottier. Producing All Ideals of a Forest, Functionally. Journal of Functional Programming, 13(5):945--956, September 2003. [ bib | PDF ]
[2] Jean-Christophe Filliâtre. Verification of non-functional programs using interpretations in type theory. Journal of Functional Programming, 13(4):709--745, July 2003. [ bib | PDF | .pdf ]
[1] Delia Kesner Roberto Di Cosmo and Emmanuel Polonovski. Proof nets and explicit substitutions. Mathematical Structures in Computer Science, 13(3):409--450, 2003. [ bib ]

Conferences

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

PhD theses

[2] Julien Forest. Réécriture d'ordre supérieur avec motifs. Thèse de doctorat, Université Paris-Sud, Orsay, France, September 2003. http://www.pps.jussieu.fr/~forest/these/TheseForest.ps.gz. [ bib | .ps.gz ]
[1] Daria Walukiewicz-Chrzaszcz. Termination of Rewriting in the Calculus of Constructions. PhD thesis, Warsaw University, Poland and Université de Paris-Sud, April 2003. [ bib ]

Misc.

Reports

[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. http://www.lri.fr/~filliatr/ftp/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 ]

Back

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


This page was generated by bibtex2html.