Diferencia entre revisiones de «Lecturas del año 2012»

De WikiGLC
Saltar a: navegación, buscar
 
Línea 1: Línea 1:
 
== Lecturas de Enero de 2012 ==
 
== Lecturas de Enero de 2012 ==
* [http://interstices.info/jcms/int_63549/l-ordinateur-au-coeur-de-la-decouverte-mathematique L'ordinateur au cœur de la découverte mathématique].
+
* [http://interstices.info/jcms/int_63549/l-ordinateur-au-coeur-de-la-decouverte-mathematique L'ordinateur au cœur de la découverte mathématique]. #Matematica_experimental
* [http://bit.ly/uulX9N Últimos dos dígitos de (1+5^(2==n+1))/6]. #Haskell ==
+
* [http://bit.ly/uulX9N Últimos dos dígitos de (1+5^(2*n+1))/6]. #Haskell  
* [http://bit.ly/uwVb4B Disparad contra la Ilustración].
 
* [http://bit.ly/wdaCvM On the aesthetics of computer science].
 
 
* [http://arxiv.org/abs/1112.3782 Computing with hereditarily finite sequences]. #Prolog #MKM
 
* [http://arxiv.org/abs/1112.3782 Computing with hereditarily finite sequences]. #Prolog #MKM
* [http://conservancy.umn.edu/bitstream/107226/1/oh350sc.pdf An interview with Stephen A. Cook]
 
* [http://bit.ly/wGBM93 Lecturas del Grupo de Lógica Computacional (Enero de 2012)].
 
 
* [http://afp.sourceforge.net/entries/Markov_Models.shtml Markov models]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Markov_Models.shtml Markov models]. #Isabelle
 
* [http://bit.ly/xQa7rZ Turing machines] #Clásico #Divulgación
 
* [http://bit.ly/xQa7rZ Turing machines] #Clásico #Divulgación
* [http://cacm.acm.org/blogs/blog-cacm/145237-the-way-forward-for-computer-science-in-the-uk/fulltext The way forward for Computer Science in the U.K.] #Enseñanza
 
 
* [http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf Teaching semantics with a proof assistant: No more LSD trip proofs]. #Isabelle #Enseñanza
 
* [http://www4.in.tum.de/~nipkow/pubs/vmcai12.pdf Teaching semantics with a proof assistant: No more LSD trip proofs]. #Isabelle #Enseñanza
 
* [http://www.fing.edu.uy/~sierra/pres/2011/ciesc2008.pdf Enseñando deducción natural con Coq]. #Enseñanza #Lógica #Coq
 
* [http://www.fing.edu.uy/~sierra/pres/2011/ciesc2008.pdf Enseñando deducción natural con Coq]. #Enseñanza #Lógica #Coq
Línea 20: Línea 15:
  
 
== Lecturas de Febrero de 2012 ==
 
== Lecturas de Febrero de 2012 ==
* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-enero-de-2012-2/ Lecturas del Grupo de Lógica Computacional (Enero de 2012)].
 
 
* [https://iist.unu.edu/sites/iist.unu.edu/files/biblio/report429.pdf Emergence and refinement]. #Sistemas_complejos
 
* [https://iist.unu.edu/sites/iist.unu.edu/files/biblio/report429.pdf Emergence and refinement]. #Sistemas_complejos
 
* [http://www.springerlink.com/content/y222346j35g72064/fulltext.pdf Formalizing a hierarchical file system]. #PVS
 
* [http://www.springerlink.com/content/y222346j35g72064/fulltext.pdf Formalizing a hierarchical file system]. #PVS
Línea 27: Línea 21:
 
* [http://www.nicta.com.au/pub?doc=5614 Formal system verification for trustworthy embedded systems]. #Isabelle
 
* [http://www.nicta.com.au/pub?doc=5614 Formal system verification for trustworthy embedded systems]. #Isabelle
 
* [http://www.sciencedirect.com/science/article/pii/S1571066111000594 The mechanical verification of a DPLL-based satisfiability solver]. #PVS
 
* [http://www.sciencedirect.com/science/article/pii/S1571066111000594 The mechanical verification of a DPLL-based satisfiability solver]. #PVS
* [http://slidesha.re/x6Usor Innovación en el tratamiento de la información desde la Ingeniería del Conocimiento (1/2)]
 
* [http://slidesha.re/A9F7kl Innovación en el tratamiento de la información desde la Ingeniería del Conocimiento (2/2)]
 
* [http://gallium.inria.fr/~fpottier/publis/pouillard-pottier-unified.pdf A unified treatment of syntax with binders].
 
* [http://nyti.ms/xbs3Mq The age of Big Data]. #IA
 
* [http://bitnavegante.blogspot.com/2012/02/crear-moleculas-desde-cero-sin-la.html Crear moléculas desde cero sin la endiablada ecuación de Schrödinger]. #IA
 
 
* [http://afp.sourceforge.net/entries/Refine_Monadic.shtml Refinement for monadic programs]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Refine_Monadic.shtml Refinement for monadic programs]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml Dijkstra's shortest path algorithm]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml Dijkstra's shortest path algorithm]. #Isabelle
* [http://bit.ly/wV38h6 Computational topology].
+
* [http://bit.ly/wV38h6 Computational topology]. #MC
 
* [http://www.cs.st-andrews.ac.uk/~mik/categories.pdf Category theory and functional programming]. #Haskell
 
* [http://www.cs.st-andrews.ac.uk/~mik/categories.pdf Category theory and functional programming]. #Haskell
* [http://dl.acm.org/citation.cfm?id=2089134 The artist in the computer scientist: more humanity to our research].
 
* [https://www.cs.indiana.edu/~lepike/pubs/fm-ethics.pdf When formal systems kill: computer ethics and formal methods].
 
 
* [http://www.math.pitt.edu/~thales/papers/turing.pdf Mathematics in the age of the Turing machine]. #Panorama #DAO  
 
* [http://www.math.pitt.edu/~thales/papers/turing.pdf Mathematics in the age of the Turing machine]. #Panorama #DAO  
 
* [http://www.cl.cam.ac.uk/~mom22/itp12.pdf The reflective Milawa theorem prover is sound]. #ACL2 #HOL4
 
* [http://www.cl.cam.ac.uk/~mom22/itp12.pdf The reflective Milawa theorem prover is sound]. #ACL2 #HOL4
Línea 57: Línea 44:
 
* [http://www.lri.fr/~paulin/LASER/course-notes.pdf Introduction to the Coq proof-assistant for practical software verification]. #Tutorial #Coq
 
* [http://www.lri.fr/~paulin/LASER/course-notes.pdf Introduction to the Coq proof-assistant for practical software verification]. #Tutorial #Coq
 
* [http://www.lmcs-online.org/ojs/viewarticle.php?id=926&layout=abstract&iid=35 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #Coq
 
* [http://www.lmcs-online.org/ojs/viewarticle.php?id=926&layout=abstract&iid=35 Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #Coq
* [http://courses.csail.mit.edu/6.042/spring12/mcsfull.pdf Mathematics for Computer Science]. #Libro
+
* [http://courses.csail.mit.edu/6.042/spring12/mcsfull.pdf Mathematics for computer science]. #Libro
 
* [http://www21.in.tum.de/~popescua/pos.pdf Proving possibilistic, probabilistic noninterference]. #Isabelle
 
* [http://www21.in.tum.de/~popescua/pos.pdf Proving possibilistic, probabilistic noninterference]. #Isabelle
* [http://bit.ly/xH1KJy Decision procedures in Algebra and Logic (Reading material)]. #Libro #Lógica
+
* [http://bit.ly/xH1KJy Decision procedures in algebra and logic (Reading material)]. #Libro #Lógica
 
* [http://cgi.cse.unsw.edu.au/~rvg/eptcs/Published/LSFA2011/Papers/7/paper/AvelarAyalaRincon-1.pdf A formalization of the theorem of existence of first-order most general unifiers]. #PVS
 
* [http://cgi.cse.unsw.edu.au/~rvg/eptcs/Published/LSFA2011/Papers/7/paper/AvelarAyalaRincon-1.pdf A formalization of the theorem of existence of first-order most general unifiers]. #PVS
  
Línea 68: Línea 55:
 
* [http://www.springerlink.com/content/4t355540232364p2/ PVS linear algebra libraries for verification of control software algorithms in C/ACSL]. #PVS
 
* [http://www.springerlink.com/content/4t355540232364p2/ PVS linear algebra libraries for verification of control software algorithms in C/ACSL]. #PVS
 
* [http://www.springerlink.com/content/g520875717744612/ Generating verifiable Java code from verified PVS specifications]. #PVS
 
* [http://www.springerlink.com/content/g520875717744612/ Generating verifiable Java code from verified PVS specifications]. #PVS
* [http://www.cs.nott.ac.uk/~bmv/Papers/tfp2012_abstract.pdf Haskell gets argumentative]. #Haskell #Lógica @IA  
+
* [http://www.cs.nott.ac.uk/~bmv/Papers/tfp2012_abstract.pdf Haskell gets argumentative]. #Haskell #Lógica #IA  
* [http://education.lms.ac.uk/wp-content/uploads/2012/02/David_Pierce.pdf Induction and recursion]. #Fundamentos
+
* [http://education.lms.ac.uk/wp-content/uploads/2012/02/David_Pierce.pdf Induction and recursion]. #Fundamentos #LI
 
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq
 
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq
 
* [http://r6.ca/Goedel/goedel1.html Essential incompleteness of arithmetic verified by Coq]. #Coq
 
* [http://r6.ca/Goedel/goedel1.html Essential incompleteness of arithmetic verified by Coq]. #Coq
 
* [http://r6.ca/Thesis/ Incompleteness & completeness: Formalizing logic and analysis in type theory]. #Tesis #Coq
 
* [http://r6.ca/Thesis/ Incompleteness & completeness: Formalizing logic and analysis in type theory]. #Tesis #Coq
 
* [http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml Well-quasi-orders]. #Isabelle
 
* [http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml Well-quasi-orders]. #Isabelle
* [http://www.irisa.fr/celtique/genet/ACF/ Analyse et Conception Formelles (Software formal analysis and design)]. #Curso #Isabelle
+
* [http://www.irisa.fr/celtique/genet/ACF/ Analyse et conception formelles (Software formal analysis and design)]. #Curso #Isabelle
  
 
== Lecturas de Mayo de 2012 ==
 
== Lecturas de Mayo de 2012 ==
Línea 84: Línea 71:
 
* [http://kuscholarworks.ku.edu/dspace/handle/1808/8037 HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving]. #Tesis #Haskell
 
* [http://kuscholarworks.ku.edu/dspace/handle/1808/8037 HaskHOL: A Haskell hosted domain specific language for Higher-Order Logic theorem proving]. #Tesis #Haskell
 
* [http://cdn.bitbucket.org/jhlchan/hol/downloads/fermatProof.pdf A string of pearls: proofs of Fermat's little theorem]. #HOL4
 
* [http://cdn.bitbucket.org/jhlchan/hol/downloads/fermatProof.pdf A string of pearls: proofs of Fermat's little theorem]. #HOL4
* [http://www.cs.cmu.edu/~jcr/seplogic.pdf Separation logic: A logic for shared mutable data structures].
 
* [http://www.doc.ic.ac.uk/~ccris/ftp/asl-short.pdf Local action and abstract separation logic].
 
 
* [http://afp.sourceforge.net/entries/Separation_Algebra.shtml Separation algebra]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Separation_Algebra.shtml Separation algebra]. #Isabelle
 
* [http://www.eecs.qmul.ac.uk/~masci/works/preprints/preprint-ISSE-modelling_DC_in_PVS-embedded_refs-V1.pdf Using PVS to support the analysis of distributed cognition systems]. #PVS
 
* [http://www.eecs.qmul.ac.uk/~masci/works/preprints/preprint-ISSE-modelling_DC_in_PVS-embedded_refs-V1.pdf Using PVS to support the analysis of distributed cognition systems]. #PVS
Línea 91: Línea 76:
 
* [http://www.ece.concordia.ca/~o_hasan/thesis_hasan.pdf Formal probabilistic analysis using theorem proving]. #Tesis #HOL
 
* [http://www.ece.concordia.ca/~o_hasan/thesis_hasan.pdf Formal probabilistic analysis using theorem proving]. #Tesis #HOL
 
* [http://web.student.chalmers.se/~danr/master-thesis-draft.pdf Proving equational Haskell properties using automated theorem provers]. #Haskell #Thesis
 
* [http://web.student.chalmers.se/~danr/master-thesis-draft.pdf Proving equational Haskell properties using automated theorem provers]. #Haskell #Thesis
* [http://cps-vo.org/node/3338 Accessible integrated formal reasoning environments in classroom instruction of mathematics].
+
* [http://cps-vo.org/node/3338 Accessible integrated formal reasoning environments in classroom instruction of mathematics]. #Enseñanza
* [http://cs-people.bu.edu/lapets/resource/dalfvs.pdf Designing accessible lightweight formal verification systems].
+
* [http://cs-people.bu.edu/lapets/resource/dalfvs.pdf Designing accessible lightweight formal verification systems]. #AR
* [http://www.scienceomega.com/article/359/artificial-intelligence-from-fantasy-to-reality Artificial intelligence: from fantasy to reality]. #IA
 
 
* [http://web.student.chalmers.se/~danr/hipspec-atx.pdf HipSpec: Automating inductive proofs of program properties]. #Haskell
 
* [http://web.student.chalmers.se/~danr/hipspec-atx.pdf HipSpec: Automating inductive proofs of program properties]. #Haskell
 
* [http://www.cs.toronto.edu/~hector/tc-instructor.html Supplementary material for "Thinking as computation"]. #IA #Prolog
 
* [http://www.cs.toronto.edu/~hector/tc-instructor.html Supplementary material for "Thinking as computation"]. #IA #Prolog
Línea 99: Línea 83:
 
* [http://www.ssrg.nicta.com.au/publications/papers/Greenaway_AK_12.pdf Bridging the gap: Automatic verified abstraction of C]
 
* [http://www.ssrg.nicta.com.au/publications/papers/Greenaway_AK_12.pdf Bridging the gap: Automatic verified abstraction of C]
 
* [http://faculty.cs.byu.edu/~jay/static/toronto-2012flops.pdf Computing in Cantor’s paradise with λZFC].  
 
* [http://faculty.cs.byu.edu/~jay/static/toronto-2012flops.pdf Computing in Cantor’s paradise with λZFC].  
* [http://blog.ezyang.com/2012/05/thoughts-on-gamifying-textbooks/ Thoughts on gamifying textbooks].
 
 
* [http://www.lri.fr/~mcg/PDF/VSSTE2012.pdf Isabelle/Circus: A process specification and verification environment]. #Isabelle
 
* [http://www.lri.fr/~mcg/PDF/VSSTE2012.pdf Isabelle/Circus: A process specification and verification environment]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Circus.shtml Isabelle/Circus]. #Isabelle
 
* [http://afp.sourceforge.net/entries/Circus.shtml Isabelle/Circus]. #Isabelle
Línea 148: Línea 131:
 
* [http://www.cs.princeton.edu/~rdockins/dissertation/thesis-online.pdf Operational refinement for compiler correctness]. #Tesis #Coq
 
* [http://www.cs.princeton.edu/~rdockins/dissertation/thesis-online.pdf Operational refinement for compiler correctness]. #Tesis #Coq
 
* [http://www.irit.fr/~Martin.Strecker/Publications/proofs_graph_transformations.html Interactive and automated proofs for graph transformations]. #Isabelle
 
* [http://www.irit.fr/~Martin.Strecker/Publications/proofs_graph_transformations.html Interactive and automated proofs for graph transformations]. #Isabelle
* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-marzo-agosto-de-2012/ Lecturas del Grupo de Lógica Computacional (Marzo-Agosto de 2012)]
 
 
* [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. #Haskell
 
* [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. #Haskell
 
* [http://blogs.elpais.com/turing/2012/09/computadores-von-neumann-o-computadores-turing.html ¿Computadores von Neumann, o computadores Turing?] #Historia
 
* [http://blogs.elpais.com/turing/2012/09/computadores-von-neumann-o-computadores-turing.html ¿Computadores von Neumann, o computadores Turing?] #Historia
Línea 157: Línea 139:
 
* [http://hal.inria.fr/hal-00712938/PDF/article.pdf Improving real analysis in Coq: a user-friendly approach to integrals and derivatives]. #Coq ([http://cpp12.kuis.kyoto-u.ac.jp/accepted.html CPP2012])
 
* [http://hal.inria.fr/hal-00712938/PDF/article.pdf Improving real analysis in Coq: a user-friendly approach to integrals and derivatives]. #Coq ([http://cpp12.kuis.kyoto-u.ac.jp/accepted.html CPP2012])
 
* [http://www.cse.chalmers.se/~mortberg/papers/cphwcs.pdf Computing persistent homology within Coq/SSReflect]. #Coq
 
* [http://www.cse.chalmers.se/~mortberg/papers/cphwcs.pdf Computing persistent homology within Coq/SSReflect]. #Coq
* [http://www.traficantes.net/index.php/editorial/catalogo/coleccion_mapas/Software-libre-para-una-sociedad-libre Software libre para una sociedad libre]. #Libro #Pensamiento
 
 
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq ([http://www.map2012.uni-konstanz.de/ MAP2012], [http://www.cse.chalmers.se/~siles/coq/formalisation.html code], [http://www.cse.chalmers.se/~mortberg/talks/anders-map2012.pdf Presentación]).
 
* [http://www.cse.chalmers.se/~siles/papers/sasaki-murao.pdf A formal proof of Sasaki-Murao algorithm]. #Coq ([http://www.map2012.uni-konstanz.de/ MAP2012], [http://www.cse.chalmers.se/~siles/coq/formalisation.html code], [http://www.cse.chalmers.se/~mortberg/talks/anders-map2012.pdf Presentación]).
  
Línea 169: Línea 150:
 
* [http://hal.inria.fr/docs/00/74/30/90/PDF/article.pdf A formally-verified C compiler supporting floating-point arithmetic]. #Coq
 
* [http://hal.inria.fr/docs/00/74/30/90/PDF/article.pdf A formally-verified C compiler supporting floating-point arithmetic]. #Coq
 
* [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/BoyerMoore.pdf The Boyer-Moore waterfall model revisited]. #HOL_Light
 
* [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/BoyerMoore.pdf The Boyer-Moore waterfall model revisited]. #HOL_Light
* [http://proc.isecon.org/2012/cases/2136.pdf A Python pattern matcher project for an introduction to Artificial Intelligence course]. #IA
 
  
 
== Lecturas de Noviembre de 2012 ==
 
== Lecturas de Noviembre de 2012 ==
Línea 197: Línea 177:
  
 
== Lecturas de Diciembre de 2012 ==
 
== Lecturas de Diciembre de 2012 ==
* [http://www.glc.us.es/~jalonso/vestigium/lecturas-del-grupo-de-logica-computacional-septiembre-noviembre-de-2012/ Lecturas del Grupo de Lógica Computacional (Septiembre-Noviembre de 2012)].
 
 
* [http://arxiv.org/pdf/1211.6197 Verifying probabilistic correctness in Isabelle with pGCL]. #Isabelle
 
* [http://arxiv.org/pdf/1211.6197 Verifying probabilistic correctness in Isabelle with pGCL]. #Isabelle
 
* [http://www.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf Formalization of a strategy for the KRK chess endgame]. #Coq
 
* [http://www.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf Formalization of a strategy for the KRK chess endgame]. #Coq
Línea 206: Línea 185:
 
* [http://www.irit.fr/~Ralph.Matthes/papers/MatthesPicardTYPES11PostProc.pdf Verification of redecoration for infinite triangular matrices using coinduction]. #Coq
 
* [http://www.irit.fr/~Ralph.Matthes/papers/MatthesPicardTYPES11PostProc.pdf Verification of redecoration for infinite triangular matrices using coinduction]. #Coq
 
* [http://www.irit.fr/~Celia.Picard/These/ Représentation coinductive des graphes]. #Tesis #Coq
 
* [http://www.irit.fr/~Celia.Picard/These/ Représentation coinductive des graphes]. #Tesis #Coq
* [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9268-z Formal mathematics for mathematicians].
+
* [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9268-z Formal mathematics for mathematicians]. #RA
 
* [http://link.springer.com/article/10.1007/s10817-012-9250-9 The HOL Light theory of euclidean space]. #HOL_Light
 
* [http://link.springer.com/article/10.1007/s10817-012-9250-9 The HOL Light theory of euclidean space]. #HOL_Light
 
* [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9265-2 Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar]. #Mizar
 
* [http://link.springer.com/content/pdf/10.1007%2Fs10817-012-9265-2 Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar]. #Mizar
Línea 213: Línea 192:
 
* [http://arxiv.org/pdf/1212.3870v1 Interactive verification of Markov chains: Two distributed protocol case studies]. #Isabelle
 
* [http://arxiv.org/pdf/1212.3870v1 Interactive verification of Markov chains: Two distributed protocol case studies]. #Isabelle
 
* [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. (Interstices, 2012) #Divulgación #DAO
 
* [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. (Interstices, 2012) #Divulgación #DAO
* [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]
+
* [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation] #RA

Revisión actual del 06:32 28 abr 2013

Lecturas de Enero de 2012

Lecturas de Febrero de 2012

Lecturas de Marzo de 2012

Lecturas de Abril de 2012

Lecturas de Mayo de 2012

Lecturas de Junio de 2012

Lecturas de Julio de 2012

Lecturas de Agosto de 2012

Lecturas de Septiembre de 2012

Lecturas de Octubre de 2012

Lecturas de Noviembre de 2012

Lecturas de Diciembre de 2012