|
|
Línea 1: |
Línea 1: |
− | == Lecturas compartidas ==
| |
− | En esta sección se recopilada la lecturas compartidas en en lista de correo del Grupo de Lógica Computacional, ordenadas por orden cronológico según su publicación en la lista.
| |
− |
| |
− | === Lecturas del 27-Oct-2010 al 1-Jul-2011 ===
| |
− | * [http://goo.gl/Mpz03 Ejercicios de programación en Haskell] #Haskell #V
| |
− | * [http://goo.gl/0FwrK El valor del fracaso digno] #CM
| |
− | * [http://goo.gl/aWC1 Computational science: ... Error (... why scientific programming does not compute)] #Verificación
| |
− | * [http://goo.gl/5mUCh El tipo abstracto de datos de las pilas en Haskell] #Haskell #V
| |
− | * [http://goo.gl/rwY3S The free-form linguistics revolution in mathematica]
| |
− | * [http://goo.gl/3hNgt A preliminary survey on functional programming] #PF
| |
− | * [http://goo.gl/HDZyb Desarrollo del comando wc de Unix en Haskell] #Haskell #V
| |
− | * [http://goo.gl/AVXPW Lógica Computacional en Sevilla (30 años en una hora)] #V
| |
− | * [http://goo.gl/V7Sud Problema sobre números naturales] #Haskell #V
| |
− | * [http://goo.gl/PkVYW Rompecabeza de Ullman en Haskell] #Haskell #V
| |
− | * [http://goo.gl/hWPRa Lisp bot wins Google AI challenge — Will Lisp win in the semantic web, too?] #Lisp #IA
| |
− | * [http://goo.gl/NRnls Decálogo de la didáctica matemática] #Enseñanza #V
| |
− | * [http://goo.gl/b9gFY El decálogo del profesor (según Polya)] #Enseñanza #V
| |
− | * [http://goo.gl/CnWj0 Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers en] #Libro #AR
| |
− | * [http://goo.gl/87Z9o Parallelizing a CLIPS-based course timetabling expert system] #SE
| |
− | * [http://goo.gl/s4etS Certifying compilers using higher-order theorem provers as certificate checkers] #Verificación #V
| |
− | * [http://goo.gl/wo8BN Teorías y aplicaciones] #V
| |
− | * [http://goo.gl/95csF Does Godel's theorem matter to mathematics?]
| |
− | * [http://goo.gl/LBsyx Distributed SAT] #SAT
| |
− | * [http://posgrado.escom.ipn.mx/biblioteca/Semantic%20web%20reasoners%20and%20languages.pdf Semantic web reasoners and languages] #WS
| |
− | * [http://bit.ly/emHhvZ El 2011 y los números primos (en Haskell)] #Haskell #V
| |
− | * [http://bit.ly/ebNi54 The Dialectica interpertation in Coq] #Coq
| |
− | * [http://bit.ly/heSTJJ Errores aritméticos en Haskell y en Lisp] #Haskell #Lisp #V
| |
− | * [http://bit.ly/gLU60K Why Lisp is a big hack (and haskell is doomed to succeed)] #Lisp #Haskell
| |
− | * [http://bit.ly/h5v14x ProofWiki y la verificación de las demostraciones matemáticas] #Verificación #MKM #V
| |
− | * [http://bit.ly/fMi9V7 A quick and gentle guide to constraint logic programming via ECLiPSe] #PL #Restricciones
| |
− | * [http://bit.ly/gb4Dn9 A language for mathematical knowledge management] #MKM
| |
− | * [http://bit.ly/eLkbsW Automated inference of finite unsatisfiability] #AR
| |
− | * [http://bit.ly/evywxv The free vector space on a type] http://bit.ly/e9c5Zl #Haskell
| |
− | * [http://goo.gl/6t8YI Formal methods applied to a floating-point number system] #Z
| |
− | * [http://goo.gl/WT6G3 A machine-checked theory of floating point arithmetic] #HOL_Light
| |
− | * [http://goo.gl/k6NJJ Formal verification of floating point trigonometric functions] #HOL_Light
| |
− | * [http://goo.gl/RRb7p A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor] #ACL2
| |
− | * [http://goo.gl/gvh4C A Generic Library for Floating-Point Numbers and Its Application to Exact Computing] #Coq.
| |
− | * [http://goo.gl/oEgxU A High-Level Formalization of Floating-Point Numbers in PVS] #PVS
| |
− | * [http://goo.gl/4CHMF Formal verification of floating-point programs] #Coq
| |
− | * [http://goo.gl/W9svV The pitfalls of verifying floating-point computations] #Verificación
| |
− | * [http://goo.gl/xs5IG Floats and Ropes: A Case Study for Formal Numerical Program Verification] #Coq.
| |
− | * [http://bit.ly/grfNfD Algorithms Take Control of Wall Street] #IA
| |
− | * [http://bit.ly/gC0m7p Formal reliability analysis of combinational circuits using theorem proving] #HOL
| |
− | * [http://bit.ly/f8Nvpv Determinación, esperanza y éxitos en la resolución de problemas] #Enseñanza #V
| |
− | * [http://bit.ly/gZYKNJ Lectures in Game Theory for Computer Scientists] #Libro
| |
− | * [http://bit.ly/dNvlXU Reactive Valuations] #TFM
| |
− | * [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet]
| |
− | * [http://bit.ly/haeTax Algunas aplicaciones de las bases de Groebner]
| |
− | * [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell
| |
− | * [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq
| |
− | * [http://bit.ly/ht6544 El tipo abstracto de datos de las colas en Haskell] #Haskell #V
| |
− | * [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V
| |
− | * [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V
| |
− | * [http://bit.ly/h2co0D fKenzo: A user interface for computations in Algebraic Topology]
| |
− | * [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle
| |
− | * [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V
| |
− | * [http://bit.ly/epypbt Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?] #Verificación
| |
− | * [http://bit.ly/hIeQQi El próximo después de 1811] #Haskell #V
| |
− | * [http://bit.ly/hWod4k Humanos más capaces y robots que están en las nubes] #IA
| |
− | * [http://bit.ly/fTekAA Charming Proofs: A Journey Into Elegant Mathematics] #Libro #DAO
| |
− | * [http://bit.ly/fpnnu7 Functional Binomial Queues] #RF #Isabelle
| |
− | * [http://bit.ly/glOw9x Lower Semicontinuous Functions] #RF #Isabelle
| |
− | * [http://bit.ly/hvqHiB Lógica Informática (2010-11)] #V
| |
− | * [http://bit.ly/e6TgsN Inconsistent heuristics in theory and practice] #IA
| |
− | * [http://goo.gl/Igcbu On proof and progress in mathematics] #CM
| |
− | * [http://bit.ly/i9FH8v Artificial Intelligence (Foundations of Computational Agents)] #Libro #IA
| |
− | * [http://bit.ly/eLUOMY Are Mathematicians In Jeopardy?] #IA
| |
− | * [http://bit.ly/fMVueD Give me that good old-fashioned AI] #IA
| |
− | * [http://bit.ly/evZnr7 Building Watson: An Overview of the DeepQA Project] #IA
| |
− | * [http://bit.ly/hJWFDv Software verification turns maintstream] #Verificación
| |
− | * [http://rok.strnisa.com/thesis/thesis.pdf Formalising, improving, and reusing the Java Module System] http://bit.ly/dF68vF #Tesis #Isabelle
| |
− | * [http://goo.gl/D4L3j SMT solvers: new oracles for the HOL theorem prover] #SMT #HOL4
| |
− | * [http://bit.ly/e3QiRU Isabelle como un lenguaje funcional] #Isabelle #V
| |
− | * [http://bit.ly/fKKC3D El tipo abstracto de datos de las pilas en Haskell] #Haskell #V
| |
− | * [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V
| |
− | * [http://goo.gl/oUlcY Executable Transitive Closures of Finite Relations] #RF #Isabelle
| |
− | * [http://goo.gl/epNrc Solución española para un problema de John Nash]
| |
− | + [http://goo.gl/FoL94 Reduced Ordered Binary Decision Diagram with Implied Literals: A New knowledge Compilation Approach]. #AR
| |
− | * [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF
| |
− | * [http://goo.gl/2fK3d Introduction to Artificial Intelligence] #Libro #IA
| |
− | * [http://bit.ly/hZ9TWG La Universidad Carnegie-Mellon elimina la programación OO de su primer curso] #Enseñanza
| |
− | * [http://goo.gl/NXhJI Experience Report: Functional Programming through Deep Time (Modeling the first complex ecosystems on Earth)] #Haskell
| |
− | * [http://bit.ly/eEvWOO A Comparative Study on ILP-based Concept Discovery Systems] #ILP
| |
− | * [http://bit.ly/gE69RT Logic-Based Artificial Intelligence] #Libro #IA
| |
− | * [http://bit.ly/f4JcZN A Formalization of the C99 Standard in HOL, Isabelle and Coq] #HOL #Isabelle #Coq
| |
− | * [http://bit.ly/gQRpsr Formal methods in agent-oriented software engineering] #MF
| |
− | * [http://bit.ly/hO9ewV The cognitive agents specification language and verification environment] #Verificación
| |
− | * [http://bit.ly/hjBReD Software Bugs and Scientific Progress] #Verificación
| |
− | * [http://bit.ly/ffR1jT Representing model theory in a type-theoretical logical framework] #RF #Twelfe
| |
− | * [http://goo.gl/vCDeE Towards a verification framework for faulty message passing systems in PVS] #PVS
| |
− | * [http://bit.ly/g2tz4T Por qué y cómo se hace investigación en matemáticas] #CM
| |
− | * [http://goo.gl/Y6pl Introduction to newLISP] #Libro #Lisp
| |
− | * [http://goo.gl/23une Verified Firewall Policy Transformations for Test Case Generation] #Isabelle
| |
− | * [http://goo.gl/bxSx7 An Approach to Modular and Testable Security Models of Real-world Health-care Applications] #Isabelle
| |
− | * [http://bit.ly/fTzgF0 Psi-calculi: a framework for mobile processes with nominal data and logic] #Isabelle
| |
− | * [http://goo.gl/ZAqRw Artificial Intelligence and Human Thinking] #IA
| |
− | * [http://goo.gl/aKNFv Simplification Rules for Intuitionistic Propositional Tableaux] #AR
| |
− | * [http://bit.ly/e0qElc A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free] #ACL2
| |
− | * [http://bit.ly/h7oESi Gestión mecanizada del conocimiento matemático en Topología algebraica] #Tesis #ACL2
| |
− | * [http://bit.ly/faUvcE The first formalized math wiki is here] #MKM
| |
− | * [http://bit.ly/fAt2n2 Los matemáticos no buscan resultados, van tras la belleza] #CM
| |
− | * [http://bit.ly/hXvjFF Extending Sledgehammer with SMT Solvers] #Isabelle #SMT
| |
− | * [http://bit.ly/eTdbPY Book of proof] #Libro #DAO
| |
− | * [http://bit.ly/hTeyJl The General Triangle Is Unique] #RF #Isabelle
| |
− | * [http://bit.ly/fPmmPo NASA Formal Methods] #Libro #MF #Verificación
| |
− | * [http://bit.ly/eK1u3z How To Read A Mathematics Textbook] #Enseñanza
| |
− | * [http://bit.ly/eGDE9E Haskell for the cloud] #Haskell
| |
− | * [http://bit.ly/gx9OfA The OpenTheory Standard Theory Library] #Verificación
| |
− | * [http://bit.ly/ghnBkQ A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry] #RF #Coq
| |
− | * [http://bit.ly/esoyE5 Mechanical Support for Efficient Dissemination on the CAN Overlay Network] #Isabelle
| |
− | * [http://bit.ly/g0ybyb A Wiki for Formal Mathematics] #MKM
| |
− | * [http://bit.ly/eNHWj1 Recent Developments in Computing and Philosophy] #Prover9
| |
− | * [http://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2011_Constructive.pdf Constructive formalization of classical modal logic]. #Coq
| |
− | * [http://bit.ly/f7uyEs Numbers as Data Structures: The Prime Successor Function as Primitive] #Enseñanza
| |
− | * [http://bit.ly/iYb67t Proving Equality between Streams"] #Coq
| |
− | * [http://bit.ly/dOkauQ The limits of correctness] #Verificación
| |
− | * [http://bit.ly/e2aqGc A formal proof of the Riesz representation theorem] #RF #PVS
| |
− | * [http://bit.ly/lXvY1G A formal proof that π₁(S¹)=Z] #RF #Coq
| |
− | * [http://bit.ly/f0FX0O On a Strongly Normalizing STG Machine] #Tesis
| |
− | * [http://bit.ly/hi9u3T Balancing Weight-Balanced Trees] #Coq #Haskell
| |
− | * [http://bit.ly/gDCUy0 A Formal Programming Model of Orléans Skeleton Library] #Coq
| |
− | * [http://bit.ly/gxGyjq Formal Verification of a small real-time operating system] #Tesis #Isabelle
| |
− | * [http://bit.ly/io1joM Deus ex machina]. #Prover9
| |
− | * [http://bit.ly/jdhTBc Computationally-discovered simplification of the ontological argument]. #Prover9
| |
− | * [http://bit.ly/eI3roc Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)] #AR
| |
− | * [http://bit.ly/f9tTAC Heaps and Data Structures: A Challenge for Automated Provers] #AR
| |
− | * [http://bit.ly/jkEZGy Haskell: Not pure enough?] #Haskell
| |
− | * [http://bit.ly/lT7IZ3 Verified Stack-Based Genetic Programming via Dependent Types] #RF #Agda #IA
| |
− | * [http://bit.ly/lDrbjG Sorpresa sumando potencias de 2 en Haskell] #Haskell #V
| |
− | * [http://bit.ly/kzKmwS A List-Machine Benchmark for Mechanized Metatheory] #AR
| |
− | * [http://bit.ly/ls0jmQ The Locally Nameless Representation] #AR
| |
− | * [http://bit.ly/j1Ma1D Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem] #TFM #PVS
| |
− | * [http://bit.ly/lxkECl Solving Rubik's Cube Using SAT Solvers] #SAT
| |
− | * [http://bit.ly/kU11XQ Entusiasmo, clave del buen maestro] #Enseñanza
| |
− | * [http://slidesha.re/iwSxsW Programação Funcional: Novos Horizontes para a Expansão da Consciência] #PF
| |
− | * [http://bit.ly/lL64ln Computer certified efficient exact reals in Coq] #Coq
| |
− | * [http://bit.ly/ieX6gS Parallel and Concurrent Programming in Haskell] #Haskell
| |
− | * [http://bit.ly/lvyAWJ TRX: A Formally Verified Parser Interpreter] #Coq
| |
− | * [http://bit.ly/lgbo2i Computational Meta-Ethics: Towards the Meta-Ethical Robot] #Prover9
| |
− | * [http://bit.ly/j8R2cA Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover] #RF #Matita
| |
− | * [http://bit.ly/kYxElW ALPprolog — A New Logic Programming Method for Dynamic Domains] #PL
| |
− | * [http://bit.ly/mBQXgl Logical Formalization of Semantic Business Vocabulary and Rules"] #RC
| |
− | * [http://bit.ly/illSo The Proof is in the Pudding (The Changing Nature of Mathematical Proof)] #Libro
| |
− | * [http://goo.gl/JzUX7 Knowledge-Based Programs] #RF #Isabelle
| |
− | * [http://bit.ly/kH7Xz7 Elegance and Power] #Haskell
| |
− | * [http://bit.ly/iiAhk5 Validated Compilation through Logic] #Verificación
| |
− | * [http://bit.ly/jXmH4d Teaching Computational Logic: Technology-enhanced Learning and Animations] #Enseñanza
| |
− | * [http://bit.ly/k0HycO Sigma: An Integrated Development Environment for Formal Ontology] #RC
| |
− | * [http://bit.ly/m3Qmr3 Termination of Isabelle Functions via Termination of Rewriting] #AR #Isabelle
| |
− | * [http://bit.ly/koQ4Ti Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics] #AR
| |
− | * [http://bit.ly/jzGZo1 Rationality and Escalation in Infinite Extensive Games] #Libro #RF #Coq
| |
− | * [http://bit.ly/lHXxS8 Efficient Interactive Construction of Machine-Checked Protocol Security Proofs in the Context of Dynamically Compromising Adversaries] #TFM #RF #Isabelle
| |
− | * [http://bit.ly/iir2wI Specification and Verification: The Spec# Experience] #Verificación
| |
− | * [http://bit.ly/lhybds Formal Verification of Chess Endgames Tables] #HOL4 #IA
| |
− | * [http://bit.ly/l5BtTc Integrating Testing and Interactive Theorem Proving] #ACL2
| |
− | * [http://bit.ly/l5gjtf Conway’s Games and Some of Their Basic Properties] #Mizar
| |
− | * [http://bit.ly/jZeiPa A verified runtime for a verified theorem prover] #HOL4
| |
− | * [http://bit.ly/jnkpNT Modelling distributed cognition systems in PVS] #PVS
| |
− | * [http://bit.ly/kuY9Ad Three Chapters of Measure Theory in Isabelle/HOL] #RF #Isabelle
| |
− | * [http://bit.ly/kbX6ZI seL4 Enforces Integrity] #Verificación #Isabelle
| |
− | * [http://bit.ly/m4r6a7#RF Initial Semantics for higher-order typed syntax in Coq] #Coq
| |
− | * [http://bit.ly/lGZVoa Initial Semantics for higher-order typed syntax in Coq] #RF #Coq
| |
− | * [http://bit.ly/jXe3QN Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #RF #Coq
| |
− | * [http://bit.ly/mOh20v Specification of imperative languages using operational semantics in Coq] #RF #Coq
| |
− | * [http://bit.ly/mlftfm A First-Order Calculus for Allegories] #AR
| |
− | * [http://bit.ly/imjeTQ Generating Schemata of Resolution Proofs] #AR
| |
− | * [http://bit.ly/iGWaxr On the Generation of Positivstellensatz Witnesses in Degenerate Cases] #RF #Coq
| |
− | * [http://bit.ly/lAHBc0 Deciding Kleene Algebras in Coq] #RF #Coq
| |
− | * [http://bit.ly/lH7T3a Glasgow Haskell vs. Lispworks] #Haskell #Lisp
| |
− | * [http://bit.ly/jzm3hG On the expressive power of unit resolution] #AR
| |
− | * [http://bit.ly/jo9RKj Proceedings 15th International Refinement Workshop] #AR
| |
− | * [http://bit.ly/mLskMG Solving the Unsolvable] #AR
| |
− | * [http://bit.ly/kJTmix Type classes for efficient exact real arithmetic in Coq] #Coq
| |
− | * [http://bit.ly/lbXy2P Un problema de las olimpiadas rusas en Haskell] #Haskell #V
| |
− | * [http://bit.ly/lcO4n8 BDDs verified in a proof assistant] #Isabelle
| |
− | * [http://arxiv.org/pdf/1106.3685v3 Embedding and Automating Conditional Logics in Classical Higher-Order Logic]
| |
− | * [http://bit.ly/iJwaDm Incidence simplicial matrices formalized in Coq/SSReflect]. #RF #Coq
| |
− | * [http://bit.ly/mTuPbK What’s Fun About Teaching] #Enseñanza
| |
− | * [http://bit.ly/khYlHh Isabelle Repository for Relational and Algebraic Methods] #Isabelle
| |
− | * [http://bit.ly/kPQSDw Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL] #Isabelle
| |
− | * [http://bit.ly/kANpSp SAT solver of Howe & King as a logic program] #SAT #PL
| |
− |
| |
| == Lecturas comentadas == | | == Lecturas comentadas == |
| En esta sección se recogen los comentarios de los miembros del Grupo de algunas de las lecturas de publicaciones relacionadas con los temas de investigación del Grupo. | | En esta sección se recogen los comentarios de los miembros del Grupo de algunas de las lecturas de publicaciones relacionadas con los temas de investigación del Grupo. |