{"id":1554,"date":"2011-09-03T18:59:33","date_gmt":"2011-09-03T18:59:33","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1554"},"modified":"2011-09-03T18:59:33","modified_gmt":"2011-09-03T18:59:33","slug":"lecturas-compartidas-en-twitter-agosto-de-2011","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-compartidas-en-twitter-agosto-de-2011\/","title":{"rendered":"Lecturas compartidas en Twitter (Agosto de 2011)"},"content":{"rendered":"

Esta entrada es una recopilaci\u00f3n de lecturas que he compartido en Twitter<\/a>. La recopilaci\u00f3n de los tweets est\u00e1 ordenada seg\u00fan la fecha de su publicaci\u00f3n en Twitter<\/a>.\n<\/p>\n

<\/p>\n

    \n
  1. \nSimply Scheme: Introducing Computer Science<\/a> de B. Harvey y M. Wright.\n<\/li>\n
  2. \nEl problema de los n\u00fameros felices en Haskell y en Maxima<\/a>. #Vestigium\n<\/li>\n
  3. \nIntroducci\u00f3n al c\u00e1lculo simb\u00f3lico con Maxima mediante ejercicios<\/a>. #LibroLibre\n<\/li>\n
  4. \nImperative Programming in Coq<\/a> by Greg Morrisettw. #Coq\n<\/li>\n
  5. \nReasoning about Representations in Autonomous Systems: What Polya and Lakatos have to say<\/a> by Alan Bundy.\n<\/li>\n
  6. \nPeut-on faire des Math\u00e9matiques avec un ordinateur?<\/a> por Ren\u00e9 David. #Historia\n<\/li>\n
  7. \nPeut-on avoir confiance en l’informatique?<\/a> por Ren\u00e9 David y Christophe Raffalli. #Verificacion\n<\/li>\n
  8. \nIntroduction to Machine Learning (An early draft of a proposed textbook)<\/a> by Nils J. Nilsson.\n<\/li>\n
  9. \nThe Theory Behind TheoryMind<\/a>. #Matematicas #Computacion\n<\/li>\n
  10. \nOn why Goodstein sequences should terminate<\/a> by Luke Palmer. #Logica\n<\/li>\n
  11. \nModels in science and technology<\/a> by Wilfrid Hodges.\n<\/li>\n
  12. \nComputability And Incompleteness<\/a> por Errol Martin. #Logica #Computacion\n<\/li>\n
  13. \nUsing a Proof Assistant to Teach Programming Language Foundations<\/a> by Benjamin C. Pierce.\n<\/li>\n
  14. \nRese\u00f1a \u2013 Automated theorem provers: a practical tool for the working mathematician?<\/a> #Vestigium.\n<\/li>\n
  15. \nHow to Write a Proof<\/a> by Leslie Lamport. #Matematicas #Logica\n<\/li>\n
  16. \nIntroducing Logic and Formal Methods with Coq<\/a> by Martin Henz and Aquinas Hobor. #Coq\n<\/li>\n
  17. \nPurely Functional Data Structures<\/a> by Chris Okasaki. #LibroLibre #PF\n<\/li>\n
  18. \nExpresiones aritm\u00e9ticas mediante tipos abstracto de datos y polinomios en Haskell<\/a>. #Vestigium #Haskell #Matematicas\n<\/li>\n
  19. \nF*: A Verifying ML Compiler for Distributed Programming.<\/a>\n<\/li>\n
  20. \nLos principios del programador<\/a>. #Vestigium #Programacion\n<\/li>\n
  21. \nA verified runtime for a verified theorem prover<\/a> by Magnus O. Myreen and Jared Davis. #ACL2 #Lisp\n<\/li>\n
  22. \nFoundations of Mathematics from the Perspective of Computer Mathematics<\/a> by H. Barendregt. #Matematicas #Computacion\n<\/li>\n
  23. \nProofs of Correctness in Mathematics and Industry<\/a> by H. Barendregt.\n<\/li>\n
  24. \nProof Assistants: history, ideas and future<\/a> by H. Geuvers. #ITP\n<\/li>\n
  25. \nChurch\u2019s Thesis and Functional Programming<\/a> by David Turner. #FP\n<\/li>\n
  26. \nAnswer Set Solving in Practice<\/a> by Martin Gebser and Torsten Schaub. #Tutorial\n<\/li>\n
  27. \nmizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library<\/a> by J. Alama #RazonamientoFormalizado\n<\/li>\n
  28. \nThe Principles of Good Programming<\/a> by Christopher Diggins. (via @jneira )\n<\/li>\n
  29. \nAprende a programar en diez a\u00f1os<\/a> por Peter Norvig.\n<\/li>\n
  30. \nTool Support for Refactoring Haskell Programs<\/a>. Ph.D. Thesis, Chris Brown.\n<\/li>\n
  31. \nClone Detection and Elimination for Haskell<\/a> by Christopher Brown and Simon Thompson. #Haskell\n<\/li>\n
  32. \nALPprolog: A New Logic Programming Method for Dynamic Domains<\/a>. #Prolog\n<\/li>\n
  33. \nA Framework for Automated and Certified Refinement Steps<\/a>. #Isabelle\n<\/li>\n
  34. \nIntroduction to Haskell<\/a> by Jerry Cain. #Haskell\n<\/li>\n
  35. \nAutomating Algebraic Methods in Isabelle<\/a>. #IsabelleHOL\n<\/li>\n
  36. \nLe langage math\u00e9matique et les langages de programmation<\/a> por G. Dowek.\n<\/li>\n
  37. \nCategory theory introduction using ML<\/a>. #ML\n<\/li>\n
  38. \nOCaml for Haskellers<\/a> by Edward Z. Yang. #OCaml #Haskell\n<\/li>\n
  39. \nAnd Logic Begat Computer Science: When Giants Roamed the Earth<\/a> by Moshe Vardi. #Logic #CS\n<\/li>\n
  40. \nFrom Philosophical to Industrial Logics<\/a> by Moshe Vardi. #Logica #Computacion\n<\/li>\n
  41. \nWhy Functional Programming Matters<\/a> by John Hughes. #Haskell\n<\/li>\n
  42. \nInteractive Proof: Introduction to Isabelle\/HOL<\/a>. #Isabelle_HOL\n<\/li>\n
  43. \nCoq au vin (The Coq proof assistant and the Curry-Howard correspondence)<\/a>.\n<\/li>\n
  44. \nEnumeraciones de los n\u00fameros racionales en Haskell<\/a>. #Vestigium #Haskell\n<\/li>\n
  45. \nAn Algebraic Specification of the Semantic Web<\/a>. #SW\n<\/li>\n
  46. \nUna cuesti\u00f3n de unos y ceros en Haskell<\/a>. #Vestigium #Haskell #Matematicas\n<\/li>\n
  47. \nTheorem Proving for Verification (the Early Days)<\/a> by J S. Moore. #ATP\n<\/li>\n
  48. \nSelecting Attributes for Sport Forecasting using Formal Concept Analysis<\/a> por @garanda, @jborrego y J. Gal\u00e1n. #FCA\n<\/li>\n
  49. \nReasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving<\/a>. #ATP #SW\n<\/li>\n
  50. \nPara contestar rapidito y casi sin pensar<\/a>. #Vestigium #Haskell #Matematicas\n<\/li>\n
  51. \nFormal methods: Practice and Experience<\/a> por J. Woodcock et als. #FM\n<\/li>\n
  52. \nAutomated deduction for verification<\/a> por N. Shankar. #ATP\n<\/li>\n
  53. \nSoftware model checking<\/a> por R. Jhala y R. Majumdar. #MC\n<\/li>\n
  54. \nThe verified software initiative: A Manifesto<\/a>. por C.A.R. Hoare, J. Misra, G.T. Leavens y N. Shankar. #FM\n<\/li>\n
  55. \nCodificaci\u00f3n de Huffman en Haskell<\/a>. #Vestigium #Haskell #QuickCheck\n<\/li>\n
  56. \nTesting in Haskell: an introduction to HUnit and QuickCheck<\/a> by Mark P Jones.\n<\/li>\n
  57. \nEngineering Large Projects in Haskell: A Decade of FP at Galois<\/a>. #Haskell\n<\/li>\n
  58. \nSoftware Foundations<\/a> by Benjamin Peirce. #Coq\n<\/li>\n
  59. \nIntroducci\u00f3n a la l\u00f3gica mediante la l\u00f3gica aristot\u00e9lica y el sistema de razonamiento Coq<\/a>. #Logica #Coq\n<\/li>\n
  60. \nIntroducci\u00f3n a las definiciones de conjuntos inductivos en Java y en Coq<\/a>.\n<\/li>\n
  61. \nIntroducci\u00f3n a la l\u00f3gica proposicional usando el sistema de razonamiento Coq<\/a>.\n<\/li>\n
  62. \nType Theory and Functional Programming<\/a> by Simon Thompson. #LibroLibre\n<\/li>\n
  63. \nProceedings of the First Workshop on Automated Theory Engineering<\/a>. #ATP\n<\/li>\n
  64. \nTesting as a Certification Approach<\/a> by Alberto Sim\u00f5es , Nuno Carvalho and Jos\u00e9 Jo\u00e3o Almeida. #TDD #Perl\n<\/li>\n
  65. \nA Very General Method of Computing Shortest Paths<\/a> by Russell O\u2019Connor.\n<\/li>\n
  66. \nSemantics with Applications: A Formal Introduction<\/a> by Hanne Riis Nielson and Flemming Nielson. #LibroLibre\n<\/li>\n
  67. \nAutomated Proving in Geometry using Gr\u00f6bner Bases in Isabelle\/HOL<\/a> by Danijela Petrovi\u0107. #Isabelle\n<\/li>\n
  68. \nGeometry Constructions Language<\/a> by Predrag Jani\u010di\u0107. #Dynamic_geometry\n<\/li>\n
  69. \nImperative Functional Programming with Isabelle\/HOL<\/a>. #Formal_verification\n<\/li>\n
  70. \nAn Excursion Into the Proofs-as-programs Correspondence<\/a> by Hugo Herbelin.\n<\/li>\n
  71. \nAutomated reasoning about retrograde chess problems using Coq<\/a> by Marko Malikovi\u0107. #Coq\n<\/li>\n
  72. \nFormal Verication of Key Properties for Several Probability Logics in the Proof Assistant Coq<\/a> by Petar Maksimovi\u0107. #Coq\n<\/li>\n
  73. \nIntegrating Isabelle\/HOL And Functional Programming – Current Trends<\/a> by Florian Haftmann. #Haskell #Isabelle\n<\/li>\n
  74. \nEl problema de la igualdad de los bordes de los \u00e1rboles binarios (sameFringe)<\/a>. #LogicaMente #Haskell #Lisp #Maxima\n<\/li>\n
  75. \nIntegrating Testing and Interactive Theorem Proving<\/a> by H. R. Chamarthi et als. #Formal_verification #Testing #ACL2\n<\/li>\n
  76. \nA Flexible Formal Verification Framework for Industrial Scale Validation<\/a>.\n<\/li>\n
  77. \nEfficient Interactive Construction of Machine-Checked Protocol Security Proofs<\/a>. #IsabelleHOL\n<\/li>\n
  78. \nProofs and Types<\/a> by Jean-Yves Girard, Yves Lafont and Paul Taylor.\n<\/li>\n
  79. \nUse of Formal Verification at Centaur Technology<\/a>. #Formal_verification #ACL2\n<\/li>\n
  80. \nVerification of the Completeness of Unification Algorithms \u00e0 la Robinson<\/a>.\n<\/li>\n
  81. \nTowards Flight Control Verification Using Automated Theorem Proving<\/a>. #PVS\n<\/li>\n
  82. \nOtt: Effective tool support for the working semanticist<\/a>. #IsabelleHOL #Coq\n<\/li>\n
  83. \nModelling and verifying algorithms in Coq: an introduction<\/a>. #Coq\n<\/li>\n
  84. \nLem, a tool for lightweight executable mathematics<\/a>. #Coq #IsabelleHOL #HOL4\n<\/li>\n
  85. \nVerifying SAT and SMT in Coq for a fully automated decision procedure<\/a>. #Coq\n<\/li>\n
  86. \nInductive Programming (A Survey of Program Synthesis Techniques)<\/a> by E. Kitzelmann. #Program_synthesis\n<\/li>\n
  87. \nA deductive approach to program synthesis<\/a> by Z. Manna y R. Waldinger.\n<\/li>\n
  88. \nInductive Synthesis of Functional Programs: An Explanation Based Generalization Approach<\/a> by E. Kitzelmann & U. Schmid. #Program_synthesis\n<\/li>\n
  89. \nGeneraci\u00f3n autom\u00e1tica de programas a partir de ejemplos (FOIL y PROGOL)<\/a>. #PLI\n<\/li>\n
  90. \nAn Introduction to Progol (Inductive Logic Programming)<\/a> by S. Roberts. #ILP\n<\/li>\n
  91. \nInductive Logic Programming (Techniques and Applications)<\/a> by Nada Lavrac and Saso Dzeroski. #ILP #LibroLibre\n<\/li>\n
  92. \nApproaches to Automatic Programming<\/a>. #Automatic_programming\n<\/li>\n
  93. \nLearn Prolog Now!<\/a>. #Prolog #LibroLibre\n<\/li>\n
  94. \nProlog for Software Engineering<\/a>. #Prolog\n<\/li>\n
  95. \nIntroduction to Prolog for Mathematicians<\/a>. #Prolog\n<\/li>\n
  96. \nA Logical Zoo: Interesting Fallacious Mathematical Arguments<\/a>. #Falacias\n<\/li>\n
  97. \nVerification of Certifying Computations<\/a>. #Isabelle_HOL #VCC #LEDA\n<\/li>\n
  98. \nVCC : A mechanical verifier for concurrent C programs<\/a>. #VCC\n<\/li>\n
  99. \nLet Over Lambda\u201450 Years of Lisp<\/a> by Doug Hoyte. #LibroLibre #Lisp\n<\/li>\n
  100. \nProlog programming in depth<\/a>. #Prolog\n<\/li>\n
  101. \nFrom Logic Programming to Prolog<\/a> by K.R. Apt #Prolog #LibroLibre\n<\/li>\n
  102. \n\u00bfQu\u00e9 tiene que ver el n\u00famero e con los n\u00fameros primos?<\/a>. #LogicaMente #Haskell\n<\/li>\n
  103. \nCertified programming with dependent types (Because the future of defense is liberal application of math)<\/a>. #Coq\n<\/li>\n
  104. \nVentajas de la pereza en el problema de los k menores elementos<\/a>. #LogicaMente\n<\/li>\n
  105. \nLa funci\u00f3n de Takeuchi como banco de prueba para la eficiencia<\/a>. #LogicaMente\n<\/li>\n
  106. \nAutomated Deduction and its Application to Mathematics<\/a>. #Mathematics\n<\/li>\n
  107. \nEl problema de la mayor subsucesi\u00f3n creciente en Haskell y en Clojure<\/a>.\n<\/li>\n
  108. \nEl problema del cruce de listas en Haskell, Clojure, Common_Lisp, Maxima y Prolog<\/a>. #LogicaMente #Haskell, #Clojure, #Common_Lisp, #Maxima y #Prolog\n<\/li>\n
  109. \nGauss-Jordan Elimination for Matrices Represented as Functions<\/a> by Tobias Nipkow. #IsabelleHOL\n<\/li>\n
  110. \nDependent Types at Work<\/a> by Ana Bove and Peter Dybjer. #Matematicas\n<\/li>\n
  111. \nBK-Trees in Haskell<\/a>. #Haskell #Matematicas (via @joseanpg)\n<\/li>\n
  112. \nCategorical programming with inductive and coinductive types<\/a>. by V. Vene.\n<\/li>\n
  113. \nSeven Myths of Formal Methods<\/a> by Anthony Hall. (via @Math_Bits)\n<\/li>\n
  114. \nCrash Course in Monads<\/a> by Vlad Patryshev (via @ajlopez)\n<\/li>\n
  115. \nVerification of Dependable Software using Spark and Isabelle<\/a> by Stefan Berghofer. #Isabelle_HOL\n<\/li>\n
  116. \nAn Overview of Ciao<\/a> by M. Hermenegildo at als. #Ciao #Prolog\n<\/li>\n
  117. \nUsing Answer Set Programming for Representing and Reasoning with Preferences and Uncertainty in Dynamic Domains<\/a>. #ASP\n<\/li>\n
  118. \nVerification of Programs in Virtual Memory Using Separation Logic<\/a> (PhD Thesis) by Rafal Kolanski. #IsabelleHOL\n<\/li>\n
  119. \nAutomated Specification Analysis Using an Interactive Theorem Prover<\/a> H.R. Chamarti & P. Manolios. #ACL2\n<\/li>\n
  120. \nThe First 10 Prolog Programming Contest<\/a>. #Prolog #LibroLibre (via @EtnasSoft)\n<\/li>\n
  121. \nSorting Morphisms<\/a> by Lex Augusteijn #Haskell\n<\/li>\n
  122. \nTutorial de Lisp de Conrad Barski adaptado a Clojure por Wei-Ju Wu<\/a> #Clojure\n<\/li>\n
  123. \nAutomated Error Localization and Correction for Imperative Programs<\/a>by R. Koenighofer and R. Bloem. #Verification #SMT\n<\/li>\n
  124. \nFormal Analysis of Fractional Order Systems in HOL<\/a>. #HOL\n<\/li>\n
  125. \nFormalization of Abstract State Transition Systems for SAT<\/a> by Filip Mari\u0107 & Predrag Jani\u010di\u0107. #IsabelleHOL\n<\/li>\n
  126. \nCoquet: a Coq library for verifying hardware<\/a> by Thomas Braibant.\n<\/li>\n
  127. \nA short introduction to Clojure<\/a> by Matthias N\u00fc\u00dfler #Clojure\n<\/li>\n
  128. \nEl problema de los n\u00fameros felices en Haskell y en Maxima<\/a>. #LogicaMente\n<\/li>\n
  129. \nA tutorial on the universality and expressiveness of fold<\/a> by Graham Hutton\n<\/li>\n
  130. \nSistemas l\u00f3gicos proposicionales en Prolog<\/a>. #Prolog #Logica #LibroLibre\n<\/li>\n
  131. \nComputing with Logic as Operator Elimination: The ToyElim System<\/a> by Christoph\n<\/li>\n
  132. \nFormal Verification for Numerical Methods<\/a>. #Tesis #Razonamiento_formalizado\n<\/li>\n
  133. \nCertified Programming with Dependent Types<\/a> by Adam Chlipala. #ITP #Coq\n<\/li>\n
  134. \nMenor elemento com\u00fan en listas infinitas ordenadas en Haskell y en Clojure<\/a>.\n<\/li>\n
  135. \nModelado algebraico de tipos de datos recursivos<\/a>. #Haskell (via @joseanpg)\n<\/li>\n
  136. \nFunctional programming<\/a> by Olaf Chitil. #Haskell\n<\/li>\n
  137. \nYoda: a simple tool for natural deduction<\/a>. #Logica\n<\/li>\n
  138. \nCan a machine know that it is a machine?<\/a> #Logic #AI\n<\/li>\n
  139. \nSatisfiability at Microsoft<\/a> by Leonardo de Moura. #Logic\n<\/li>\n
  140. \nHCAS: Haskell Computer Algebra System<\/a> by Rob Tougher. #Haskell #CAS\n<\/li>\n
  141. \nEl tipo abstracto de datos de las tablas en Haskell<\/a>. #Vestigium #Haskell\n<\/li>\n
  142. \nEl tipo abstracto de datos de los \u00e1rboles binarios de b\u00fasqueda en Haskell<\/a>.\n<\/li>\n
  143. \nPropositional Consequence Relations and Algebraic Logic<\/a> by Ramon Jansana\n<\/li>\n
  144. \nWhy Functional Programming Matters<\/a>. (via @dr_chaieb)\n<\/li>\n
  145. \nAesthetics for the Working Mathematician<\/a>. #Math (via @MathUpdate)\n<\/li>\n
  146. \nEl tipo abstracto de datos de los mont\u00edculos en Haskell<\/a>. #Vestigium #Haskell\n<\/li>\n
  147. \nFeasibility via quantifier elimination II<\/a> by Rod Carvalho. #Math\n<\/li>\n
  148. \nWho Killed Prolog?<\/a> by Maarten van Emden. #Prolog\n<\/li>\n
  149. \nProlog\u2019s Death<\/a> by Andre Vellino. #Prolog #Logic_programming #History\n<\/li>\n
  150. \nA survey on Interactive Theorem Proving<\/a> by Andrea Asperti #ITP #Math\n<\/li>\n
  151. \nEjercicios de programaci\u00f3n funcional con Haskell (Pon a prueba tus habilidades!)<\/a>. #Haskell (via @EtnasSoft)\n<\/li>\n
  152. \n\u00a1Aprende #Haskell por el bien de todos!<\/a>. #Haskell #LibroLibre\n<\/li>\n
  153. \nPerformance and Evaluation of Lisp Systems<\/a> by Richard P. Gabriel #Lisp\n<\/li>\n
  154. \nRecorridos de grafos en Haskell<\/a>. #Vestigium #Haskell\n<\/li>\n
  155. \nConstructive Computation Theory: an executable course from Gerard Huet<\/a>. #ML (via @psnively)\n<\/li>\n<\/ol>\n","protected":false},"excerpt":{"rendered":"

    Esta entrada es una recopilaci\u00f3n de lecturas que he compartido en Twitter. La recopilaci\u00f3n de los tweets est\u00e1 ordenada seg\u00fan la fecha de su publicaci\u00f3n en Twitter.<\/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":[177],"tags":[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\/1554"}],"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=1554"}],"version-history":[{"count":5,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1554\/revisions"}],"predecessor-version":[{"id":1559,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1554\/revisions\/1559"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1554"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1554"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1554"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}