Lecturas del año 2013

Lecturas de enero de 2013

• 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. #RA
• Termination tools in automated reasoning. #Tesis #RA

Lecturas de febrero de 2013

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

Lecturas de marzo de 2013

• 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
• DAO: Ejercicios de deducción natural en lógica proposicional con Isabelle/HOL. #Isabelle
• DAO: Ejercicios de argumentación proposicional con Isabelle/HOL. #Isabelle
• Knowledge representation, reasoning, and the design of intelligent agents. #Libro #ASP
• DAO: Deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
• DAO: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL. #Isabelle
• A hierarchy of mathematical structures in ACL2. #ACL2
• DAO: Argumentación en lógica de primer orden con Isabelle/HOL (1). #Isabelle
• DAO: Argumentación en lógica de primer orden con Isabelle/HOL (2). #Isabelle
• Programming and reasonning with powerlists in Coq. #Coq
• Formalization of the complex number theory in HOL4. #HOL4

Lecturas de abril de 2013

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