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

Aldizkaria:
Lecture Notes in Computer Science

ISSN: 0302-9743

Argitalpen urtea: 2011

Alea: 6564 LNCS

Orrialdeak: 37-51

Mota: Artikulua

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_openSarbide irekia editor

Beste argitalpen batzuk: Lecture Notes in Computer Science

Laburpena

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.