Lecturas compartidas en Twitter (Agosto de 2011)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas que he compartido en Twitter. La recopilación de los tweets está ordenada según la fecha de su publicación en Twitter.

  1. Simply Scheme: Introducing Computer Science de B. Harvey y M. Wright.
  2. El problema de los números felices en Haskell y en Maxima. #Vestigium
  3. Introducción al cálculo simbólico con Maxima mediante ejercicios. #LibroLibre
  4. Imperative Programming in Coq by Greg Morrisettw. #Coq
  5. Reasoning about Representations in Autonomous Systems: What Polya and Lakatos have to say by Alan Bundy.
  6. Peut-on faire des Mathématiques avec un ordinateur? por René David. #Historia
  7. Peut-on avoir confiance en l’informatique? por René David y Christophe Raffalli. #Verificacion
  8. Introduction to Machine Learning (An early draft of a proposed textbook) by Nils J. Nilsson.
  9. The Theory Behind TheoryMind. #Matematicas #Computacion
  10. On why Goodstein sequences should terminate by Luke Palmer. #Logica
  11. Models in science and technology by Wilfrid Hodges.
  12. Computability And Incompleteness por Errol Martin. #Logica #Computacion
  13. Using a Proof Assistant to Teach Programming Language Foundations by Benjamin C. Pierce.
  14. Reseña – Automated theorem provers: a practical tool for the working mathematician? #Vestigium.
  15. How to Write a Proof by Leslie Lamport. #Matematicas #Logica
  16. Introducing Logic and Formal Methods with Coq by Martin Henz and Aquinas Hobor. #Coq
  17. Purely Functional Data Structures by Chris Okasaki. #LibroLibre #PF
  18. Expresiones aritméticas mediante tipos abstracto de datos y polinomios en Haskell. #Vestigium #Haskell #Matematicas
  19. F*: A Verifying ML Compiler for Distributed Programming.
  20. Los principios del programador. #Vestigium #Programacion
  21. A verified runtime for a verified theorem prover by Magnus O. Myreen and Jared Davis. #ACL2 #Lisp
  22. Foundations of Mathematics from the Perspective of Computer Mathematics by H. Barendregt. #Matematicas #Computacion
  23. Proofs of Correctness in Mathematics and Industry by H. Barendregt.
  24. Proof Assistants: history, ideas and future by H. Geuvers. #ITP
  25. Church’s Thesis and Functional Programming by David Turner. #FP
  26. Answer Set Solving in Practice by Martin Gebser and Torsten Schaub. #Tutorial
  27. mizar-items: Exploring fine-grained dependencies in the Mizar Mathematical Library by J. Alama #RazonamientoFormalizado
  28. The Principles of Good Programming by Christopher Diggins. (via @jneira )
  29. Aprende a programar en diez años por Peter Norvig.
  30. Tool Support for Refactoring Haskell Programs. Ph.D. Thesis, Chris Brown.
  31. Clone Detection and Elimination for Haskell by Christopher Brown and Simon Thompson. #Haskell
  32. ALPprolog: A New Logic Programming Method for Dynamic Domains. #Prolog
  33. A Framework for Automated and Certified Refinement Steps. #Isabelle
  34. Introduction to Haskell by Jerry Cain. #Haskell
  35. Automating Algebraic Methods in Isabelle. #IsabelleHOL
  36. Le langage mathématique et les langages de programmation por G. Dowek.
  37. Category theory introduction using ML. #ML
  38. OCaml for Haskellers by Edward Z. Yang. #OCaml #Haskell
  39. And Logic Begat Computer Science: When Giants Roamed the Earth by Moshe Vardi. #Logic #CS
  40. From Philosophical to Industrial Logics by Moshe Vardi. #Logica #Computacion
  41. Why Functional Programming Matters by John Hughes. #Haskell
  42. Interactive Proof: Introduction to Isabelle/HOL. #Isabelle_HOL
  43. Coq au vin (The Coq proof assistant and the Curry-Howard correspondence).
  44. Enumeraciones de los números racionales en Haskell. #Vestigium #Haskell
  45. An Algebraic Specification of the Semantic Web. #SW
  46. Una cuestión de unos y ceros en Haskell. #Vestigium #Haskell #Matematicas
  47. Theorem Proving for Verification (the Early Days) by J S. Moore. #ATP
  48. Selecting Attributes for Sport Forecasting using Formal Concept Analysis por @garanda, @jborrego y J. Galán. #FCA
  49. Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving. #ATP #SW
  50. Para contestar rapidito y casi sin pensar. #Vestigium #Haskell #Matematicas
  51. Formal methods: Practice and Experience por J. Woodcock et als. #FM
  52. Automated deduction for verification por N. Shankar. #ATP
  53. Software model checking por R. Jhala y R. Majumdar. #MC
  54. The verified software initiative: A Manifesto. por C.A.R. Hoare, J. Misra, G.T. Leavens y N. Shankar. #FM
  55. Codificación de Huffman en Haskell. #Vestigium #Haskell #QuickCheck
  56. Testing in Haskell: an introduction to HUnit and QuickCheck by Mark P Jones.
  57. Engineering Large Projects in Haskell: A Decade of FP at Galois. #Haskell
  58. Software Foundations by Benjamin Peirce. #Coq
  59. Introducción a la lógica mediante la lógica aristotélica y el sistema de razonamiento Coq. #Logica #Coq
  60. Introducción a las definiciones de conjuntos inductivos en Java y en Coq.
  61. Introducción a la lógica proposicional usando el sistema de razonamiento Coq.
  62. Type Theory and Functional Programming by Simon Thompson. #LibroLibre
  63. Proceedings of the First Workshop on Automated Theory Engineering. #ATP
  64. Testing as a Certification Approach by Alberto Simões , Nuno Carvalho and José João Almeida. #TDD #Perl
  65. A Very General Method of Computing Shortest Paths by Russell O’Connor.
  66. Semantics with Applications: A Formal Introduction by Hanne Riis Nielson and Flemming Nielson. #LibroLibre
  67. Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL by Danijela Petrović. #Isabelle
  68. Geometry Constructions Language by Predrag Janičić. #Dynamic_geometry
  69. Imperative Functional Programming with Isabelle/HOL. #Formal_verification
  70. An Excursion Into the Proofs-as-programs Correspondence by Hugo Herbelin.
  71. Automated reasoning about retrograde chess problems using Coq by Marko Maliković. #Coq
  72. Formal Verication of Key Properties for Several Probability Logics in the Proof Assistant Coq by Petar Maksimović. #Coq
  73. Integrating Isabelle/HOL And Functional Programming – Current Trends by Florian Haftmann. #Haskell #Isabelle
  74. El problema de la igualdad de los bordes de los árboles binarios (sameFringe). #LogicaMente #Haskell #Lisp #Maxima
  75. Integrating Testing and Interactive Theorem Proving by H. R. Chamarthi et als. #Formal_verification #Testing #ACL2
  76. A Flexible Formal Verification Framework for Industrial Scale Validation.
  77. Efficient Interactive Construction of Machine-Checked Protocol Security Proofs. #IsabelleHOL
  78. Proofs and Types by Jean-Yves Girard, Yves Lafont and Paul Taylor.
  79. Use of Formal Verification at Centaur Technology. #Formal_verification #ACL2
  80. Verification of the Completeness of Unification Algorithms à la Robinson.
  81. Towards Flight Control Verification Using Automated Theorem Proving. #PVS
  82. Ott: Effective tool support for the working semanticist. #IsabelleHOL #Coq
  83. Modelling and verifying algorithms in Coq: an introduction. #Coq
  84. Lem, a tool for lightweight executable mathematics. #Coq #IsabelleHOL #HOL4
  85. Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq
  86. Inductive Programming (A Survey of Program Synthesis Techniques) by E. Kitzelmann. #Program_synthesis
  87. A deductive approach to program synthesis by Z. Manna y R. Waldinger.
  88. Inductive Synthesis of Functional Programs: An Explanation Based Generalization Approach by E. Kitzelmann & U. Schmid. #Program_synthesis
  89. Generación automática de programas a partir de ejemplos (FOIL y PROGOL). #PLI
  90. An Introduction to Progol (Inductive Logic Programming) by S. Roberts. #ILP
  91. Inductive Logic Programming (Techniques and Applications) by Nada Lavrac and Saso Dzeroski. #ILP #LibroLibre
  92. Approaches to Automatic Programming. #Automatic_programming
  93. Learn Prolog Now!. #Prolog #LibroLibre
  94. Prolog for Software Engineering. #Prolog
  95. Introduction to Prolog for Mathematicians. #Prolog
  96. A Logical Zoo: Interesting Fallacious Mathematical Arguments. #Falacias
  97. Verification of Certifying Computations. #Isabelle_HOL #VCC #LEDA
  98. VCC : A mechanical verifier for concurrent C programs. #VCC
  99. Let Over Lambda—50 Years of Lisp by Doug Hoyte. #LibroLibre #Lisp
  100. Prolog programming in depth. #Prolog
  101. From Logic Programming to Prolog by K.R. Apt #Prolog #LibroLibre
  102. ¿Qué tiene que ver el número e con los números primos?. #LogicaMente #Haskell
  103. Certified programming with dependent types (Because the future of defense is liberal application of math). #Coq
  104. Ventajas de la pereza en el problema de los k menores elementos. #LogicaMente
  105. La función de Takeuchi como banco de prueba para la eficiencia. #LogicaMente
  106. Automated Deduction and its Application to Mathematics. #Mathematics
  107. El problema de la mayor subsucesión creciente en Haskell y en Clojure.
  108. El problema del cruce de listas en Haskell, Clojure, Common_Lisp, Maxima y Prolog. #LogicaMente #Haskell, #Clojure, #Common_Lisp, #Maxima y #Prolog
  109. Gauss-Jordan Elimination for Matrices Represented as Functions by Tobias Nipkow. #IsabelleHOL
  110. Dependent Types at Work by Ana Bove and Peter Dybjer. #Matematicas
  111. BK-Trees in Haskell. #Haskell #Matematicas (via @joseanpg)
  112. Categorical programming with inductive and coinductive types. by V. Vene.
  113. Seven Myths of Formal Methods by Anthony Hall. (via @Math_Bits)
  114. Crash Course in Monads by Vlad Patryshev (via @ajlopez)
  115. Verification of Dependable Software using Spark and Isabelle by Stefan Berghofer. #Isabelle_HOL
  116. An Overview of Ciao by M. Hermenegildo at als. #Ciao #Prolog
  117. Using Answer Set Programming for Representing and Reasoning with Preferences and Uncertainty in Dynamic Domains. #ASP
  118. Verification of Programs in Virtual Memory Using Separation Logic (PhD Thesis) by Rafal Kolanski. #IsabelleHOL
  119. Automated Specification Analysis Using an Interactive Theorem Prover H.R. Chamarti & P. Manolios. #ACL2
  120. The First 10 Prolog Programming Contest. #Prolog #LibroLibre (via @EtnasSoft)
  121. Sorting Morphisms by Lex Augusteijn #Haskell
  122. Tutorial de Lisp de Conrad Barski adaptado a Clojure por Wei-Ju Wu #Clojure
  123. Automated Error Localization and Correction for Imperative Programsby R. Koenighofer and R. Bloem. #Verification #SMT
  124. Formal Analysis of Fractional Order Systems in HOL. #HOL
  125. Formalization of Abstract State Transition Systems for SAT by Filip Marić & Predrag Janičić. #IsabelleHOL
  126. Coquet: a Coq library for verifying hardware by Thomas Braibant.
  127. A short introduction to Clojure by Matthias Nüßler #Clojure
  128. El problema de los números felices en Haskell y en Maxima. #LogicaMente
  129. A tutorial on the universality and expressiveness of fold by Graham Hutton
  130. Sistemas lógicos proposicionales en Prolog. #Prolog #Logica #LibroLibre
  131. Computing with Logic as Operator Elimination: The ToyElim System by Christoph
  132. Formal Verification for Numerical Methods. #Tesis #Razonamiento_formalizado
  133. Certified Programming with Dependent Types by Adam Chlipala. #ITP #Coq
  134. Menor elemento común en listas infinitas ordenadas en Haskell y en Clojure.
  135. Modelado algebraico de tipos de datos recursivos. #Haskell (via @joseanpg)
  136. Functional programming by Olaf Chitil. #Haskell
  137. Yoda: a simple tool for natural deduction. #Logica
  138. Can a machine know that it is a machine? #Logic #AI
  139. Satisfiability at Microsoft by Leonardo de Moura. #Logic
  140. HCAS: Haskell Computer Algebra System by Rob Tougher. #Haskell #CAS
  141. El tipo abstracto de datos de las tablas en Haskell. #Vestigium #Haskell
  142. El tipo abstracto de datos de los árboles binarios de búsqueda en Haskell.
  143. Propositional Consequence Relations and Algebraic Logic by Ramon Jansana
  144. Why Functional Programming Matters. (via @dr_chaieb)
  145. Aesthetics for the Working Mathematician. #Math (via @MathUpdate)
  146. El tipo abstracto de datos de los montículos en Haskell. #Vestigium #Haskell
  147. Feasibility via quantifier elimination II by Rod Carvalho. #Math
  148. Who Killed Prolog? by Maarten van Emden. #Prolog
  149. Prolog’s Death by Andre Vellino. #Prolog #Logic_programming #History
  150. A survey on Interactive Theorem Proving by Andrea Asperti #ITP #Math
  151. Ejercicios de programación funcional con Haskell (Pon a prueba tus habilidades!). #Haskell (via @EtnasSoft)
  152. ¡Aprende #Haskell por el bien de todos!. #Haskell #LibroLibre
  153. Performance and Evaluation of Lisp Systems by Richard P. Gabriel #Lisp
  154. Recorridos de grafos en Haskell. #Vestigium #Haskell
  155. Constructive Computation Theory: an executable course from Gerard Huet. #ML (via @psnively)