Jalonso en 17:42 27 abr 2013

2013-04-27T17:42:40Z

Jalonso: New page: == 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]. * [htt...

2013-04-27T17:39:59Z

New page: == 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]. * [htt...

Página nueva

== 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://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://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://bit.ly/xQa7rZ Turing machines] por J. Hopcroft #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://www.fing.edu.uy/~sierra/pres/2011/ciesc2008.pdf Enseñando deducción natural con Coq]. #Enseñanza #Lógica #Coq
* [http://hal.archives-ouvertes.fr/docs/00/65/65/26/PDF/rfia2012_submission_117.pdf Formalisation en OWL pour vérifier les spécifications d’un environnement intelligent]. #OWL
* [http://greenteapress.com/complexity/thinkcomplexity.pdf Think complexity]. #Sistemas_complejos #Python
* [http://code.google.com/p/graphbook/ Algorithmic graph theory]. #Libro #Sage
* [http://www.mat.uniroma1.it/~caminati/CaminatiTesi20111130_09.16.44.pdf A simplified framework for first-order languages and its formalization in Mizar]. #Tesis #Metalógica #Mizar
* [http://arxiv.org/abs/1201.0540 ProofPeer - A cloud-based interactive theorem proving system]. #ProofPeer
* [http://ssr.msr-inria.inria.fr/proofreading/current.pdf Generic proof tools and finite group theory]. #Tesis #Coq

== 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
* [http://www.springerlink.com/content/y222346j35g72064/fulltext.pdf Formalizing a hierarchical file system]. #PVS
* [https://master-informatique.unistra.fr/intranet/uploads/M2ISI/Stages/Rapports_2011/JD_Genevaux_Memoire_M2.pdf Etude et formalisation de la méthode de Wu dans Coq]. #Tesis #Coq
* [http://www.eecs.qmul.ac.uk/~masci/works/masci-nasafm2012.pdf Using PVS to investigate incidents through the lens of distributed cognition]. #PVS
* [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://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/Dijkstra_Shortest_Path.shtml Dijkstra's shortest path algorithm]. #Isabelle
* [http://bit.ly/wV38h6 Computational topology].
* [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.cl.cam.ac.uk/~mom22/itp12.pdf The reflective Milawa theorem prover is sound]. #ACL2 #HOL4
* [http://bit.ly/zQWLJr Ejercicios de "Informática de 1º de Matemáticas" (2011-12)]. #Haskell
* [http://bit.ly/yXCSE1 Temas de programación funcional con Haskell (curso 2011-12)]. #Haskell
* [Http://afp.sourceforge.net/entries/Transitive-Closure-II.shtml Executable transitive closures]. #Isabelle

== Lecturas de Marzo de 2012 ==
* [http://www21.in.tum.de/~blanchet/phdthesis-draft.pdf Automatic proofs and refutations for higher-order logic]. #Tesis #Isabelle
* [http://www.brucker.ch/bibliography/download/2012/brucker.ea-theorem-prover-2012.pdf On theorem prover-based testing]. #Isabelle
* [http://arxiv.org/abs/1202.6473 CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates]. #Coq
* [http://bit.ly/wmPn13 Tips on Haskell]. #Tutorial #Haskell
* [http://www.sfu.ca/~xwa33/pubs/LPAR18-System.pdf Enfragmo: A system for modelling and solving search problems with logic]. #SAT
* [http://bit.ly/xPObnN Logic & reasoning: from Aristotle to Intel]. #Panorama #Lógica
* [http://www.lmcs-online.org/ojs/viewarticle.php?id=934&layout=abstract&iid=35 Deciding Kleene Algebras in Coq]. #Coq
* [http://www-sop.inria.fr/members/Sylvain.Heraud/paper/these_heraud.pdf Vérification semi-automatique de primitives cryptographiques]. #Tesis #Coq
* [http://www.mat.unb.br/~ayala/DY_Full_formalization.pdf Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. #PVS
* [http://hvg.ece.concordia.ca/Publications/TECH_REP/FDE_TR12/FDE_TR12.pdf Formal error analysis and verification of the frequency domain equalizer]. #HOL
* [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://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://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

== Lecturas de Abril de 2012 ==
* [http://www.sciencedirect.com/science/article/pii/S0890540112000727 The worldʼs shortest correct exact real arithmetic program?]. #PVS #Haskell
* [http://tel.archives-ouvertes.fr/docs/00/68/36/61/PDF/these-braibant_archivage_2012.pdf Kleene algebra, rewriting modulo AC and circuits in Coq]. #Tesis #Coq
* [http://logic.csci.unt.edu/tarau/teaching/SoftEng/pcantor.pdf Deriving a fast inverse of the generalized Cantor n-tupling bijection]. #Prolog
* [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.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://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/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://www.irisa.fr/celtique/genet/ACF/ Analyse et Conception Formelles (Software formal analysis and design)]. #Curso #Isabelle

== Lecturas de Mayo de 2012 ==
* [http://www4.in.tum.de/~wenzelm/test/website_18-Apr-2012/dist/Isabelle_18-Apr-2012/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. #Isabelle
* [http://home.in.tum.de/~immler/itp2012_draft.pdf Numerical analysis of ordinary differential equations]. #Isabelle
* [http://afp.sourceforge.net/entries/Inductive_Confidentiality.shtml Inductive study of confidentiality]. #AFP #Isabelle
* [http://books.google.es/books?id=RBwEoSASE5sC&pg=PA136&dq=2Formal+Correctness+of+Security+Protocols%22&hl=es&sa=X&ei=rVehT6KzEMey0QWN5YH-Bw&redir_esc=y#v=onepage&q&f=false Formal correctness of security protocols]. #Libro #Isabelle
* [http://afp.sourceforge.net/entries/Stuttering_Equivalence.shtml Stuttering equivalence]. #AFP
* [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://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://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://hvg.ece.concordia.ca/Publications/Conferences/CCECE12.pdf Formal verification of the heavy hitter problem]. #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://cps-vo.org/node/3338 Accessible integrated formal reasoning environments in classroom instruction of mathematics].
* [http://cs-people.bu.edu/lapets/resource/dalfvs.pdf Designing accessible lightweight formal verification systems].
* [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://www.cs.toronto.edu/~hector/tc-instructor.html Supplementary material for "Thinking as computation"]. #IA #Prolog
* [https://esus.unirioja.es/psycotrip/archivos_publicaciones/73620215.pdf Verifying an algorithm computing discrete vector fields for digital imaging]. #Coq
* [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://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://afp.sourceforge.net/entries/Circus.shtml Isabelle/Circus]. #Isabelle
* [http://www-lipn.univ-paris13.fr/~mayero/publis/JARFOST2012.pdf Wave equation numerical resolution: a comprehensive mechanized proof of a C program] #Coq

== Lecturas de Junio de 2012 ==
* [http://nicta.com.au/research/research_publications/show%3Fid%3D5396 Large-scale formal verification in practice: A process perspective]. #Isabelle
* [http://www.cs.ucla.edu/~lesani/downloads/Papers/CONCUR12.pdf A framework for formally verifying software transactional memory algorithms]. #PVS
* [http://www-lipn.univ-paris13.fr/~mayero/publis/RPA-NFM.pdf Rigorous polynomial approximation using Taylor models in Coq]. #Coq
* [http://perso.ens-lyon.fr/mioara.joldes/these/theseJoldes.pdf Rigorous polynomial approximations and applications]. #Tesis #Coq

== Lecturas de Julio de 2012 ==
* [http://homepages.inf.ed.ac.uk/apease/papers/seventy-four.pdf Seventy four minutes of mathematics: An analysis of the third Mini-Polymath project]. #MKM
* [http://www.jaist.ac.jp/~hirokawa/aj12/sternagel.pdf Formalizing Kruskal’s tree theorem in Isabelle/HOL]. #Isabelle
* [http://arxiv.org/abs/1207.3315 Verifying an algorithm computing discrete vector fields for digital imaging]. #Coq
* [http://arxiv.org/abs/1207.3208 Formal verification of monad transformers]. #Isabelle
* [http://research.microsoft.com/en-us/um/people/simonpj/papers/verify/hcc-popl.pdf HALO: Haskell to logic through denotational semantics]. #Haskell
* [http://www21.in.tum.de/~nipkow/MOD2011/isabelle-notes.pdf Interactive proof: Introduction to Isabelle/HOL]. #Tutorial #Isabelle
* [http://shemesh.larc.nasa.gov/people/cam/Bernstein/bernstein.pdf Formalization of an efficient representation of Bernstein polynomials and applications to global optimization] #PVS
* [http://www21.in.tum.de/~nipkow/Isabelle2012/p5.pdf Lifting and transfer: A modular design for quotients in Isabelle/HOL]. #Isabelle
* [http://www.cs.utexas.edu/users/bendy/papers/MTC.pdf Meta-theory à la carte]. #Coq
* [http://www.dcc.fc.up.pt/dcc/Pubs/TReports/TR12/dcc-2012-04.pdf Mechanization of an algorithm for deciding KAT terms equivalence]. #Coq
* [http://blogs.elpais.com/turing/2012/07/es-posible-construir-software-que-no-falle.html ¿Es posible construir software que no falle?]. #Verificación

== Lecturas de Agosto de 2012 ==
* [http://afp.sourceforge.net/entries/Impossible_Geometry.shtml Proving the impossibility of trisecting an angle and doubling the cube]. #Isabelle
* [http://www.dsc.ufcg.edu.br/~spg/uploads/lawasp2012.pdf Formal specification and verification of well-formedness in business process product lines]. #PVS
* [http://www.cs.nott.ac.uk/~gmh/hu-thesis.pdf} Compiling concurrency correctly (Verifying software transactional memory)]. #Tesis #Agda #Haskell
* [http://www.irit.fr/~Celia.Picard/These/TheseCeliaPicard.pdf Représentation coinductive des graphes]. #Tesis #Coq
* [http://nicta.com.au/research/research_publications/show%3Fid%3D4836 Formalizing adequacy: A case study for higher-order abstract syntax]. #Isabelle
* [http://www.in.tum.de/~nipkow/Isabelle2012/p4.pdf Algorithms in games evolving in time: Winning strategies based on testing]. #Isabelle
* [http://perso.ens-lyon.fr/martin.bodin/M2/stage/rapport.pdf A certified JavaScript interpreter]. #Coq
* [http://staff.aist.go.jp/reynald.affeldt/documents/affeldt-itp2012-preprint.pdf Formalization of Shannon’s theorems in SSReflect-Coq]. #Coq
* [http://www21.in.tum.de/~nipkow/pubs/itp12.pdf Abstract interpretation of annotated commands]. #Isabelle
* [http://hal.inria.fr/hal-00671809 Construction of real algebraic numbers in Coq]. #Coq
* [http://www.irit.fr/~Mathieu.Giorgino/Publications/GiSt2012BDD.html Correctness of pointer manipulating algorithms illustrated by a verified BDD construction]. #Isabelle
* [http://hal.inria.fr/hal-00682398 Towards provably robust watermarking]. #Coq
* [http://www.unirioja.es/cu/jodivaso/degree_thesis/Memoria.pdf Proofs of properties of finite-dimensional vector spaces using Isabelle/HOL]. #Isabelle
* [http://wiki.portal.chalmers.se/cse/uploads/ForMath/DivasonEACA2012 Formalizing an abstract algebra textbook in Isabelle/HOL]. #Isabelle
* [http://home.in.tum.de/~immler/itp2012_draft.pdf Numerical analysis of ordinary differential equations in Isabelle/HOL]. #Isabelle
* [http://www.cse.chalmers.se/~mortberg/papers/coqeal.pdf A refinement-based approach to computational algebra in Coq]. #Coq
* [http://www.cse.chalmers.se/~mortberg/papers/coherent.pdf Coherent and strongly discrete rings in type theory]. #Coq
* [http://www.ida.liu.se/~wlodr/drabent.2012vii28.pdf Logic * control: An example of program construction]. #Prolog
* [http://drops.dagstuhl.de/opus/volltexte/2012/3632/pdf/30.pdf Deriving a fast inverse of the generalized Cantor N-tupling bijection]. #Prolog
* [http://elrond.informatik.tu-freiberg.de/papers/WorldComp2012/FCS2680.pdf Formalization and verification of number theoretic algorithms using the Mizar proof checker]. #Mizar

== Lecturas de Septiembre de 2012 ==
* [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.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://blogs.elpais.com/turing/2012/09/computadores-von-neumann-o-computadores-turing.html ¿Computadores von Neumann, o computadores Turing?] #Historia
* [http://argo.matf.bg.ac.rs/publications/2012/frankl.pdf Formalizing Frankl's conjecture: FC-families]. #Isabelle
* [http://riazanov.webs.com/Riazanov_PhD_thesis.pdf Implementing an efficient theorem prover]. #Tesis #Vampire
* [http://dld.bz/bKwJY System of logic based on ordinals]. #Tesis #Historia
* [http://www21.in.tum.de/~nipkow/pubs/cpp12.html Proving concurrent noninterference] ([http://afp.sourceforge.net/entries/Possibilistic_Noninterference.shtml código]) #Isabelle
* [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.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]).

== Lecturas de Octubre de 2012 ==
* [http://arxiv.org/pdf/1210.1100 Confluence by decreasing diagrams formalized]. #Isabelle
* [http://cl-informatik.uibk.ac.at/users/griff/publications/S-JAR12.pdf Proof Pearl – A mechanized proof of GHC’s mergesort]. #Isabelle #Haskell
* [http://www.springerlink.com/content/w1083121v2mm3488/ A logic-algebraic approach to decision taking in a railway interlocking system]. #BG
* [http://ozk.unizd.hr/proceedings/index.php/els/article/viewFile/105/99&sa Scheme in industrial automation]. #Scheme
* [https://www.cs.utexas.edu/~ragerdl/papers/dissertation/dissertation.pdf Parallelizing an interactive theorem prover: Functional programming and proofs with ACL2]. #ACL2 #Tesis
* [http://nicta.com.au/research/research_publications/show?id=6061 A string of pearls: Proofs of Fermat’s little theorem]. #HOL4
* [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://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 ==
* [http://wwwnipkow.in.tum.de/teaching/info2/WS1213/slides.pdf Informatik 2: Functional programming]. #Haskell
* [http://tel.archives-ouvertes.fr/docs/00/74/55/53/PDF/MARTIN_DOREL_Erik_2012_these.pdf Contributions to the formal verification of arithmetic algorithms]. #Tesis #Coq
* [http://staff.science.uva.nl/~raquel/teaching/cosp/cosp2012/slides/WLH.pdf Why learn Haskell?]. #Tutorial #Haskell
* [http://researcharchive.vuw.ac.nz/handle/10063/2315 A mechanical verification of the independence of Tarski's euclidean axiom] y [http://afp.sourceforge.net/entries/Tarskis_Geometry.shtml código] #Tesina #Isabelle
* [http://fm.mizar.org/fm20-3/ltlaxio4.pdf Weak completeness theorem for propositional linear time temporal logic]. #Mizar
* [http://nlpwp.org/book Natural language processing for the working programmer]. #Haskell #IA
* [http://arxiv.org/abs/1211.3700 Nexus authorization logic (NAL): Logical results]. #Coq
* [http://www.icvl.eu/2012/disc/icvl/documente/pdf/soft/ICVL_SoftwareSolutions_paper07.pdf Reasons for studying Haskell in University]. #Haskell
* [http://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2012_ContructiveTC.pdf Constructive completeness for modal logic with transitive closure]. #Coq #Modal
* [http://jite.informingscience.org/documents/Vol11/JITEv11IIPp353-376Panovics1174.pdf A functional programming approach to AI search algorithms]. #IA #PF
* [http://sevein.matap.uma.es/~aciego/TR/ins-dual.pdf Dual multi-adjoint concept lattices]. #AFC
* [http://www.glc.us.es/~jalonso/DAO2012/index.php5/Temas Temas de "Demostración asistida por ordenador"]. #Isabelle #Tutorial
* [http://www.slideshare.net/jborregouses/tema-8-15269984 Verificación de programas: Introducción]. #Verificación
* [http://www.glc.us.es/~jalonso/vestigium/i1m2012-ultimo-digito-del-producto-de-numeros-de-fermat Último dígito del producto de números de Fermat]. #Haskell #IMO
* [http://www.lix.polytechnique.fr/~neron/Publi/Elimsqrt/Elimsqrtlong.pdf A formal proof of square root and division elimination in embedded programs]. #PVS
* [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères (Preuve formelle du théorème de Feit et Thompson)]. #Coq #Divulgación
* [http://perso.crans.org/cohen/papers/thesis-to-review.pdf Formalized algebraic numbers: construction and first order theory]. #Tesis #Coq
* [http://homepages.inf.ed.ac.uk/wadler/papers/how-and-why/how-and-why.pdf How enterprises use functional languages, and why they don't]. #PF
* [http://doras.dcu.ie/17459/1/thesis-denis-butin-oneside.pdf Inductive analysis of security protocols in Isabelle/HOL with applications to electronic voting]. #Tesis #Isabelle
* [http://www.ps.uni-saarland.de/~jokaiser/thesis.pdf Constructive formalization of regular languages]. #Tesina #Coq
* [http://www.cse.unt.edu/~tarau/teaching/CompMath/freealgH.pdf Computing with free algebras]. #Haskell
* [http://www.botkes.nl/wp-content/uploads/HaskellTutor.pdf Ask-Elle: a Haskell Tutor]. #Tesis #Haskell #TI
* [http://arxiv.org/pdf/1211.6468v1 Using Isabelle to verify special relativity, with application to hypercomputation theory]. #Isabelle

== 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://www.ceciis.foi.hr/app/public/conferences/1/papers2012/dkb3.pdf Formalization of a strategy for the KRK chess endgame]. #Coq
* [http://rvg.web.cse.unsw.edu.au/eptcs/paper.cgi?THedu11.4 Formalization and implementation of algebraic methods in Geometry]. #Isabelle
* [http://shemesh.larc.nasa.gov/people/cam/publications/rc2012-draft.pdf Formal verification of conflict detection algorithms for arbitrary trajectories]. #PVS
* [http://arxiv.org/abs/1211.7012 Learning-assisted automated reasoning with Flyspeck]. #Mizar
* [http://etd.lsu.edu/docs/available/etd-11102012-171915/unrestricted/Lu_Diss.pdf Deductive formal verification of embedded systems]. #Tesis #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://link.springer.com/content/pdf/10.1007%2Fs10817-012-9268-z Formal mathematics for mathematicians].
* [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://fm.mizar.org/fm20-3/goedcpuc.pdf The Gödel completeness theorem for uncountable languages]. #Mizar
* [http://arxiv.org/pdf/1212.3618v1 Machine learning in Proof General: Interfacing interfaces]. #Coq
* [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://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]

Lecturas del año 2012 - Historial de revisiones

Jalonso en 05:32 28 abr 2013

Jalonso en 17:42 27 abr 2013

Jalonso: New page: == 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]. * [htt...

@@ Línea 8: / Línea 8: @@
 * [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://bit.ly/xQa7rZ Turing machines] por J. Hopcroft #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
@@ Línea 42: / Línea 42: @@
 * [http://bit.ly/zQWLJr Ejercicios de "Informática de 1º de Matemáticas" (2011-12)]. #Haskell
 * [http://bit.ly/yXCSE1 Temas de programación funcional con Haskell (curso 2011-12)]. #Haskell
-* [Http://afp.sourceforge.net/entries/Transitive-Closure-II.shtml Executable transitive closures]. #Isabelle
+* [http://afp.sourceforge.net/entries/Transitive-Closure-II.shtml Executable transitive closures]. #Isabelle
 == Lecturas de Marzo de 2012 ==