https://www.glc.us.es/web/index.php?action=history&feed=atom&title=Lecturas_del_a%C3%B1o_2013 Lecturas del año 2013 - Historial de revisiones 2026-07-19T00:50:27Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.0 https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1233&oldid=prev Jalonso en 17:03 30 mar 2014 2014-03-30T17:03:24Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 17:03 30 mar 2014</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l82" >Línea 82:</td> <td colspan="2" class="diff-lineno">Línea 82:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://cl-informatik.uibk.ac.at/users/griff/publications/S-Draft-2013 A formal proof of Kruskal&#039;s tree theorem in Isabelle/HOL]. #Isabelle</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://cl-informatik.uibk.ac.at/users/griff/publications/S-Draft-2013 A formal proof of Kruskal&#039;s tree theorem in Isabelle/HOL]. #Isabelle</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.ps.uni-saarland.de/Publications/documents/DoczkalEtAl_2013_A-Constructive.pdf A constructive theory of regular languages in Coq]. #Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.ps.uni-saarland.de/Publications/documents/DoczkalEtAl_2013_A-Constructive.pdf A constructive theory of regular languages in Coq]. #Coq</div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">== Lecturas de mayo de 2013 ==</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10XLrRA Graph theory (in Isabelle/HOL)] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1238B4m A macro for reusing abstract functions and theorems] ACL2</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/YwuCeL Reseña: Light-weight containers for Isabelle: efficient, extensible, nestable] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/17H2mqy Formalizing Turing machines (in Matita)] Matita</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11UgN6A HLearn: A machine learning library for Haskell] Haskell IA</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/191FmkG Computer science concepts in Scratch] Libro Scratch</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11s43JA Introduction to the OCaml programming language] OCaml</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/13nLTXc Introduction to the Coq proof assistant] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/12sKJZm An introduction to quantum programming in Quipper] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18MIR11 A certified reduction strategy for homological image processin] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HO] HOL4</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/15TzD4u Asynchronous functional reactive programming for GUIs] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/15TCOJx How computers work: Computational thinking for everyone] Libro</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generatio] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10Eem64 The four colour theorem: Engineering of a formal proof] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/15VfcEq Discrete structures via circuits, BDD, SAT, SMT, and functional programming in Python] Libro Python</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/15VfB9T Modeling and reasoning about computation] Libro Python</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18UE1iz Understanding Yoneda&#039;s lemma with Haskell examples] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18UETUf Game of life in Haskell] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18UF6H6 Functional game of life (part 3)] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/oDveH8 Haskell for kids] Haskell Gloss</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10ftmf1 Practical SAT solving (Course slides)] SAT</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10fv8wO Verifying refutations with extended resolution] ACL2 SAT</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10fAEvR Homotopy theory in type theory: Progress report] Agda</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HO] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/13IUDEf Parallel and concurrent programming in Haskell] Libro Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/179JeEP The complete correctness of sorting] Agda</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/12FU9PS Discrete mathematics with algorithms (Downloadable version)] Libro</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18rKiRn Certifying Network Calculus in a proof assistant] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution] ACL2 SAT</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1at0dOu Solving the snake cube puzzle in Haskell] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/ZfSQrQ Automatic data refinement] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/12Tb15U Data analysis with monoids] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10JcLBC Understanding continuations] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/12Tc0CT The functional programming elevator pitch] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1432H6b The seven bridges of Königsberg] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;">== Lecturas de junio de 2013 ==</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"></ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11K1stt Representing game dialogue as expressions in first-order logic] Tesis Clojure</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/19ypp8D Haskell string calculator kata] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11ZcYkJ Algebra lineal con aplicaciones y Python] Libro Python</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11ZhcJh Haskell from C: Where are the for Loops] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11myzPd Speeding through Haskell] Libro Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11mz4sj Arithmetic algorithms for hereditarily binary natural numbers] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11wiWYo Answer-set programming: Motivation and introduction] ASP</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/ZxcEHy Structural induction principles for functional programmers] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/124Zl3A Automating theorem proving with SMT] Dafny</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/189OpFa Racket Functional programming to elementary mathematic teachers] Racket</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/16PRHgh Certified HLints with Isabelle/HOLCF-Prelude] Haskell Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11qdq6G Formalization of basic linear algebra] Tesis Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/13MDBGS Theorem of three circles in Coq] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11qegA8 A Prolog specification of giant number arithmetic] Prolog</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11ywFxW Formalizing bounded increase] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/198ohtI Formal verification of language-based concurrent noninterference] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1bsjhNu Arithmetic algorithms for hereditarily binary natural numbers] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/13y94Ms A Haskell library for term rewriting] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/19t8xlh Understanding algebras] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11sd27Q Miller-Rabin primality test] Python</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11se6sC Data flow fusion with series expressions in Haskell] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/17UPobq De Bruijn&#039;s ideas on the Formalization of Mathematics] Historia</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/17UQELC Formal mathematics on display: A wiki for Flyspec] Flyspec</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/100o1rz Proofs, upside down (A functional correspondence between natural deduction and the sequent calculus)] OCaml</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1bU7YO8 Solveurs CP(FD) vérifiés formellemen] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/12Z5pw4 Formalizing bounded increas] Isabelle</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/10Gjc9y Certified symbolic manipulation: Bivariate simplicial polynomial] ACL2</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/15tgOiC Quipper: a quantum programming language] Haskell</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11UyCB6 Distributed data structures with Coq: PN-Counters] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1323Pbu Computational verification of network programs in Coq] Coq</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/1c2oQTc The HoTT Book (Homotopy type theory: Univalent foundations of mathematics)] Libro HoTT</ins></div></td></tr> <tr><td colspan="2">&#160;</td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div><ins style="font-weight: bold; text-decoration: none;"># [http://bit.ly/11N6Bjv Certifying homological algorithms to study biomedical image] Coq SSReflect Haskell QuickCheck</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de julio de 2013 ==</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de julio de 2013 ==</div></td></tr> </table> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1228&oldid=prev Jalonso en 16:09 30 mar 2014 2014-03-30T16:09:43Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 16:09 30 mar 2014</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l83" >Línea 83:</td> <td colspan="2" class="diff-lineno">Línea 83:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.ps.uni-saarland.de/Publications/documents/DoczkalEtAl_2013_A-Constructive.pdf A constructive theory of regular languages in Coq]. #Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.ps.uni-saarland.de/Publications/documents/DoczkalEtAl_2013_A-Constructive.pdf A constructive theory of regular languages in Coq]. #Coq</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Julio </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">julio </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/17CSSg0 Automated proof checking in introductory discrete mathematics classes]. ITP Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/17CSSg0 Automated proof checking in introductory discrete mathematics classes]. ITP Coq</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l133" >Línea 133:</td> <td colspan="2" class="diff-lineno">Línea 133:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.cs.kent.ac.uk/people/rpg/jek26/FvB/main.pdf Proofs you can believe in: Proving equivalences between Prolog semantics in Coq]. Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.cs.kent.ac.uk/people/rpg/jek26/FvB/main.pdf Proofs you can believe in: Proving equivalences between Prolog semantics in Coq]. Coq</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Agosto </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">agosto </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://dld.bz/cJ8EG A tutorial on the universality and expressiveness of fold] Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://dld.bz/cJ8EG A tutorial on the universality and expressiveness of fold] Haskell</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l192" >Línea 192:</td> <td colspan="2" class="diff-lineno">Línea 192:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/18n1lSB An introduction to language processing] Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/18n1lSB An introduction to language processing] Haskell</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Septiembre </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">septiembre </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1dEWCnt Call-by-need supercompilation] Tesis Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1dEWCnt Call-by-need supercompilation] Tesis Haskell</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l243" >Línea 243:</td> <td colspan="2" class="diff-lineno">Línea 243:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1fBT4mW Revisiting examples of computer assisted mathematics] Sage</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1fBT4mW Revisiting examples of computer assisted mathematics] Sage</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Octubre </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">octubre </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl] Nuprl</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl] Nuprl</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l269" >Línea 269:</td> <td colspan="2" class="diff-lineno">Línea 269:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1aqlYjo Course: Language-oriented programming] Lisp</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1aqlYjo Course: Language-oriented programming] Lisp</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Noviembre </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">noviembre </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/16ur1zF Trimming while checking clausal proofs] SAT</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/16ur1zF Trimming while checking clausal proofs] SAT</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l322" >Línea 322:</td> <td colspan="2" class="diff-lineno">Línea 322:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1b2Z7wD Autómatas celulares] IA</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://bit.ly/1b2Z7wD Autómatas celulares] IA</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del class="diffchange diffchange-inline">=</del>== Lecturas de <del class="diffchange diffchange-inline">Diciembre </del>de 2013 <del class="diffchange diffchange-inline">=</del>==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">diciembre </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.sciencedirect.com/science/article/pii/S2212671613000693 Formal modeling and verification of multi-agent system architecture]. PVS</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div># [http://www.sciencedirect.com/science/article/pii/S2212671613000693 Formal modeling and verification of multi-agent system architecture]. PVS</div></td></tr> </table> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1227&oldid=prev Jalonso en 16:06 30 mar 2014 2014-03-30T16:06:44Z <p></p> <a href="https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&amp;diff=1227&amp;oldid=1202">Mostrar los cambios</a> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1202&oldid=prev Jalonso en 11:00 7 jul 2013 2013-07-07T11:00:12Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 11:00 7 jul 2013</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td> <td colspan="2" class="diff-lineno">Línea 1:</td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <del class="diffchange diffchange-inline">Enero </del>de 2013 ==</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de <ins class="diffchange diffchange-inline">enero </ins>de 2013 ==</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell</div></td></tr> </table> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1200&oldid=prev Jalonso en 05:36 28 abr 2013 2013-04-28T05:36:41Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 05:36 28 abr 2013</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td> <td colspan="2" class="diff-lineno">Línea 1:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de Enero de 2013 ==</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de Enero de 2013 ==</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div><del style="font-weight: bold; text-decoration: none;">* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-diciembre-de-2012/ Lecturas del Grupo de Lógica Computacional (Diciembre de 2012)]. #GLC</del></div></td><td colspan="2">&#160;</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l21" >Línea 21:</td> <td colspan="2" class="diff-lineno">Línea 20:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www21.in.tum.de/~traytel/papers/mso/mso.pdf A verified decision procedure for MSO on words based on derivatives of regular expressions]. #Isabelle</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www21.in.tum.de/~traytel/papers/mso/mso.pdf A verified decision procedure for MSO on words based on derivatives of regular expressions]. #Isabelle</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://arxiv.org/abs/1301.6039 Statistical proof-patterns in Coq/SSReflect]. #Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://arxiv.org/abs/1301.6039 Statistical proof-patterns in Coq/SSReflect]. #Coq</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://arxiv.org/pdf/1301.6905v1 Towards a logic-based unifying framework for computing]. &#160;</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://arxiv.org/pdf/1301.6905v1 Towards a logic-based unifying framework for computing]. <ins class="diffchange diffchange-inline">#RA</ins></div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/SW13.pdf Termination tools in automated reasoning]. #Tesis</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/SW13.pdf Termination tools in automated reasoning]. #Tesis <ins class="diffchange diffchange-inline">#RA</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de febrero de 2013&#160; ==</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>== Lecturas de febrero de 2013&#160; ==</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l33" >Línea 33:</td> <td colspan="2" class="diff-lineno">Línea 32:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://blogs.elpais.com/turing/2013/02/algunos-vinculos-entre-los-teoremas-de-godel-y-turing.html Algunos vínculos entre los teoremas de Gödel y Turing]</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://blogs.elpais.com/turing/2013/02/algunos-vinculos-entre-los-teoremas-de-godel-y-turing.html Algunos vínculos entre los teoremas de Gödel y Turing]</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_%28v._1.02%29.pdf Formal computations and methods]. #Tesis #HOL_Light</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_%28v._1.02%29.pdf Formal computations and methods]. #Tesis #HOL_Light</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://goo.gl/LXZra Complex concept lattices for simulating human prediction in sport].</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://goo.gl/LXZra Complex concept lattices for simulating human prediction in sport]. <ins class="diffchange diffchange-inline">#AFC</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www4.in.tum.de/~blanchet/mash.pdf MaSh: Machine learning for Sledgehammer]. #Isabelle #ITP2013</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www4.in.tum.de/~blanchet/mash.pdf MaSh: Machine learning for Sledgehammer]. #Isabelle #ITP2013</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.theses.fr/2012BOR14708 Une étude formelle de la théorie des calculs locaux à l&#039;aide de l&#039;assistant de preuve Coq]. #Tesis #Coq</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.theses.fr/2012BOR14708 Une étude formelle de la théorie des calculs locaux à l&#039;aide de l&#039;assistant de preuve Coq]. #Tesis #Coq</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.cs.us.es/~jalonso/publicaciones/2013-Temas_de_PLIA.pdf Temas de programación lógica e inteligencia artificial]. #Prolog</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.cs.us.es/~jalonso/publicaciones/2013-Temas_de_PLIA.pdf Temas de programación lógica e inteligencia artificial]. #Prolog</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell].</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell]. <ins class="diffchange diffchange-inline">#Haskell</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell].</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell]. <ins class="diffchange diffchange-inline">#Haskell</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle</div></td></tr> <tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l70" >Línea 70:</td> <td colspan="2" class="diff-lineno">Línea 69:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf Formalization of real analysis: A survey of proof assistants and libraries]. #ITP</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf Formalization of real analysis: A survey of proof assistants and libraries]. #ITP</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_21.pdf AI over large formal knowledge bases: The first decade]. #Mizar</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_21.pdf AI over large formal knowledge bases: The first decade]. #Mizar</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_20.pdf ForMaRE-formal mathematical reasoning in economics].</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_20.pdf ForMaRE-formal mathematical reasoning in economics]. <ins class="diffchange diffchange-inline">#RA</ins></div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www4.in.tum.de/~nipkow/pubs/cav13.pdf A fully verified executable LTL model checker]. #Isabelle</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www4.in.tum.de/~nipkow/pubs/cav13.pdf A fully verified executable LTL model checker]. #Isabelle</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.cse.chalmers.se/~nicsma/hipspec-cade.pdf Automating inductive proofs using theory exploration]. #Haskell #HipSpec</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.cse.chalmers.se/~nicsma/hipspec-cade.pdf Automating inductive proofs using theory exploration]. #Haskell #HipSpec</div></td></tr> </table> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1193&oldid=prev Jalonso en 17:46 27 abr 2013 2013-04-27T17:46:45Z <p></p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 17:46 27 abr 2013</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l39" >Línea 39:</td> <td colspan="2" class="diff-lineno">Línea 39:</td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell].</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell].</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2</div></td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>* [<del class="diffchange diffchange-inline">%20http</del>://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell].</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>* [<ins class="diffchange diffchange-inline">http</ins>://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell].</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>* [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle</div></td></tr> </table> Jalonso https://www.glc.us.es/web/index.php?title=Lecturas_del_a%C3%B1o_2013&diff=1192&oldid=prev Jalonso: New page: == Lecturas de Enero de 2013 == * [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-diciembre-de-2012/ Lecturas del Grupo de Lógica Computacional (Diciem... 2013-04-27T17:44:54Z <p>New page: == Lecturas de Enero de 2013 == * [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-diciembre-de-2012/ Lecturas del Grupo de Lógica Computacional (Diciem...</p> <p><b>Página nueva</b></p><div>== Lecturas de Enero de 2013 ==<br /> * [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-diciembre-de-2012/ Lecturas del Grupo de Lógica Computacional (Diciembre de 2012)]. #GLC<br /> * [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell<br /> * [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell<br /> * [http://www.glc.us.es/~jalonso/vestigium/representacion-de-2n-como-7x2y2-en-haskell/ Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell] #Haskell<br /> * [http://afp.sourceforge.net/entries/Sqrt_Babylonian.shtml Computing square roots using the babylonian method]. #Isabelle<br /> * [http://arxiv.org/pdf/1301.1702v1 Formal verification of nonlinear inequalities with Taylor interval approximations]. #HOL_Light<br /> * [http://www.chargueraud.org/research/2010/thesis/thesis_final.pdf Characteristic formulae for mechanized program verification]. #Tesis #Coq<br /> * [http://home.informatik.tu-muenchen.de/~hoelzl/documents/hoelzl2012thesis-draft.pdf Construction and stochastic applications of measure spaces in Higher-Order Logic]. #Tesis #Isabelle<br /> * [http://www.cs.unibo.it/~asperti/PAPERS/bertrand.pdf A proof of Bertrand’s postulate]. #Matita<br /> * [http://arxiv.org/abs/1212.6641 Trusting computations: a mechanized proof from partial differential equations to actual program]. #Coq<br /> * [http://www.ps.uni-saarland.de/Publications/documents/Kaiser_2012_Formal.pdf Formal construction of a set theory in Coq]. #Tesis #Coq<br /> * [http://afp.sourceforge.net/browser_info/current/HOL/HOL-Multivariate_Analysis/Rank_Nullity_Theorem/document.pdf Rank-nullity theorem in linear algebra]. #Isabelle #AFP<br /> * [http://studia.complexica.net/Art/RI100301.pdf GDT4MAS: a formal model and language to specify and verify agent-based complex systems]. #PVS<br /> * [http://afp.sourceforge.net/entries/Kleene_Algebra.shtml Kleene algebra]. #AFP #Isabelle<br /> * [http://hvg.ece.concordia.ca/Publications/Thesis/Tarek-PhD-Thesis.pdf Information-theoretic analysis using theorem proving]. #Tesis #HOL4<br /> * [http://www.cs.ru.nl/~leonard/thesis/phdthesis.pdf Applying formal methods in software development]. #Tesis #PVS<br /> * [http://hal.inria.fr/hal-00762627 Formalization and concretization of ordered networks]. #Coq<br /> * [http://people.cs.missouri.edu/~harrisonwl/papers/tfp2012.pdf The design of a practical proof checker for a lazy functional language]. #MProver #Haskell<br /> * [http://events.math.unipd.it/fomcaf13/sites/default/files/Farmer_slides.pdf The formalization of syntax-based mathematical algorithms using quotation and evaluation]<br /> * [http://www21.in.tum.de/~traytel/papers/mso/mso.pdf A verified decision procedure for MSO on words based on derivatives of regular expressions]. #Isabelle<br /> * [http://arxiv.org/abs/1301.6039 Statistical proof-patterns in Coq/SSReflect]. #Coq<br /> * [http://arxiv.org/pdf/1301.6905v1 Towards a logic-based unifying framework for computing]. <br /> * [http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/SW13.pdf Termination tools in automated reasoning]. #Tesis<br /> <br /> == Lecturas de febrero de 2013 ==<br /> * [http://hal.inria.fr/docs/00/77/93/76/PDF/jfla2013-04.pdf Matrices à blocs et en forme canonique]. #Coq<br /> * [https://who.rocq.inria.fr/Frederic.Blanqui/papers/hanoi12.pdf Automated verification of termination certificates]. #Coq<br /> * [http://perso.crans.org/cohen/papers/thesis.pdf Formalized algebraic numbers: construction and first-order theory]. #Tesis #Coq<br /> * [http://www21.in.tum.de/~blanchet/self.pdf Towards self-verification of Isabelle&#039;s Sledgehammer]. #Isabelle<br /> * [http://arxiv.org/abs/1301.7462 A framework for the verification of certifying computations]. #Isabelle<br /> * [http://arxiv.org/abs/1302.1207 A preliminary univalent formalization of the p-adic numbers]. #Coq<br /> * [http://blogs.elpais.com/turing/2013/02/algunos-vinculos-entre-los-teoremas-de-godel-y-turing.html Algunos vínculos entre los teoremas de Gödel y Turing]<br /> * [http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_%28v._1.02%29.pdf Formal computations and methods]. #Tesis #HOL_Light<br /> * [http://goo.gl/LXZra Complex concept lattices for simulating human prediction in sport].<br /> * [http://www4.in.tum.de/~blanchet/mash.pdf MaSh: Machine learning for Sledgehammer]. #Isabelle #ITP2013<br /> * [http://www.theses.fr/2012BOR14708 Une étude formelle de la théorie des calculs locaux à l&#039;aide de l&#039;assistant de preuve Coq]. #Tesis #Coq<br /> * [http://www.cs.us.es/~jalonso/publicaciones/2013-Temas_de_PLIA.pdf Temas de programación lógica e inteligencia artificial]. #Prolog<br /> * [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell].<br /> * [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2<br /> * [%20http://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell].<br /> * [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS<br /> * [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle<br /> <br /> == Lecturas de marzo de 2013 ==<br /> * [http://arxiv.org/abs/1302.6421 ML4PG: proof-mining in Coq]. #Coq<br /> * [http://sevein.matap.uma.es/~aciego/TR/icfca13.pdf Concept-forming operators on multilattices]. #AFC<br /> * [http://downloads.hindawi.com/journals/jam/aip/160875.pdf The gauge integral theory in HOL4]. #HOL4<br /> * [http://www.cs.ru.nl/~spitters/Picard.pdf The Picard algorithm for ordinary differential equations in Coq]. #Coq<br /> * [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle #ITP2013<br /> * [http://jcst.ict.ac.cn:8080/jcst/EN/abstract/abstract9593.shtml Formal reasoning about finite-state discrete-time Markov chains in HOL]. #HOL<br /> * [http://arxiv.org/pdf/1303.1420 Verifying a plaftorm for digital imaging: a multi-tool strategy]. #Coq #ACL2<br /> * [http://goo.gl/fDR4t Deducción natural en lógica proposicional con Isabelle/HOL]. #Isabelle<br /> * [http://www.glc.us.es/~jalonso/vestigium/resena-formalized-algebraic-numbers-construction-and-first-order-theory/ Formalized algebraic numbers: construction and first-order theory]. #Tesis #Coq<br /> * [http://goo.gl/GGXrV DAO: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL]. #Isabelle<br /> * [http://goo.gl/CXziO DAO: Ejercicios de argumentación proposicional con Isabelle/HOL]. #Isabelle<br /> * [http://redwood.cs.ttu.edu/~mgelfond/FALL-2012/book.pdf Knowledge representation, reasoning, and the design of intelligent agents]. #Libro #ASP<br /> * [http://goo.gl/7q8fp DAO: Deducción natural en lógica de primer orden con Isabelle/HOL]. #Isabelle<br /> * [http://goo.gl/UeDaX DAO: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL]. #Isabelle<br /> * [http://www.computing.dundee.ac.uk/staff/jheras/papers/ahomsia.pdf A hierarchy of mathematical structures in ACL2]. #ACL2<br /> * [http://goo.gl/fqITF DAO: Argumentación en lógica de primer orden con Isabelle/HOL (1)]. #Isabelle<br /> * [http://goo.gl/GMqX7 DAO: Argumentación en lógica de primer orden con Isabelle/HOL (2)]. #Isabelle<br /> * [http://www.univ-orleans.fr/lifo/prodsci/rapports/RR/RR2013/RR-2013-02.pdf Programming and reasonning with powerlists in Coq]. #Coq<br /> * [http://qpl.naturalspublishing.com/files/published/j44lfykd8715l9.pdf Formalization of the complex number theory in HOL4]. #HOL4<br /> <br /> == Lecturas de abril de 2013 ==<br /> * [http://arxiv.org/abs/1303.7335 Formalizing the confluence of orthogonal rewriting systems]. #PVS<br /> * [http://arxiv.org/abs/1304.0680 Homotopy limits in Coq]. #Coq<br /> * [http://isabelle.in.tum.de/~haftmann/pdf/data_refinement_haftmann_kuncar_krauss_nipkow.pdf Data refinement in Isabelle/HOL]. #Isabelle_HOL<br /> * [http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf Formalization of real analysis: A survey of proof assistants and libraries]. #ITP<br /> * [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_21.pdf AI over large formal knowledge bases: The first decade]. #Mizar<br /> * [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_20.pdf ForMaRE-formal mathematical reasoning in economics].<br /> * [http://www4.in.tum.de/~nipkow/pubs/cav13.pdf A fully verified executable LTL model checker]. #Isabelle<br /> * [http://www.cse.chalmers.se/~nicsma/hipspec-cade.pdf Automating inductive proofs using theory exploration]. #Haskell #HipSpec<br /> * [http://hal.inria.fr/hal-00809651/en/ One logic to use them all]. #CADE24 #Why3<br /> * [http://www.lix.polytechnique.fr/~neron/Publi/Elimsqrt/elimsqstrat.pdf Square root and division elimination in PVS]. #PVS #ITP2013<br /> * [http://home.in.tum.de/~traytel/papers/teaching_haskell/teaching.pdf Experience report: Teaching Haskell to the masses]. #Haskell<br /> * [http://www4.in.tum.de/~blanchet/compl.pdf Coinductive pearl: Modular first-order logic completeness]. #Isabelle<br /> * [http://argo.matf.bg.ac.rs/publications/2012/simplex.pdf Formalization of incremental simplex algorithm by stepwise refinement]. #Isabelle <br /> * [http://hal.inria.fr/docs/00/80/94/48/PDF/slides_vulgarisation_coq.pdf Les assistants de preuve, ou comment avoir confiance en ses démonstrations]. #DAO<br /> * [http://www.cs.bham.ac.uk/research/projects/formare/events/aisb2013/submissions/stage2/99990025.pdf Developing an auction theory toolbox]. #Isabelle<br /> * [http://cl-informatik.uibk.ac.at/users/griff/publications/ST-RTA13.pdf Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. #Isabelle<br /> * [http://cl-informatik.uibk.ac.at/users/griff/publications/S-Draft-2013 A formal proof of Kruskal&#039;s tree theorem in Isabelle/HOL]. #Isabelle<br /> * [http://www.ps.uni-saarland.de/Publications/documents/DoczkalEtAl_2013_A-Constructive.pdf A constructive theory of regular languages in Coq]. #Coq</div> Jalonso