{"id":4356,"date":"2014-07-07T09:16:33","date_gmt":"2014-07-07T07:16:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4356"},"modified":"2014-07-07T09:18:04","modified_gmt":"2014-07-07T07:18:04","slug":"towards-abstract-and-executable-multivariate-polynomials-in-isabelle","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/towards-abstract-and-executable-multivariate-polynomials-in-isabelle\/","title":{"rendered":"Towards abstract and executable multivariate polynomials in Isabelle"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle\/HOL<\/a> sobre \u00e1lgebra computacional titulado <a href=\"http:\/\/bit.ly\/1pF2eo2\">Towards abstract and executable multivariate polynomials in Isabelle<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/isabelle.in.tum.de\/~haftmann\">Florian Haftmann<\/a>, TU Munich<\/li>\n<li><a href=\"http:\/\/www.infsec.ethz.ch\/people\/andreloc\">Andreas Lochbihler<\/a>, Institute of Information Security, ETH Zurich<\/li>\n<li><a href=\"http:\/\/www.risc.jku.at\/people\/schreine\">Wolfgang Schreiner<\/a>, RISC, Johannes Kepler University Linz<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  This work in progress report envisions a library for multivariate polynomials developed jointly by experts from computer theorem proving (CTP) and computer algebra (CA). The urgency of verified algorithms has been recognised in the field of CA, but the cultural gap to CTP is considerable; CA users expect high usability and efficiency. This work collects the needs of CA experts and reports on the design of a proof-of-concept prototype in Isabelle\/HOL. The CA requirements have not yet been fully settled, and its development is still at an early stage. The authors hope for lively discussions at the Isabelle Workshop.\n<\/p><\/blockquote>\n<p>El trabajo se presentar\u00e1 el pr\u00f3ximo domingo en el <a href=\"http:\/\/www.easychair.org\/smart-program\/VSL2014\/Isabelle-program.html\">Isabelle Workshop<\/a> del <a href=\"http:\/\/vsl2014.at\">Vienna Summer of Logic (VSL2014)<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre \u00e1lgebra computacional titulado Towards abstract and executable multivariate polynomials in Isabelle. Sus autores son Florian Haftmann, TU Munich Andreas Lochbihler, Institute of Information Security, ETH Zurich Wolfgang Schreiner, RISC, Johannes Kepler University Linz Su resumen es This work in progress report envisions a library&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[85,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4356"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4356"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4356\/revisions"}],"predecessor-version":[{"id":4358,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4356\/revisions\/4358"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4356"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4356"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4356"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}