{"id":2383,"date":"2012-12-03T06:39:26","date_gmt":"2012-12-03T06:39:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=2383"},"modified":"2013-03-08T05:47:37","modified_gmt":"2013-03-08T05:47:37","slug":"lecturas-del-grupo-de-logica-computacional-septiembre-noviembre-de-2012","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-del-grupo-de-logica-computacional-septiembre-noviembre-de-2012\/","title":{"rendered":"Lecturas del Grupo de L\u00f3gica Computacional (Septiembre-Noviembre de 2012)"},"content":{"rendered":"

Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional<\/a> desde el mes de septiembre de 2012. La anterior recopilaci\u00f3n fue la de agosto de 2012<\/a>.\n<\/p>\n

\nLa recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista. Al final de cada art\u00edculo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.\n<\/p>\n

    \n
  1. \nOperational refinement for compiler correctness<\/a>. #Tesis #Coq\n<\/li>\n
  2. \nInteractive and automated proofs for graph transformations<\/a>. #Isabelle\n<\/li>\n
  3. \nLecturas del Grupo de L\u00f3gica Computacional (Marzo-Agosto de 2012)<\/a>\n<\/li>\n
  4. \nPiensa en Haskell (Ejercicios de programaci\u00f3n funcional con Haskell)<\/a>. #Haskell\n<\/li>\n
  5. \n\u00bfComputadores von Neumann, o computadores Turing?<\/a> #Historia\n<\/li>\n
  6. \nFormalizing Frankl’s conjecture: FC-families<\/a>. #Isabelle\n<\/li>\n
  7. \nImplementing an efficient theorem prover<\/a>. #Tesis #Vampire\n<\/li>\n
  8. \nSystem of logic based on ordinals<\/a>. #Tesis #Historia\n<\/li>\n
  9. \nProving concurrent noninterference<\/a> (c\u00f3digo<\/a>) #Isabelle\n<\/li>\n
  10. \nImproving real analysis in Coq: a user-friendly approach to integrals and derivatives<\/a>. #Coq (CPP2012<\/a>)\n<\/li>\n
  11. \nComputing persistent homology within Coq\/SSReflect<\/a>. #Coq\n<\/li>\n
  12. \nSoftware libre para una sociedad libre<\/a>. #Libro #Pensamiento\n<\/li>\n
  13. \nA formal proof of Sasaki-Murao algorithm<\/a>. #Coq (MAP2012<\/a>, code<\/a>, Presentaci\u00f3n<\/a>).\n<\/li>\n
  14. \nConfluence by decreasing diagrams formalized<\/a>. #Isabelle\n<\/li>\n
  15. \nProof Pearl \u2013 A mechanized proof of GHC\u2019s mergesort<\/a>. #Isabelle #Haskell\n<\/li>\n
  16. \nA logic-algebraic approach to decision taking in a railway interlocking system<\/a>. #BG\n<\/li>\n
  17. \nScheme in industrial automation<\/a>. #Scheme\n<\/li>\n
  18. \nParallelizing an interactive theorem prover: Functional programming and proofs with ACL2<\/a>. #ACL2 #Tesis\n<\/li>\n
  19. \nA string of pearls: Proofs of Fermat\u2019s little theorem<\/a>. #HOL4\n<\/li>\n
  20. \nA formally-verified C compiler supporting floating-point arithmetic<\/a>. #Coq\n<\/li>\n
  21. \nThe Boyer-Moore waterfall model revisited<\/a>. #HOL_Light\n<\/li>\n
  22. \nA Python pattern matcher project for an introduction to Artificial Intelligence course<\/a>. #IA\n<\/li>\n
  23. \nInformatik 2: Functional Programming<\/a>. #Haskell\n<\/li>\n
  24. \nContributions to the formal verification of arithmetic algorithms<\/a>. #Tesis #Coq\n<\/li>\n
  25. \nWhy learn Haskell?<\/a>. #Tutorial #Haskell\n<\/li>\n
  26. \nA mechanical verification of the independence of Tarski’s euclidean axiom<\/a> y c\u00f3digo<\/a> #Tesina #Isabelle\n<\/li>\n
  27. \nWeak completeness theorem for propositional linear time temporal logic<\/a>. #Mizar\n<\/li>\n
  28. \nNatural language processing for the working programmer<\/a>. #Haskell #IA\n<\/li>\n
  29. \nNexus authorization logic (NAL): Logical results<\/a>. #Coq\n<\/li>\n
  30. \nReasons for studying Haskell in University<\/a>. #Haskell\n<\/li>\n
  31. \nConstructive completeness for modal logic with transitive closure<\/a>. #Coq #Modal\n<\/li>\n
  32. \nA functional programming approach to AI search algorithms<\/a>. #IA #PF\n<\/li>\n
  33. \nDual multi-adjoint concept lattices<\/a>. #AFC\n<\/li>\n
  34. \nTemas de “Demostraci\u00f3n asistida por ordenador”<\/a>. #Isabelle #Tutorial\n<\/li>\n
  35. \nVerificaci\u00f3n de programas: Introducci\u00f3n<\/a>. #Verificaci\u00f3n\n<\/li>\n
  36. \n\u00daltimo d\u00edgito del producto de n\u00fameros de Fermat<\/a>. #Haskell #IMO\n<\/li>\n
  37. \nA formal proof of square root and division elimination in embedded programs<\/a>. #PVS\n<\/li>\n
  38. \nCoq et caract\u00e8res (Preuve formelle du th\u00e9or\u00e8me de Feit et Thompson)<\/a>. #Coq #Divulgaci\u00f3n\n<\/li>\n
  39. \nFormalized algebraic numbers: construction and first order theory<\/a>. #Tesis #Coq\n<\/li>\n
  40. \nHow enterprises use functional languages, and why they don’t<\/a>. #PF\n<\/li>\n
  41. \nInductive analysis of security protocols in Isabelle\/HOL with applications to electronic voting<\/a>. #Tesis #Isabelle\n<\/li>\n
  42. \nConstructive formalization of regular languages<\/a>. #Tesina #Coq\n<\/li>\n
  43. \nComputing with free algebras<\/a>. #Haskell\n<\/li>\n
  44. \nAsk-Elle: a Haskell Tutor<\/a>. #Tesis #Haskell #TI\n<\/li>\n
  45. \nUsing Isabelle to verify special relativity, with application to hypercomputation theory<\/a>. #Isabelle<\/p>\n<\/li>\n<\/ol>\n

    En Mendeley tambi\u00e9n se encuentran las lecturas del Grupo de L\u00f3gica Computacional<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"

    Esta entrada es una recopilaci\u00f3n de lecturas compartidas en la lista de correo del grupo de l\u00f3gica computacional desde el mes de septiembre de 2012. La anterior recopilaci\u00f3n fue la de agosto de 2012. La recopilaci\u00f3n est\u00e1 ordenada por la fecha de su publicaci\u00f3n en la lista. Al final de cada art\u00edculo se encuentra etiquetas…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[177],"tags":[178,292],"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\/2383"}],"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=2383"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2383\/revisions"}],"predecessor-version":[{"id":2733,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/2383\/revisions\/2733"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=2383"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=2383"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=2383"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}