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

Any de publicació: 2011

Volum: 6564 LNCS

Pàgines: 37-51

Tipus: Article

beta Ver similares en nube de resultados
DOI: 10.1007/978-3-642-20551-4_3 SCOPUS: 2-s2.0-79955412840 WoS: WOS:000296753400003 GOOGLE SCHOLAR lock_openAccés obert editor

Altres publicacions en: Lecture Notes in Computer Science

Resum

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.