Lecturas del Grupo de Lógica Computacional (Junio de 2013)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de enero de 2013. La anterior recopilación fue la de diciembre de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Problemas sobre el 2013 en Haskell. #Haskell
  2. La sucesión de Perrin en Haskell. #Haskell
  3. Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
  4. Computing square roots using the babylonian method. #Isabelle
  5. Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
  6. Characteristic formulae for mechanized program verification. #Tesis #Coq
  7. Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
  8. A proof of Bertrand’s postulate. #Matita
  9. Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
  10. Formal construction of a set theory in Coq. #Tesis #Coq
  11. Rank-nullity theorem in linear algebra. #Isabelle #AFP
  12. GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
  13. Kleene algebra. #AFP #Isabelle
  14. Information-theoretic analysis using theorem proving. #Tesis #HOL4
  15. Applying formal methods in software development. #Tesis #PVS
  16. Formalization and concretization of ordered networks. #Coq
  17. The design of a practical proof checker for a lazy functional language. #MProver #Haskell
  18. The formalization of syntax-based mathematical algorithms using quotation and evaluation
  19. A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
  20. Statistical proof-patterns in Coq/SSReflect. #Coq
  21. Towards a logic-based unifying framework for computing.
  22. Termination tools in automated reasoning. #Tesis
  23. Matrices à blocs et en forme canonique. #Coq
  24. Automated verification of termination certificates. #Coq
  25. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  26. Towards self-verification of Isabelle’s Sledgehammer. #Isabelle
  27. A framework for the verification of certifying computations. #Isabelle
  28. A preliminary univalent formalization of the p-adic numbers. #Coq
  29. Algunos vínculos entre los teoremas de Gödel y Turing
  30. Formal computations and methods. #Tesis #HOL_Light
  31. Complex concept lattices for simulating human prediction in sport.
  32. MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
  33. Une étude formelle de la théorie des calculs locaux à l’aide de l’assistant de preuve Coq. #Tesis #Coq
  34. Temas de programación lógica e inteligencia artificial. #Prolog
  35. Una curiosa propiedad del 123 en Haskell. #Haskell
  36. A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
  37. Otra curiosa propiedad del 123 en Haskell. #Haskell
  38. Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
  39. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
  40. ML4PG: proof-mining in Coq. #Coq
  41. Concept-forming operators on multilattices. #AFC
  42. The gauge integral theory in HOL4. #HOL4
  43. The Picard algorithm for ordinary differential equations in Coq. #Coq
  44. Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
  45. Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
  46. Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
  47. Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
  48. Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
  49. Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
  50. A hierarchy of mathematical structures in ACL2. #ACL2
  51. Programming and reasonning with powerlists in Coq. #Coq
  52. Formalization of the complex number theory in HOL4. #HOL4
  53. Formalizing the confluence of orthogonal rewriting systems. #PVS
  54. Homotopy limits in Coq. #Coq
  55. Data refinement in Isabelle/HOL. #Isabelle_HOL
  56. Formalization of real analysis: A survey of proof assistants and libraries. #ITP
  57. AI over large formal knowledge bases: The first decade. #Mizar
  58. ForMaRE-formal mathematical reasoning in economics.
  59. A fully verified executable LTL model checker. #Isabelle
  60. Automating inductive proofs using theory exploration. #Haskell #HipSpec
  61. One logic to use them all. #CADE24 #Why3
  62. Square root and division elimination in PVS. #PVS #ITP2013
  63. Experience report: Teaching Haskell to the masses. #Haskell
  64. Coinductive pearl: Modular first-order logic completeness. #Isabelle
  65. Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
  66. Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
  67. Developing an auction theory toolbox. #Isabelle
  68. Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
  69. A formal proof of Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  70. A constructive theory of regular languages in Coq. #Coq
  71. A machine-checked proof of the odd order theorem. #Coq
  72. Graph theory. #Isabelle #AFP
  73. A macro for reusing abstract functions and theorems. #ACL2
  74. Light-weight containers for Isabelle: efficient, extensible, nestable. #Isabelle
  75. Formalizing Turing machines. #Matita
  76. A certified reduction strategy for homological image processing. #Coq
  77. On the formalization of continuous-time Markov chains in HOL. #HOL
  78. A Web interface for Isabelle: The next generation. #Isabelle #CICM2013
  79. Verifying refutations with extended resolution. #ACL2
  80. Type classes and filters for mathematical analysis in Isabelle/HOL. #Isabelle
  81. Mechanical verification of SAT refutations with extended resolution. #ACL2 #ITP2013
  82. The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). #Coq
  83. Automatic data refinement. #Isabelle #ITP2013
  84. Certified HLints with Isabelle/HOLCF-Prelude. #Isabelle
  85. Theorem of three circles in Coq. #Coq
  86. A Haskell library for term rewriting. #Haskell
  87. Formal mathematics on display: A wiki for Flyspeck. #HOL_Light
  88. Solveurs CP(FD) vérifiés formellement. #Coq
  89. Formalizing bounded increase. #Isabelle
  90. Certified symbolic manipulation: Bivariate simplicial polynomials. #ACL2
  91. The formalization of syntax-based mathematical algorithms using quotation and evaluation.
  92. Homotopy type theory: Univalent foundations of mathematics. #Libro
  93. Mathematicians think like machines for perfect proofs.
  94. Certifying homological algorithms to study biomedical images. #Tesis #Coq #Haskell
  95. Formalizing cut elimination of coalgebraic logics in Coq. #Coq

