Lecturas del Grupo de Lógica Computacional (Junio de 2013)
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.
- Problemas sobre el 2013 en Haskell. #Haskell
- La sucesión de Perrin en Haskell. #Haskell
- Representación de 2ⁿ como 7x²+y² (con x e y impares) en Haskell #Haskell
- Computing square roots using the babylonian method. #Isabelle
- Formal verification of nonlinear inequalities with Taylor interval approximations. #HOL_Light
- Characteristic formulae for mechanized program verification. #Tesis #Coq
- Construction and stochastic applications of measure spaces in Higher-Order Logic. #Tesis #Isabelle
- A proof of Bertrand’s postulate. #Matita
- Trusting computations: a mechanized proof from partial differential equations to actual program. #Coq
- Formal construction of a set theory in Coq. #Tesis #Coq
- Rank-nullity theorem in linear algebra. #Isabelle #AFP
- GDT4MAS: a formal model and language to specify and verify agent-based complex systems. #PVS
- Kleene algebra. #AFP #Isabelle
- Information-theoretic analysis using theorem proving. #Tesis #HOL4
- Applying formal methods in software development. #Tesis #PVS
- Formalization and concretization of ordered networks. #Coq
- The design of a practical proof checker for a lazy functional language. #MProver #Haskell
- The formalization of syntax-based mathematical algorithms using quotation and evaluation
- A verified decision procedure for MSO on words based on derivatives of regular expressions. #Isabelle
- Statistical proof-patterns in Coq/SSReflect. #Coq
- Towards a logic-based unifying framework for computing.
- Termination tools in automated reasoning. #Tesis
- Matrices à blocs et en forme canonique. #Coq
- Automated verification of termination certificates. #Coq
- Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
- Towards self-verification of Isabelle’s Sledgehammer. #Isabelle
- A framework for the verification of certifying computations. #Isabelle
- A preliminary univalent formalization of the p-adic numbers. #Coq
- Algunos vínculos entre los teoremas de Gödel y Turing
- Formal computations and methods. #Tesis #HOL_Light
- Complex concept lattices for simulating human prediction in sport.
- MaSh: Machine learning for Sledgehammer. #Isabelle #ITP2013
- Une étude formelle de la théorie des calculs locaux à l’aide de l’assistant de preuve Coq. #Tesis #Coq
- Temas de programación lógica e inteligencia artificial. #Prolog
- Una curiosa propiedad del 123 en Haskell. #Haskell
- A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2. #Isabelle #ACL2
- Otra curiosa propiedad del 123 en Haskell. #Haskell
- Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos. #PVS
- Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle
- ML4PG: proof-mining in Coq. #Coq
- Concept-forming operators on multilattices. #AFC
- The gauge integral theory in HOL4. #HOL4
- The Picard algorithm for ordinary differential equations in Coq. #Coq
- Mechanising Turing machines and computability theory in Isabelle/HOL. #Isabelle #ITP2013
- Formal reasoning about finite-state discrete-time Markov chains in HOL. #HOL
- Verifying a plaftorm for digital imaging: a multi-tool strategy. #Coq #ACL2
- Deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
- Formalized algebraic numbers: construction and first-order theory. #Tesis #Coq
- Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
- A hierarchy of mathematical structures in ACL2. #ACL2
- Programming and reasonning with powerlists in Coq. #Coq
- Formalization of the complex number theory in HOL4. #HOL4
- Formalizing the confluence of orthogonal rewriting systems. #PVS
- Homotopy limits in Coq. #Coq
- Data refinement in Isabelle/HOL. #Isabelle_HOL
- Formalization of real analysis: A survey of proof assistants and libraries. #ITP
- AI over large formal knowledge bases: The first decade. #Mizar
- ForMaRE-formal mathematical reasoning in economics.
- A fully verified executable LTL model checker. #Isabelle
- Automating inductive proofs using theory exploration. #Haskell #HipSpec
- One logic to use them all. #CADE24 #Why3
- Square root and division elimination in PVS. #PVS #ITP2013
- Experience report: Teaching Haskell to the masses. #Haskell
- Coinductive pearl: Modular first-order logic completeness. #Isabelle
- Formalization of incremental simplex algorithm by stepwise refinement. #Isabelle
- Les assistants de preuve, ou comment avoir confiance en ses démonstrations. #DAO
- Developing an auction theory toolbox. #Isabelle
- Formalizing Knuth-Bendix orders and Knuth-Bendix completion. #Isabelle
- A formal proof of Kruskal’s tree theorem in Isabelle/HOL. #Isabelle
- A constructive theory of regular languages in Coq. #Coq
- A machine-checked proof of the odd order theorem. #Coq
- Graph theory. #Isabelle #AFP
- A macro for reusing abstract functions and theorems. #ACL2
- Light-weight containers for Isabelle: efficient, extensible, nestable. #Isabelle
- Formalizing Turing machines. #Matita
- A certified reduction strategy for homological image processing. #Coq
- On the formalization of continuous-time Markov chains in HOL. #HOL
- A Web interface for Isabelle: The next generation. #Isabelle #CICM2013
- Verifying refutations with extended resolution. #ACL2
- Type classes and filters for mathematical analysis in Isabelle/HOL. #Isabelle
- Mechanical verification of SAT refutations with extended resolution. #ACL2 #ITP2013
- The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups). #Coq
- Automatic data refinement. #Isabelle #ITP2013
- Certified HLints with Isabelle/HOLCF-Prelude. #Isabelle
- Theorem of three circles in Coq. #Coq
- A Haskell library for term rewriting. #Haskell
- Formal mathematics on display: A wiki for Flyspeck. #HOL_Light
- Solveurs CP(FD) vérifiés formellement. #Coq
- Formalizing bounded increase. #Isabelle
- Certified symbolic manipulation: Bivariate simplicial polynomials. #ACL2
- The formalization of syntax-based mathematical algorithms using quotation and evaluation.
- Homotopy type theory: Univalent foundations of mathematics. #Libro
- Mathematicians think like machines for perfect proofs.
- Certifying homological algorithms to study biomedical images. #Tesis #Coq #Haskell
- Formalizing cut elimination of coalgebraic logics in Coq. #Coq
La recopilación de las lecturas anteriores se encuentra aquí.