Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre de 2012)

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de septiembre de 2012. La anterior recopilación fue la de agosto 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. Operational refinement for compiler correctness. #Tesis #Coq
  2. Interactive and automated proofs for graph transformations. #Isabelle
  3. Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)
  4. Piensa en Haskell (Ejercicios de programación funcional con Haskell). #Haskell
  5. ¿Computadores von Neumann, o computadores Turing? #Historia
  6. Formalizing Frankl’s conjecture: FC-families. #Isabelle
  7. Implementing an efficient theorem prover. #Tesis #Vampire
  8. System of logic based on ordinals. #Tesis #Historia
  9. Proving concurrent noninterference (código) #Isabelle
  10. Improving real analysis in Coq: a user-friendly approach to integrals and derivatives. #Coq (CPP2012)
  11. Computing persistent homology within Coq/SSReflect. #Coq
  12. Software libre para una sociedad libre. #Libro #Pensamiento
  13. A formal proof of Sasaki-Murao algorithm. #Coq (MAP2012, code, Presentación).
  14. Confluence by decreasing diagrams formalized. #Isabelle
  15. Proof Pearl – A mechanized proof of GHC’s mergesort. #Isabelle #Haskell
  16. A logic-algebraic approach to decision taking in a railway interlocking system. #BG
  17. Scheme in industrial automation. #Scheme
  18. Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2. #ACL2 #Tesis
  19. A string of pearls: Proofs of Fermat’s little theorem. #HOL4
  20. A formally-verified C compiler supporting floating-point arithmetic. #Coq
  21. The Boyer-Moore waterfall model revisited. #HOL_Light
  22. A Python pattern matcher project for an introduction to Artificial Intelligence course. #IA
  23. Informatik 2: Functional Programming. #Haskell
  24. Contributions to the formal verification of arithmetic algorithms. #Tesis #Coq
  25. Why learn Haskell?. #Tutorial #Haskell
  26. A mechanical verification of the independence of Tarski’s euclidean axiom y código #Tesina #Isabelle
  27. Weak completeness theorem for propositional linear time temporal logic. #Mizar
  28. Natural language processing for the working programmer. #Haskell #IA
  29. Nexus authorization logic (NAL): Logical results. #Coq
  30. Reasons for studying Haskell in University. #Haskell
  31. Constructive completeness for modal logic with transitive closure. #Coq #Modal
  32. A functional programming approach to AI search algorithms. #IA #PF
  33. Dual multi-adjoint concept lattices. #AFC
  34. Temas de “Demostración asistida por ordenador”. #Isabelle #Tutorial
  35. Verificación de programas: Introducción. #Verificación
  36. Último dígito del producto de números de Fermat. #Haskell #IMO
  37. A formal proof of square root and division elimination in embedded programs. #PVS
  38. Coq et caractères (Preuve formelle du théorème de Feit et Thompson). #Coq #Divulgación
  39. Formalized algebraic numbers: construction and first order theory. #Tesis #Coq
  40. How enterprises use functional languages, and why they don’t. #PF
  41. Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting. #Tesis #Isabelle
  42. Constructive formalization of regular languages. #Tesina #Coq
  43. Computing with free algebras. #Haskell
  44. Ask-Elle: a Haskell Tutor. #Tesis #Haskell #TI
  45. Using Isabelle to verify special relativity, with application to hypercomputation theory. #Isabelle

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