Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de marzo de 2012. La anterior recopilación fue la de febrero 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. Automatic proofs and refutations for higher-order logic. #Tesis #Isabelle
  2. On theorem prover-based testing. #Isabelle
  3. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. #Coq
  4. Tips on Haskell. #Tutorial #Haskell
  5. Enfragmo: A system for modelling and solving search problems with logic. #SAT
  6. Logic & reasoning: from Aristotle to Intel. #Panorama #Lógica
  7. Deciding Kleene Algebras in Coq. #Coq
  8. Vérification semi-automatique de primitives cryptographiques. #Tesis #Coq
  9. Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. #PVS
  10. Formal error analysis and verification of the frequency domain equalizer. #HOL
  11. Introduction to the Coq proof-assistant for practical software verification. #Tutorial #Coq
  12. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #Coq
  13. Mathematics for Computer Science. #Libro
  14. Proving possibilistic, probabilistic noninterference. #Isabelle
  15. Decision procedures in Algebra and Logic (Reading material). #Libro #Lógica
  16. A formalization of the theorem of existence of first-order most general unifiers. #PVS
  17. The worldʼs shortest correct exact real arithmetic program?. #PVS #Haskell
  18. Kleene algebra, rewriting modulo AC and circuits in Coq. #Tesis #Coq
  19. Deriving a fast inverse of the generalized Cantor n-tupling bijection. #Prolog
  20. PVS linear algebra libraries for verification of control software algorithms in C/ACSL. #PVS
  21. Generating verifiable Java code from verified PVS specifications. #PVS
  22. Haskell gets argumentative. #Haskell #Lógica @IA
  23. Induction and recursion. #Fundamentos
  24. A formal proof of Sasaki-Murao algorithm. #Coq
  25. Essential incompleteness of arithmetic verified by Coq. #Coq
  26. Incompleteness & completeness: Formalizing logic and analysis in type theory. #Tesis #Coq
  27. Well-quasi-orders. #Isabelle
  28. Analyse et Conception Formelles (Software formal analysis and design). #Curso #Isabelle
  29. Programming and proving in Isabelle/HOL. #Isabelle
  30. Numerical analysis of ordinary differential equations. #Isabelle
  31. Inductive study of confidentiality. #AFP #Isabelle
  32. Formal correctness of security protocols. #Libro #Isabelle
  33. Stuttering equivalence. #AFP
  34. HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving. #Tesis #Haskell
  35. A string of pearls: proofs of Fermat’s little theorem. #HOL4
  36. Separation logic: A logic for shared mutable data structures.
  37. Local action and abstract separation logic.
  38. Separation algebra. #Isabelle
  39. Using PVS to support the analysis of distributed cognition systems. #PVS
  40. Formal verification of the heavy hitter problem. #HOL
  41. Formal probabilistic analysis using theorem proving. #Tesis #HOL
  42. Proving equational Haskell properties using automated theorem provers. #Haskell #Thesis
  43. Accessible integrated formal reasoning environments in classroom instruction of mathematics.
  44. Designing accessible lightweight formal verification systems.
  45. Artificial intelligence: from fantasy to reality. #IA
  46. HipSpec: Automating inductive proofs of program properties. #Haskell
  47. Supplementary material for “Thinking as computation”. #IA #Prolog
  48. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  49. Bridging the gap: Automatic verified abstraction of C
  50. Computing in Cantor’s paradise with λZFC.
  51. Thoughts on gamifying textbooks.
  52. Isabelle/Circus: A process specification and verification environment. #Isabelle
  53. Isabelle/Circus. #Isabelle
  54. Wave equation numerical resolution: a comprehensive mechanized proof of a C program #Coq
  55. Large-scale formal verification in practice: A process perspective. #Isabelle
  56. A framework for formally verifying software transactional memory algorithms. #PVS
  57. Rigorous polynomial approximation using Taylor models in Coq. #Coq
  58. Rigorous polynomial approximations and applications. #Tesis #Coq
  59. Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project. #MKM
  60. Formalizing Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  61. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  62. Formal verification of monad transformers. #Isabelle
  63. HALO: Haskell to logic through denotational semantics. #Haskell
  64. Interactive proof: Introduction to Isabelle/HOL. #Tutorial #Isabelle
  65. Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
  66. Lifting and transfer: A modular design for quotients in Isabelle/HOL. #Isabelle
  67. Meta-theory à la carte. #Coq
  68. Mechanization of an algorithm for deciding KAT terms equivalence. #Coq
  69. ¿Es posible construir software que no falle?. #Verificación
  70. Proving the impossibility of trisecting an angle and doubling the cube. #Isabelle
  71. Formal specification and verification of well-formedness in business process product lines. #PVS
  72. Compiling concurrency correctly (Verifying software transactional memory). #Tesis #Agda #Haskell
  73. Représentation coinductive des graphes. #Tesis #Coq
  74. Formalizing adequacy: A case study for higher-order abstract syntax. #Isabelle
  75. Algorithms in games evolving in time: Winning strategies based on testing. #Isabelle
  76. A certified JavaScript interpreter. #Coq
  77. Formalization of Shannon’s theorems in SSReflect-Coq. #Coq
  78. Abstract interpretation of annotated commands. #Isabelle
  79. Construction of real algebraic numbers in Coq. #Coq
  80. Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. #Isabelle
  81. Towards provably robust watermarking. #Coq
  82. Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL. #Isabelle
  83. Formalizing an abstract algebra textbook in Isabelle/HOL. #Isabelle
  84. Numerical analysis of ordinary differential equations in Isabelle/HOL. #Isabelle
  85. A refinement-based approach to computational algebra in Coq. #Coq
  86. Coherent and strongly discrete rings in type theory. #Coq
  87. Logic + control: An example of program construction. #Prolog
  88. Deriving a fast inverse of the generalized Cantor N-tupling bijection. #Prolog
  89. Formalization and verification of number theoretic algorithms using the Mizar proof checker. #Mizar

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.