La recopilación de las lecturas anteriores se encuentra aquí.

Lecturas del Grupo de Lógica Computacional (Diciembre de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de diciembre de 2012. La anterior recopilación fue la de noviembre de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Verifying probabilistic correctness in Isabelle with pGCL. #Isabelle
  2. Formalization of a strategy for the KRK chess endgame. #Coq
  3. Formalization and implementation of algebraic methods in Geometry. #Isabelle
  4. Formal verification of conflict detection algorithms for arbitrary trajectories. #PVS
  5. Learning-assisted automated reasoning with Flyspeck. #Mizar
  6. Deductive formal verification of embedded systems. #Tesis #Coq
  7. Verification of redecoration for infinite triangular matrices using coinduction. #Coq
  8. Représentation coinductive des graphes. #Tesis #Coq
  9. Formal mathematics for mathematicians.
  10. The HOL Light theory of euclidean space. #HOLLight
  11. Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar. #Mizar
  12. The Gödel completeness theorem for uncountable languages. #Mizar
  13. Machine learning in Proof General: Interfacing interfaces. #Coq
  14. Interactive verification of Markov chains: Two distributed protocol case studies. #Isabelle
  15. Du rêve à la réalité des preuves. (Interstices, 2012) #Divulgación #DAO
  16. Interactive theorem proving, automated reasoning, and mathematical computation

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.

Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de septiembre de 2012. La anterior recopilación fue la de agosto de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

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

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.

Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el mes de marzo de 2012. La anterior recopilación fue la de febrero de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Automatic proofs and refutations for higher-order logic. #Tesis #Isabelle
  2. On theorem prover-based testing. #Isabelle
  3. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. #Coq
  4. Tips on Haskell. #Tutorial #Haskell
  5. Enfragmo: A system for modelling and solving search problems with logic. #SAT
  6. Logic & reasoning: from Aristotle to Intel. #Panorama #Lógica
  7. Deciding Kleene Algebras in Coq. #Coq
  8. Vérification semi-automatique de primitives cryptographiques. #Tesis #Coq
  9. Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model. #PVS
  10. Formal error analysis and verification of the frequency domain equalizer. #HOL
  11. Introduction to the Coq proof-assistant for practical software verification. #Tutorial #Coq
  12. Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination #Coq
  13. Mathematics for Computer Science. #Libro
  14. Proving possibilistic, probabilistic noninterference. #Isabelle
  15. Decision procedures in Algebra and Logic (Reading material). #Libro #Lógica
  16. A formalization of the theorem of existence of first-order most general unifiers. #PVS
  17. The worldʼs shortest correct exact real arithmetic program?. #PVS #Haskell
  18. Kleene algebra, rewriting modulo AC and circuits in Coq. #Tesis #Coq
  19. Deriving a fast inverse of the generalized Cantor n-tupling bijection. #Prolog
  20. PVS linear algebra libraries for verification of control software algorithms in C/ACSL. #PVS
  21. Generating verifiable Java code from verified PVS specifications. #PVS
  22. Haskell gets argumentative. #Haskell #Lógica @IA
  23. Induction and recursion. #Fundamentos
  24. A formal proof of Sasaki-Murao algorithm. #Coq
  25. Essential incompleteness of arithmetic verified by Coq. #Coq
  26. Incompleteness & completeness: Formalizing logic and analysis in type theory. #Tesis #Coq
  27. Well-quasi-orders. #Isabelle
  28. Analyse et Conception Formelles (Software formal analysis and design). #Curso #Isabelle
  29. Programming and proving in Isabelle/HOL. #Isabelle
  30. Numerical analysis of ordinary differential equations. #Isabelle
  31. Inductive study of confidentiality. #AFP #Isabelle
  32. Formal correctness of security protocols. #Libro #Isabelle
  33. Stuttering equivalence. #AFP
  34. HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving. #Tesis #Haskell
  35. A string of pearls: proofs of Fermat’s little theorem. #HOL4
  36. Separation logic: A logic for shared mutable data structures.
  37. Local action and abstract separation logic.
  38. Separation algebra. #Isabelle
  39. Using PVS to support the analysis of distributed cognition systems. #PVS
  40. Formal verification of the heavy hitter problem. #HOL
  41. Formal probabilistic analysis using theorem proving. #Tesis #HOL
  42. Proving equational Haskell properties using automated theorem provers. #Haskell #Thesis
  43. Accessible integrated formal reasoning environments in classroom instruction of mathematics.
  44. Designing accessible lightweight formal verification systems.
  45. Artificial intelligence: from fantasy to reality. #IA
  46. HipSpec: Automating inductive proofs of program properties. #Haskell
  47. Supplementary material for “Thinking as computation”. #IA #Prolog
  48. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  49. Bridging the gap: Automatic verified abstraction of C
  50. Computing in Cantor’s paradise with λZFC.
  51. Thoughts on gamifying textbooks.
  52. Isabelle/Circus: A process specification and verification environment. #Isabelle
  53. Isabelle/Circus. #Isabelle
  54. Wave equation numerical resolution: a comprehensive mechanized proof of a C program #Coq
  55. Large-scale formal verification in practice: A process perspective. #Isabelle
  56. A framework for formally verifying software transactional memory algorithms. #PVS
  57. Rigorous polynomial approximation using Taylor models in Coq. #Coq
  58. Rigorous polynomial approximations and applications. #Tesis #Coq
  59. Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project. #MKM
  60. Formalizing Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
  61. Verifying an algorithm computing discrete vector fields for digital imaging. #Coq
  62. Formal verification of monad transformers. #Isabelle
  63. HALO: Haskell to logic through denotational semantics. #Haskell
  64. Interactive proof: Introduction to Isabelle/HOL. #Tutorial #Isabelle
  65. Formalization of an efficient representation of Bernstein polynomials and applications to global optimization #PVS
  66. Lifting and transfer: A modular design for quotients in Isabelle/HOL. #Isabelle
  67. Meta-theory à la carte. #Coq
  68. Mechanization of an algorithm for deciding KAT terms equivalence. #Coq
  69. ¿Es posible construir software que no falle?. #Verificación
  70. Proving the impossibility of trisecting an angle and doubling the cube. #Isabelle
  71. Formal specification and verification of well-formedness in business process product lines. #PVS
  72. Compiling concurrency correctly (Verifying software transactional memory). #Tesis #Agda #Haskell
  73. Représentation coinductive des graphes. #Tesis #Coq
  74. Formalizing adequacy: A case study for higher-order abstract syntax. #Isabelle
  75. Algorithms in games evolving in time: Winning strategies based on testing. #Isabelle
  76. A certified JavaScript interpreter. #Coq
  77. Formalization of Shannon’s theorems in SSReflect-Coq. #Coq
  78. Abstract interpretation of annotated commands. #Isabelle
  79. Construction of real algebraic numbers in Coq. #Coq
  80. Correctness of pointer manipulating algorithms illustrated by a verified BDD construction. #Isabelle
  81. Towards provably robust watermarking. #Coq
  82. Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL. #Isabelle
  83. Formalizing an abstract algebra textbook in Isabelle/HOL. #Isabelle
  84. Numerical analysis of ordinary differential equations in Isabelle/HOL. #Isabelle
  85. A refinement-based approach to computational algebra in Coq. #Coq
  86. Coherent and strongly discrete rings in type theory. #Coq
  87. Logic + control: An example of program construction. #Prolog
  88. Deriving a fast inverse of the generalized Cantor N-tupling bijection. #Prolog
  89. Formalization and verification of number theoretic algorithms using the Mizar proof checker. #Mizar

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.

Lecturas del Grupo de Lógica Computacional (Febrero de 2012)

PorJosé A. Alonso

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de Febrero de 2012. La anterior recopilación fue la de Enero de 2012.

La recopilación está ordenada por la fecha de su publicación en la lista. Al
final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

  1. Emergence and refinement. #Sistemascomplejos
  2. Formalizing a hierarchical file system. #PVS
  3. Etude et formalisation de la méthode de Wu dans Coq. #Tesis #Coq
  4. Using PVS to investigate incidents through the lens of distributed ORG-LIST-END-MARKER cognition. #PVS
  5. Formal system verification for trustworthy embedded systems. #Isabelle
  6. The mechanical verification of a DPLL-based satisfiability solver. #PVS
  7. Innovación en el tratamiento de la información desde la Ingeniería del ORG-LIST-END-MARKER Conocimiento (1/2)
  8. Innovación en el tratamiento de la información desde la Ingeniería del ORG-LIST-END-MARKER Conocimiento (2/2)
  9. A unified treatment of syntax with binders.
  10. The age of Big Data. #IA
  11. Crear moléculas desde cero sin la endiablada ecuación de Schrödinger. #IA
  12. Refinement for monadic programs. #Isabelle
  13. Dijkstra’s shortest path algorithm. #Isabelle
  14. Computational topology.
  15. Category theory and functional programming. #Haskell
  16. The artist in the computer scientist: more humanity to our research.
  17. When formal systems kill: computer ethics and formal methods.
  18. Mathematics in the age of the Turing machine. #Panorama #DAO
  19. The reflective Milawa theorem prover is sound. #ACL2 #HOL4
  20. Ejercicios de “Informática de 1º de Matemáticas” (2011-12). #Haskell
  21. Temas de programación funcional con Haskell (curso 2011-12). #Haskell
  22. Executable transitive closures. #Isabelle