Diferencia entre revisiones de «Lecturas del año 2013»
| Línea 1: | Línea 1: | ||
== Lecturas de Enero de 2013 == | == Lecturas de Enero de 2013 == | ||
| − | |||
* [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell | * [http://www.glc.us.es/~jalonso/ejerciciosI1M2012G2/index.php5/Relaci%C3%B3n_13 Problemas sobre el 2013 en Haskell]. #Haskell | ||
* [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell | * [http://www.glc.us.es/~jalonso/vestigium/la-sucesion-de-perrin-en-haskell/ La sucesión de Perrin en Haskell]. #Haskell | ||
| Línea 21: | Línea 20: | ||
* [http://www21.in.tum.de/~traytel/papers/mso/mso.pdf A verified decision procedure for MSO on words based on derivatives of regular expressions]. #Isabelle | * [http://www21.in.tum.de/~traytel/papers/mso/mso.pdf A verified decision procedure for MSO on words based on derivatives of regular expressions]. #Isabelle | ||
* [http://arxiv.org/abs/1301.6039 Statistical proof-patterns in Coq/SSReflect]. #Coq | * [http://arxiv.org/abs/1301.6039 Statistical proof-patterns in Coq/SSReflect]. #Coq | ||
| − | * [http://arxiv.org/pdf/1301.6905v1 Towards a logic-based unifying framework for computing]. | + | * [http://arxiv.org/pdf/1301.6905v1 Towards a logic-based unifying framework for computing]. #RA |
| − | * [http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/SW13.pdf Termination tools in automated reasoning]. #Tesis | + | * [http://cl-informatik.uibk.ac.at/users/swinkler/research/papers/SW13.pdf Termination tools in automated reasoning]. #Tesis #RA |
== Lecturas de febrero de 2013 == | == Lecturas de febrero de 2013 == | ||
| Línea 33: | Línea 32: | ||
* [http://blogs.elpais.com/turing/2013/02/algunos-vinculos-entre-los-teoremas-de-godel-y-turing.html Algunos vínculos entre los teoremas de Gödel y Turing] | * [http://blogs.elpais.com/turing/2013/02/algunos-vinculos-entre-los-teoremas-de-godel-y-turing.html Algunos vínculos entre los teoremas de Gödel y Turing] | ||
* [http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_%28v._1.02%29.pdf Formal computations and methods]. #Tesis #HOL_Light | * [http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_%28v._1.02%29.pdf Formal computations and methods]. #Tesis #HOL_Light | ||
| − | * [http://goo.gl/LXZra Complex concept lattices for simulating human prediction in sport]. | + | * [http://goo.gl/LXZra Complex concept lattices for simulating human prediction in sport]. #AFC |
* [http://www4.in.tum.de/~blanchet/mash.pdf MaSh: Machine learning for Sledgehammer]. #Isabelle #ITP2013 | * [http://www4.in.tum.de/~blanchet/mash.pdf MaSh: Machine learning for Sledgehammer]. #Isabelle #ITP2013 | ||
* [http://www.theses.fr/2012BOR14708 Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq]. #Tesis #Coq | * [http://www.theses.fr/2012BOR14708 Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq]. #Tesis #Coq | ||
* [http://www.cs.us.es/~jalonso/publicaciones/2013-Temas_de_PLIA.pdf Temas de programación lógica e inteligencia artificial]. #Prolog | * [http://www.cs.us.es/~jalonso/publicaciones/2013-Temas_de_PLIA.pdf Temas de programación lógica e inteligencia artificial]. #Prolog | ||
| − | * [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell]. | + | * [http://www.glc.us.es/~jalonso/vestigium/una-curiosa-propiedad-del-123-en-haskell Una curiosa propiedad del 123 en Haskell]. #Haskell |
* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2 | * [http://wiki.portal.chalmers.se/cse/uploads/ForMath/isabelle_acl2_report A report on an experiment in porting formal theories from Isabelle/HOL to Ecore and OCL2]. #Isabelle #ACL2 | ||
| − | * [http://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell]. | + | * [http://goo.gl/4Nm5N Otra curiosa propiedad del 123 en Haskell]. #Haskell |
* [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS | * [http://wimhesselink.nl/mechver/mx4bits/whh442b.pdf Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos]. #PVS | ||
* [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle | * [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing machines and computability theory in Isabelle/HOL]. #Isabelle | ||
| Línea 70: | Línea 69: | ||
* [http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf Formalization of real analysis: A survey of proof assistants and libraries]. #ITP | * [http://hal.inria.fr/docs/00/80/69/20/PDF/article.pdf Formalization of real analysis: A survey of proof assistants and libraries]. #ITP | ||
* [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_21.pdf AI over large formal knowledge bases: The first decade]. #Mizar | * [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_21.pdf AI over large formal knowledge bases: The first decade]. #Mizar | ||
| − | * [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_20.pdf ForMaRE-formal mathematical reasoning in economics]. | + | * [http://www.computing.dundee.ac.uk/staff/katya/arw13/papers/paper_20.pdf ForMaRE-formal mathematical reasoning in economics]. #RA |
* [http://www4.in.tum.de/~nipkow/pubs/cav13.pdf A fully verified executable LTL model checker]. #Isabelle | * [http://www4.in.tum.de/~nipkow/pubs/cav13.pdf A fully verified executable LTL model checker]. #Isabelle | ||
* [http://www.cse.chalmers.se/~nicsma/hipspec-cade.pdf Automating inductive proofs using theory exploration]. #Haskell #HipSpec | * [http://www.cse.chalmers.se/~nicsma/hipspec-cade.pdf Automating inductive proofs using theory exploration]. #Haskell #HipSpec | ||
Revisión del 07:36 28 abr 2013
Sumario
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
