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

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 durante el mes 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. L’ordinateur au cœur de la découverte mathématique. #Divulgación
2. Últimos dos dígitos de (1+5^(2n+1))/6. #Haskell
3. Disparad contra la Ilustración. #Enseñanza
4. On the aesthetics of computer science. #Divulgación
5. Computing with hereditarily finite sequences. #Prolog #MKM
6. An interview with Stephen A. Cook. #Divulgación
7. Markov models. #Isabelle
8. Turing machines por J. Hopcroft #Clásico #Divulgación
9. The way forward for Computer Science in the U.K. #Enseñanza
10. Teaching semantics with a proof assistant: No more LSD trip proofs. #Enseñanza #Lógica #Isabelle
11. Enseñando deducción natural con Coq. #Enseñanza #Lógica #Coq
12. Formalisation en OWL pour vérifier les spécifications d’un environnement intelligent. #OWL #Prover9
13. Think complexity. #Sistemas_complejos #Python
14. Algorithmic graph theory. #Libro #Algorítmica #Sage
15. A simplified framework for first-order languages and its formalization in Mizar. #Tesis #Metalógica #Mizar
16. ProofPeer – A cloud-based interactive theorem proving system. #ProofPeer
17. Generic proof tools and finite group theory. #Tesis #Coq

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.

Read More “Lecturas del Grupo de Lógica Computacional (Enero de 2012)”