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