Diferencia entre revisiones de «Lecturas»
(→Lecturas del 27-Oct-2010 al 1-Jul-2011) |
(→Lecturas del 27-Oct-2010 al 1-Jul-2011) |
||
| Línea 3: | Línea 3: | ||
=== Lecturas del 27-Oct-2010 al 1-Jul-2011 === | === 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] Reduced Ordered Binary Decision Diagram with Implied Literals: A New knowledge Compilation Approach http://goo.gl/FoL94 #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 == | ||
Revisión del 18:14 27 abr 2013
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
+ Ejercicios de programación en Haskell #Haskell #V + El valor del fracaso digno #CM + Computational science: ... Error (... why scientific programming does not compute) #Verificación + El tipo abstracto de datos de las pilas en Haskell #Haskell #V + The free-form linguistics revolution in mathematica + A preliminary survey on functional programming #PF + Desarrollo del comando wc de Unix en Haskell #Haskell #V + Lógica Computacional en Sevilla (30 años en una hora) #V + Problema sobre números naturales #Haskell #V + Rompecabeza de Ullman en Haskell #Haskell #V + Lisp bot wins Google AI challenge — Will Lisp win in the semantic web, too? #Lisp #IA + Decálogo de la didáctica matemática #Enseñanza #V + El decálogo del profesor (según Polya) #Enseñanza #V + Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers en #Libro #AR + Parallelizing a CLIPS-based course timetabling expert system #SE + Certifying compilers using higher-order theorem provers as certificate checkers #Verificación #V + Teorías y aplicaciones #V + Does Godel's theorem matter to mathematics? + Distributed SAT #SAT + Semantic web reasoners and languages #WS + El 2011 y los números primos (en Haskell) #Haskell #V + The Dialectica interpertation in Coq #Coq + Errores aritméticos en Haskell y en Lisp #Haskell #Lisp #V + Why Lisp is a big hack (and haskell is doomed to succeed) #Lisp #Haskell + ProofWiki y la verificación de las demostraciones matemáticas #Verificación #MKM #V + A quick and gentle guide to constraint logic programming via ECLiPSe #PL #Restricciones + A language for mathematical knowledge management #MKM + Automated inference of finite unsatisfiability #AR + The free vector space on a type http://bit.ly/e9c5Zl #Haskell + Formal methods applied to a floating-point number system #Z + A machine-checked theory of floating point arithmetic #HOL_Light + Formal verification of floating point trigonometric functions #HOL_Light + A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor #ACL2 + A Generic Library for Floating-Point Numbers and Its Application to Exact Computing #Coq. + A High-Level Formalization of Floating-Point Numbers in PVS #PVS + Formal verification of floating-point programs #Coq + The pitfalls of verifying floating-point computations #Verificación + Floats and Ropes: A Case Study for Formal Numerical Program Verification #Coq. + Algorithms Take Control of Wall Street #IA + Formal reliability analysis of combinational circuits using theorem proving #HOL + Determinación, esperanza y éxitos en la resolución de problemas #Enseñanza #V + Lectures in Game Theory for Computer Scientists #Libro + Reactive Valuations #TFM + Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet + Algunas aplicaciones de las bases de Groebner + Programación funcional con Haskell #Libro #Haskell + Certifying compilers using higher-order theorem provers as certificate checker #Isabelle #Coq + El tipo abstracto de datos de las colas en Haskell #Haskell #V + Deducción natural en lógica proposicional con Isabelle/Isar #Isabelle #V + Deducción natural en lógica de primer orden con Isabelle/Isar #Isabelle #V + fKenzo: A user interface for computations in Algebraic Topology + A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. #Isabelle + El tipo abstracto de datos de las colas de prioridad en Haskell #Haskell #V + Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering? #Verificación + El próximo después de 1811 #Haskell #V + Humanos más capaces y robots que están en las nubes #IA + Charming Proofs: A Journey Into Elegant Mathematics #Libro #DAO + Functional Binomial Queues #RF #Isabelle + Lower Semicontinuous Functions #RF #Isabelle + Lógica Informática (2010-11) #V + Inconsistent heuristics in theory and practice #IA + On proof and progress in mathematics #CM + Artificial Intelligence (Foundations of Computational Agents) #Libro #IA + Are Mathematicians In Jeopardy? #IA + Give me that good old-fashioned AI #IA + Building Watson: An Overview of the DeepQA Project #IA + Software verification turns maintstream #Verificación + Formalising, improving, and reusing the Java Module System http://bit.ly/dF68vF #Tesis #Isabelle + SMT solvers: new oracles for the HOL theorem prover #SMT #HOL4 + Isabelle como un lenguaje funcional #Isabelle #V + El tipo abstracto de datos de las pilas en Haskell #Haskell #V + El tipo abstracto de datos de las colas en Haskell #Haskell #V + Executable Transitive Closures of Finite Relations #RF #Isabelle + Solución española para un problema de John Nash Reduced Ordered Binary Decision Diagram with Implied Literals: A New knowledge Compilation Approach http://goo.gl/FoL94 #AR + Teaching FP to freshmen #Enseñanza #PF + Introduction to Artificial Intelligence #Libro #IA + La Universidad Carnegie-Mellon elimina la programación OO de su primer curso #Enseñanza + Experience Report: Functional Programming through Deep Time (Modeling the first complex ecosystems on Earth) #Haskell + A Comparative Study on ILP-based Concept Discovery Systems #ILP + Logic-Based Artificial Intelligence #Libro #IA + A Formalization of the C99 Standard in HOL, Isabelle and Coq #HOL #Isabelle #Coq + Formal methods in agent-oriented software engineering #MF + The cognitive agents specification language and verification environment #Verificación + Software Bugs and Scientific Progress #Verificación + Representing model theory in a type-theoretical logical framework #RF #Twelfe + Towards a verification framework for faulty message passing systems in PVS #PVS + Por qué y cómo se hace investigación en matemáticas #CM + Introduction to newLISP #Libro #Lisp + Verified Firewall Policy Transformations for Test Case Generation #Isabelle + An Approach to Modular and Testable Security Models of Real-world Health-care Applications #Isabelle + Psi-calculi: a framework for mobile processes with nominal data and logic #Isabelle + Artificial Intelligence and Human Thinking #IA + Simplification Rules for Intuitionistic Propositional Tableaux #AR + A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free #ACL2 + Gestión mecanizada del conocimiento matemático en Topología algebraica #Tesis #ACL2 + The first formalized math wiki is here #MKM + Los matemáticos no buscan resultados, van tras la belleza #CM + Extending Sledgehammer with SMT Solvers #Isabelle #SMT + Book of proof #Libro #DAO + The General Triangle Is Unique #RF #Isabelle + NASA Formal Methods #Libro #MF #Verificación + How To Read A Mathematics Textbook #Enseñanza + Haskell for the cloud #Haskell + The OpenTheory Standard Theory Library #Verificación + A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry #RF #Coq + Mechanical Support for Efficient Dissemination on the CAN Overlay Network #Isabelle + A Wiki for Formal Mathematics #MKM + Recent Developments in Computing and Philosophy #Prover9 + Constructive formalization of classical modal logic. #Coq + Numbers as Data Structures: The Prime Successor Function as Primitive #Enseñanza + Proving Equality between Streams" #Coq + The limits of correctness #Verificación + A formal proof of the Riesz representation theorem #RF #PVS + A formal proof that π₁(S¹)=Z #RF #Coq + On a Strongly Normalizing STG Machine #Tesis + Balancing Weight-Balanced Trees #Coq #Haskell + A Formal Programming Model of Orléans Skeleton Library #Coq + Formal Verification of a small real-time operating system #Tesis #Isabelle + Deus ex machina. #Prover9 + Computationally-discovered simplification of the ontological argument. #Prover9 + Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II) #AR + Heaps and Data Structures: A Challenge for Automated Provers #AR + Haskell: Not pure enough? #Haskell + Verified Stack-Based Genetic Programming via Dependent Types #RF #Agda #IA + Sorpresa sumando potencias de 2 en Haskell #Haskell #V + A List-Machine Benchmark for Mechanized Metatheory #AR + The Locally Nameless Representation #AR + Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem #TFM #PVS + Solving Rubik's Cube Using SAT Solvers #SAT + Entusiasmo, clave del buen maestro #Enseñanza + Programação Funcional: Novos Horizontes para a Expansão da Consciência #PF + Computer certified efficient exact reals in Coq #Coq + Parallel and Concurrent Programming in Haskell #Haskell + TRX: A Formally Verified Parser Interpreter #Coq + Computational Meta-Ethics: Towards the Meta-Ethical Robot #Prover9 + Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover #RF #Matita + ALPprolog — A New Logic Programming Method for Dynamic Domains #PL + Logical Formalization of Semantic Business Vocabulary and Rules" #RC + The Proof is in the Pudding (The Changing Nature of Mathematical Proof) #Libro + Knowledge-Based Programs #RF #Isabelle + Elegance and Power #Haskell + Validated Compilation through Logic #Verificación + Teaching Computational Logic: Technology-enhanced Learning and Animations #Enseñanza + Sigma: An Integrated Development Environment for Formal Ontology #RC + Termination of Isabelle Functions via Termination of Rewriting #AR #Isabelle + Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics #AR + Rationality and Escalation in Infinite Extensive Games #Libro #RF #Coq + Efficient Interactive Construction of Machine-Checked Protocol Security Proofs in the Context of Dynamically Compromising Adversaries #TFM #RF #Isabelle + Specification and Verification: The Spec# Experience #Verificación + Formal Verification of Chess Endgames Tables #HOL4 #IA + Integrating Testing and Interactive Theorem Proving #ACL2 + Conway’s Games and Some of Their Basic Properties #Mizar + A verified runtime for a verified theorem prover #HOL4 + Modelling distributed cognition systems in PVS #PVS + Three Chapters of Measure Theory in Isabelle/HOL #RF #Isabelle + seL4 Enforces Integrity #Verificación #Isabelle + Initial Semantics for higher-order typed syntax in Coq #Coq + Initial Semantics for higher-order typed syntax in Coq #RF #Coq + Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #RF #Coq + Specification of imperative languages using operational semantics in Coq #RF #Coq + A First-Order Calculus for Allegories #AR + Generating Schemata of Resolution Proofs #AR + On the Generation of Positivstellensatz Witnesses in Degenerate Cases #RF #Coq + Deciding Kleene Algebras in Coq #RF #Coq + Glasgow Haskell vs. Lispworks #Haskell #Lisp + On the expressive power of unit resolution #AR + Proceedings 15th International Refinement Workshop #AR + Solving the Unsolvable #AR + Type classes for efficient exact real arithmetic in Coq #Coq + Un problema de las olimpiadas rusas en Haskell #Haskell #V + BDDs verified in a proof assistant #Isabelle + Embedding and Automating Conditional Logics in Classical Higher-Order Logic + Incidence simplicial matrices formalized in Coq/SSReflect. #RF #Coq + What’s Fun About Teaching #Enseñanza + Isabelle Repository for Relational and Algebraic Methods #Isabelle + Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL #Isabelle + SAT solver of Howe & King as a logic program #SAT #PL
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.
- K.R. Apt y M.G. Wallace (2007)
Constraint Logic Programming using Eclipse. - B. Buchberger (1991)
Logic for Computer Science - M. Cayli, A. G. Karatop, E. Kavlak, H. Kaynar, F. Ture y E. Erdem. (2007)
Solving challenging grid puzzles with answer set programming. - G. Gonthier (2008)
Formal Proof: The Four-Color Theorem - T.C. Hales (2008)
Formal Proof - J. Harrison (1998)
Formalizing basic first order model theory - J. Harrison (2007)
A short survey of automated reasoning - J. Harrison (2008)
Formal Proof: Theory and Practice - C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks y R. de Vrijer (2008)
Deduction using the ProofWeb system. - M. Krötzsch, D. Vrandecic, M. Völkel, H. Haller y R. Studer (2007)
Semantic Wikipedia. - N. Magaud, J Narboux y P. Schreck (2009)
Formalizing Desargues' theorem in Coq using ranks. - J. Rehmeyer (2008)
How to (really) trust a mathematical proof. - C.E. Veni Madhavan (2005)
Mathematics and computer science: The interplay. - P. Marić y P. Janicić (2009)
Formal Correctness Proof for DPLL Procedure.
