Modelling differential structures in proof assistants: The graded case

  1. Aransay, J. 1
  2. Domínguez, C. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2009

Alea: 5717 LNCS

Zenbakia: 5717

Orrialdeak: 203-210

Mota: Artikulua

DOI: 10.1007/978-3-642-04772-5_27 SCOPUS: 2-s2.0-77954885019 WoS: WOS:000273999000027 GOOGLE SCHOLAR

Beste argitalpen batzuk: Lecture Notes in Computer Science

Lotura duten proiektuak

Sistemas de cálculo simbólico: nuevos desarrollos en topología algebráica y fiabilidad

2006/00092/001

Laburpena

In this work we propose a representation of graded algebraic structures and morphisms over them appearing in the field of Homological Algebra in the proof assistants Isabelle and Coq. We provide particular instances of these representations in both systems showing the correctness of the representation. Moreover the adequacy of such representations is illustrated by developing a formal proof of the Trivial Perturbation Lemma in both systems. © 2009 Springer-Verlag Berlin Heidelberg.