Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System

  1. Heras, J. 1
  2. Pascual, V. 1
  3. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Lecture Notes in Computer Science

ISSN: 0302-9743

Año de publicación: 2011

Volumen: 6564 LNCS

Páginas: 37-51

Tipo: Artículo

DOI: 10.1007/978-3-642-20551-4_3 SCOPUS: 2-s2.0-79955412840 WoS: WOS:000296753400003 GOOGLE SCHOLAR lock_openAcceso abierto editor

Otras publicaciones en: Lecture Notes in Computer Science

Resumen

Kenzo is a Common Lisp system devoted to Algebraic Topology. Although Kenzo uses higher-order functional programming intensively, we show in this paper how the theorem prover ACL2 can be used to prove the correctness of first order fragments of Kenzo. More concretely, we report on the verification in ACL2 of the implementation of simplicial sets. By means of a generic instantiation mechanism, we achieve the reduction of the proving effort for each family of simplicial sets, letting ACL2 automate the routine parts of the proofs. © 2011 Springer-Verlag.