{"id":4709,"date":"2015-01-09T08:30:17","date_gmt":"2015-01-09T07:30:17","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4709"},"modified":"2015-01-09T08:31:05","modified_gmt":"2015-01-09T07:31:05","slug":"resena-relative-monads-formalised","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-relative-monads-formalised\/","title":{"rendered":"Rese\u00f1a: Relative monads formalised"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Agda titulado <a href=\"\">Relative monads formalised<\/a><\/p>\n<p>Sus autores son<\/p>\n<ul>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~txa\/\">Thorsten Altenkirch<\/a> (del <a href=\"http:\/\/fp.cs.nott.ac.uk\/\">Functional Programming Laboratory<\/a> en la Univ. de Nottingham, Inglaterra).<\/li>\n<li><a href=\"http:\/\/cs.ioc.ee\/~james\">James Chapman<\/a> (del <a href=\"http:\/\/cs.ioc.ee\/lsg\">Logic and semantics group<\/a> en la Univ. T\u00e9cnica de Tallin, Estonia) y<\/li>\n<li><a href=\"http:\/\/www.ioc.ee\/~tarmo\">Tarmo Uustalu<\/a> (del <a href=\"http:\/\/cs.ioc.ee\/lsg\">Logic and semantics group<\/a> en la Univ. T\u00e9cnica de Tallin, Estonia).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comprises the requisite basic category theory, the central concepts of the theory of relative monads and adjunctions, which are compared to their ordinary counterparts, and two running examples from programming theory.\n<\/p><\/blockquote>\n<p>El trabajo se ha publicado en el <a href=\"http:\/\/jfr.unibo.it\/article\/view\/4389\">Journal of Fromalized Reasoning<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Agda se encuentra <a href=\"http:\/\/cs.ioc.ee\/~james\/relmon.html\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Agda titulado Relative monads formalised Sus autores son Thorsten Altenkirch (del Functional Programming Laboratory en la Univ. de Nottingham, Inglaterra). James Chapman (del Logic and semantics group en la Univ. T\u00e9cnica de Tallin, Estonia) y Tarmo Uustalu (del Logic and semantics group en la Univ. T\u00e9cnica&#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":[1],"tags":[195,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\/4709"}],"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=4709"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4709\/revisions"}],"predecessor-version":[{"id":4711,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4709\/revisions\/4711"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4709"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4709"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4709"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}