Mostrar el registro sencillo del ítem

Ponencia

dc.creatorLambán Pardo, Laureanoes
dc.creatorMartín Mateos, Francisco Jesúses
dc.creatorRubio, Julioes
dc.creatorRuiz Reina, José Luises
dc.date.accessioned2019-05-07T08:12:37Z
dc.date.available2019-05-07T08:12:37Z
dc.date.issued2013
dc.identifier.citationLambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2013). Certified Symbolic Manipulation: Bivariate Simplicial Polynomials. En ISAAC'13: 38th International Symposium on Symbolic and Algebraic Computation (243-250), Boston, Maine, USA: ACM.
dc.identifier.isbn978-1-4503-2059-7es
dc.identifier.urihttps://hdl.handle.net/11441/86250
dc.description.abstractCertified symbolic manipulation is an emerging new field where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In this paper, we focus on algebraic algorithms implemented in the proof assistant ACL2, which allows us to verify correctness in the same programming environment. The case study is that of bivariate simplicial polynomials, a data structure used to help the proof of properties in Simplicial Topology. Simplicial polynomials can be computationally interpreted in two ways. As symbolic expressions, they can be handled algorithmically, increasing the automation in ACL2 proofs. As representations of functional operators, they help proving properties of categorical morphisms. As an application of this second view, we present the definition in ACL2 of some morphisms involved in the Eilenberg-Zilber reduction, a central part of the Kenzo computer algebra system. We have proved the ACL2 implementations are correct and tested that they get the same results as Kenzo does.es
dc.description.sponsorshipMinisterio de Ciencia e Innovación MTM2009-13842es
dc.description.sponsorshipUnión Europea nr. 243847 (ForMath)es
dc.formatapplication/pdfes
dc.language.isoenges
dc.publisherACMes
dc.relation.ispartofISAAC'13: 38th International Symposium on Symbolic and Algebraic Computation (2013), p 243-250
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.titleCertified Symbolic Manipulation: Bivariate Simplicial Polynomialses
dc.typeinfo:eu-repo/semantics/conferenceObjectes
dcterms.identifierhttps://ror.org/03yxnpp24
dc.type.versioninfo:eu-repo/semantics/submittedVersiones
dc.rights.accessRightsinfo:eu-repo/semantics/openAccesses
dc.contributor.affiliationUniversidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificiales
dc.relation.projectIDMTM2009-13842es
dc.relation.projectID243847 (ForMath)es
dc.relation.publisherversionhttps://dl.acm.org/citation.cfm?id=2465515es
dc.identifier.doi10.1145/2465506.2465515es
dc.contributor.groupUniversidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimientoes
idus.format.extent8es
dc.publication.initialPage243es
dc.publication.endPage250es
dc.eventtitleISAAC'13: 38th International Symposium on Symbolic and Algebraic Computationes
dc.eventinstitutionBoston, Maine, USAes
dc.relation.publicationplaceNew Yorkes

FicherosTamañoFormatoVerDescripción
Certified symbolic manipulation.pdf484.5KbIcon   [PDF] Ver/Abrir  

Este registro aparece en las siguientes colecciones

Mostrar el registro sencillo del ítem

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional