{"id":3896,"date":"2013-12-07T17:00:29","date_gmt":"2013-12-07T16:00:29","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3896"},"modified":"2013-12-07T07:39:49","modified_gmt":"2013-12-07T06:39:49","slug":"concrete-semantics-a-proof-assistant-approach","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/concrete-semantics-a-proof-assistant-approach\/","title":{"rendered":"Concrete semantics (A proof assistant approach)"},"content":{"rendered":"<p>Se ha publicado un libro de razonamiento formalizado en <a href=\"http:\/\/isabelle.in.tum.de\/\">Isabelle\/HOL<\/a> sobre sem\u00e1ntica de lenguajes de programaci\u00f3n titulado <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/Concrete-Semantics\/index.html\">Concrete semantics (A proof assistant approach)<\/a>.<\/p>\n<p>Sus autores son <\/p>\n<ul>\n<li> <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/\">Tobias Nipkow<\/a> (de la Univ. T\u00e9cnica de Munich, Alemania) y\n<li> <a href=\"http:\/\/www.cse.unsw.edu.au\/~kleing\">Gerwin Klein<\/a> (del NICTA, Australia).\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>\nThe book Concrete Semantics introduces semantics of programming languages through the medium of a proof assistant. The first part of the book is an introduction to the proof assistant Isabelle. The second part is an introduction to operational semantics and its applications and is based on a simple imperative programming language.\n<\/p><\/blockquote>\n<p>El c\u00f3digo de las correspondientes teor\u00edas en Isabelle se encuentra <a href=\"http:\/\/www21.in.tum.de\/~nipkow\/Concrete-Semantics\/theories.html\">aqu\u00ed<\/a>. <\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un libro de razonamiento formalizado en Isabelle\/HOL sobre sem\u00e1ntica de lenguajes de programaci\u00f3n titulado Concrete semantics (A proof assistant approach). Sus autores son Tobias Nipkow (de la Univ. T\u00e9cnica de Munich, Alemania) y Gerwin Klein (del NICTA, Australia). Su resumen es The book Concrete Semantics introduces semantics of programming languages through the&#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":[229,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\/3896"}],"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=3896"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3896\/revisions"}],"predecessor-version":[{"id":3898,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3896\/revisions\/3898"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3896"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3896"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3896"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}