Lecturas

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. #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.

1. K.R. Apt y M.G. Wallace (2007)
   Constraint Logic Programming using Eclipse.
2. B. Buchberger (1991)
   Logic for Computer Science
3. M. Cayli, A. G. Karatop, E. Kavlak, H. Kaynar, F. Ture y E. Erdem. (2007)
   Solving challenging grid puzzles with answer set programming.
4. G. Gonthier (2008)
   Formal Proof: The Four-Color Theorem
5. T.C. Hales (2008)
   Formal Proof
6. J. Harrison (1998)
   Formalizing basic first order model theory
7. J. Harrison (2007)
   A short survey of automated reasoning
8. J. Harrison (2008)
   Formal Proof: Theory and Practice
9. C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks y R. de Vrijer (2008)
   Deduction using the ProofWeb system.
10. M. Krötzsch, D. Vrandecic, M. Völkel, H. Haller y R. Studer (2007)
    Semantic Wikipedia.
11. N. Magaud, J Narboux y P. Schreck (2009)
    Formalizing Desargues' theorem in Coq using ranks.
12. J. Rehmeyer (2008)
    How to (really) trust a mathematical proof.
13. C.E. Veni Madhavan (2005)
    Mathematics and computer science: The interplay.
14. P. Marić y P. Janicić (2009)
    Formal Correctness Proof for DPLL Procedure.