Lecturas del Grupo de Lógica Computacional (Febrero de 2012)
Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de Febrero de 2012. La anterior recopilación fue la de Enero 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.
- Emergence and refinement. #Sistemascomplejos
- Formalizing a hierarchical file system. #PVS
- Etude et formalisation de la méthode de Wu dans Coq. #Tesis #Coq
- Using PVS to investigate incidents through the lens of distributed ORG-LIST-END-MARKER cognition. #PVS
- Formal system verification for trustworthy embedded systems. #Isabelle
- The mechanical verification of a DPLL-based satisfiability solver. #PVS
- Innovación en el tratamiento de la información desde la Ingeniería del ORG-LIST-END-MARKER Conocimiento (1/2)
- Innovación en el tratamiento de la información desde la Ingeniería del ORG-LIST-END-MARKER Conocimiento (2/2)
- A unified treatment of syntax with binders.
- The age of Big Data. #IA
- Crear moléculas desde cero sin la endiablada ecuación de Schrödinger. #IA
- Refinement for monadic programs. #Isabelle
- Dijkstra’s shortest path algorithm. #Isabelle
- Computational topology.
- Category theory and functional programming. #Haskell
- The artist in the computer scientist: more humanity to our research.
- When formal systems kill: computer ethics and formal methods.
- Mathematics in the age of the Turing machine. #Panorama #DAO
- The reflective Milawa theorem prover is sound. #ACL2 #HOL4
- Ejercicios de “Informática de 1º de Matemáticas” (2011-12). #Haskell
- Temas de programación funcional con Haskell (curso 2011-12). #Haskell
- Executable transitive closures. #Isabelle