date_range Durée de 01 octobre 2006 à 30 septembre 2009 (36 mois) Fini
euro 21 780,00 EUR

Sphère National.

Chercheurs

Foto de Julio
Julio
Rubio García
Responsable
Foto de Jesús María
Jesús María
Aransay Azofra
Foto de César
César
Domínguez Pérez
Foto de Laureano
Laureano
Lambán Pardo
Foto de Ana
Ana
Romero Ibáñez

Publications liées au projet

Montrer par typologie

2009

  1. Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems

    Lectures Notes in Computer Science: Intelligent Computer Mathematics16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings

  2. Modelling differential structures in proof assistants: The graded case

    Lecture Notes in Computer Science

2008

  1. Intelligent Computer Mathematics: 9th International Conference, AISC 2008 15th Symposium, Calculemus 2008 7th International Conference, MKM 2008 Birmingham, UK, July 28 - August 1, 2008, Proceedings

    Springer

  2. A mechanized proof of the Basic Perturbation Lemma

    Journal of Automated Reasoning

  3. Mechanized Reasoning in Homological Algebra

    AI Communications

  4. Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems

    Lecture Notes in Computer Science

  5. Mediated access to Symbolic Computation Systems

    Lecture Notes in Computer Science

2007

  1. Formal Modelling of a Coordination System: from Practice to Theory, and back again

    Lecture Notes in Computer Science, 2007, Volume 4457

  2. Object Oriented Institutions to Specify Symbolic Computation System

    RAIRO - Informatique Théorique et Applications

  3. Executing in Common Lisp, Proving in ACL2.

    Lecture Notes in Computer Science

  4. Formal Reasoning on a Web Coordination System

    Lecture Notes in Computational Science and Engineering

2006

  1. Modeling Inheritance as coercion in the Kenzo System.

    Journal of Universal Computer Science