Categoría: Lecturas

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.

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional desde el 1 de Octubre de 2011 hasta el 7 de Enero de 2012. La anterior recopilación fue la de Septiembre de 2011

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.

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional. 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. Razonamiento formalizado para la enseñanza de las matemáticas. [#Vestigium, #Enseñanza]
2. The Ideal Mathematician. [#Humor]
3. El problema de las puertas en Haskell. [#Haskell]
4. Metadata for a mathematical wiki: Initial experiments. [#Mizar]
5. Logical Verification. [#Coq]
6. Formal proofs for theoretical properties of Newton’s method. [#Coq]
7. Formalisation de la logique de description ALC dans l’assistant de preuve Coq. [#Coq, #ALC]
8. Vérification d’une méthode de preuve pour la logique de description ALC. [#Isabelle. #ALC]
9. A critique of Abelson and Sussman or why calculating is better than scheming. [#Haskell, #Lisp]
10. Experiments with computable matrices in the Coq system. [#Coq]
11. Computing the homology of groups: the geometric way. [#Kenzo]
12. Peut-on faire des mathématiques avec un ordinateur?. [#Matemática computacional]
13. The Theory Behind TheoryMind. [#Isabelle]
14. Provably correct conflict prevention bands algorithms. [#PVS]
15. Peut-on avoir confiance en l’informatique?. [#Verificación]
16. Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011). [#GLC, #Vestigium]
17. Automated theorem provers a practical tool for the working mathematician. [#DAO, #Vestigium]
18. Intellectual Freedom. [#Humor]
19. Ciencia china ‘duplicada’ en Galicia. [#Sociología]
20. Expresiones aritméticas mediante tipos abstracto de datos y polinomios. [#Haskell, #Vestigium]
21. A verified runtime for a verified theorem prover. [#ACL2]
22. A Framework for Automated and Certified Refinement Steps. [#Isabelle]
23. Descomposiciones en sumas de cuadrados en Haskell. [#Haskell, #Vestigium]
24. Interactive Proof Introduction to IsabelleHOL. [#Isabelle]
25. Coq au vin (The Coq proof assistant and the Curry-Howard correspondence) [#Coq]
26. Hardware languages and proof. [#Tesis, #PVS, #SAL]