Modelling differential structures in proof assistants: The graded case
-
1
Universidad de La Rioja
info
ISSN: 0302-9743
Datum der Publikation: 2009
Ausgabe: 5717 LNCS
Nummer: 5717
Seiten: 203-210
Art: Artikel
Andere Publikationen in: Lecture Notes in Computer Science
Projekte im Zusammenhang
Zusammenfassung
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.