Lecturas del Grupo de Lógica Computacional (Junio de 2013)

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de enero de 2013. La anterior recopilación fue la de diciembre de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Problemas sobre el 2013 en Haskell. #Haskell
  2. La sucesión de Perrin en Haskell. #Haskell
  3. Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
  4. Computing square roots using the babylonian method. #Isabelle
  5. Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
  6. Characteristic formulae for mechanized program verification. #Tesis #Coq
  7. Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
  8. A proof of Bertrand’s postulate. #Matita
  9. Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
  10. Formal construction of a set theory in Coq. #Tesis #Coq
  11. Rank-nullity theorem in linear algebra. #Isabelle #AFP
  12. GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
  13. Kleene algebra. #AFP #Isabelle
  14. Information-theoretic analysis using theorem proving. #Tesis #HOL4
  15. Applying formal methods in software development. #Tesis #PVS
  16. Formalization and concretization of ordered networks. #Coq
  17. The design of a practical proof checker for a lazy functional language. #MProver #Haskell
  18. The formalization of syntax-based mathematical algorithms using quotation and evaluation
  19. A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
  20. Statistical proof-patterns in Coq/SSReflect. #Coq
  21. Towards a logic-based unifying framework for computing.
  22. Termination tools in automated reasoning. #Tesis
  23. Matrices à blocs et en forme canonique. #Coq
  24. Automated verification of termination certificates. #Coq
  25. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  26. Towards self-verification of Isabelle’s Sledgehammer. #Isabelle
  27. A framework for the verification of certifying computations. #Isabelle
  28. A preliminary univalent formalization of the p-adic numbers. #Coq
  29. Algunos vínculos entre los teoremas de Gödel y Turing
  30. Formal computations and methods. #Tesis #HOL_Light
  31. Complex concept lattices for simulating human prediction in sport.
  32. MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
  33. Une étude formelle de la théorie des calculs locaux à l’aide de l’assistant de preuve Coq. #Tesis #Coq
  34. Temas de programación lógica e inteligencia artificial. #Prolog
  35. Una curiosa propiedad del 123 en Haskell. #Haskell
  36. A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
  37. Otra curiosa propiedad del 123 en Haskell. #Haskell
  38. Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
  39. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
  40. ML4PG: proof-mining in Coq. #Coq
  41. Concept-forming operators on multilattices. #AFC
  42. The gauge integral theory in HOL4. #HOL4
  43. The Picard algorithm for ordinary differential equations in Coq. #Coq
  44. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
  45. Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
  46. Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
  47. Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
  48. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  49. Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
  50. A hierarchy of mathematical structures in ACL2. #ACL2
  51. Programming and reasonning with powerlists in Coq. #Coq
  52. Formalization of the complex number theory in HOL4. #HOL4
  53. Formalizing the confluence of orthogonal rewriting systems. #PVS
  54. Homotopy limits in Coq. #Coq
  55. Data refinement in Isabelle/HOL. #Isabelle_HOL
  56. Formalization of real analysis: A survey of proof assistants and libraries. #ITP
  57. AI over large formal knowledge bases: The first decade. #Mizar
  58. ForMaRE-formal mathematical reasoning in economics.
  59. A fully verified executable LTL model checker. #Isabelle
  60. Automating inductive proofs using theory exploration. #Haskell #HipSpec
  61. One logic to use them all. #CADE24 #Why3
  62. Square root and division elimination in PVS. #PVS #ITP2013
  63. Experience report: Teaching Haskell to the masses. #Haskell
  64. Coinductive pearl: Modular first-order logic completeness. #Isabelle
  65. Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
  66. Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
  67. Developing an auction theory toolbox. #Isabelle
  68. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
  69. A formal proof of Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  70. A constructive theory of regular languages in Coq. #Coq
  71. A machine-checked proof of the odd order theorem. #Coq
  72. Graph theory. #Isabelle #AFP
  73. A macro for reusing abstract functions and theorems. #ACL2
  74. Light-weight containers for Isabelle: efficient, extensible, nestable. #Isabelle
  75. Formalizing Turing machines. #Matita
  76. A certified reduction strategy for homological image processing. #Coq
  77. On the formalization of continuous-time Markov chains in HOL. #HOL
  78. A Web interface for Isabelle: The next generation. #Isabelle #CICM2013
  79. Verifying refutations with extended resolution. #ACL2
  80. Type classes and filters for mathematical analysis in Isabelle/HOL. #Isabelle
  81. Mechanical verification of SAT refutations with extended resolution. #ACL2 #ITP2013
  82. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). #Coq
  83. Automatic data refinement. #Isabelle #ITP2013
  84. Certified HLints with Isabelle/HOLCF-Prelude. #Isabelle
  85. Theorem of three circles in Coq. #Coq
  86. A Haskell library for term rewriting. #Haskell
  87. Formal mathematics on display: A wiki for Flyspeck. #HOL_Light
  88. Solveurs CP(FD) vérifiés formellement. #Coq
  89. Formalizing bounded increase. #Isabelle
  90. Certified symbolic manipulation: Bivariate simplicial polynomials. #ACL2
  91. The formalization of syntax-based mathematical algorithms using quotation and evaluation.
  92. Homotopy type theory: Univalent foundations of mathematics. #Libro
  93. Mathematicians think like machines for perfect proofs.
  94. Certifying homological algorithms to study biomedical images. #Tesis #Coq #Haskell
  95. Formalizing cut elimination of coalgebraic logics in Coq. #Coq

La recopilación de las lecturas anteriores se encuentra aquí.