{"id":1451,"date":"2011-07-21T18:01:21","date_gmt":"2011-07-21T18:01:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=1451"},"modified":"2011-08-02T09:00:25","modified_gmt":"2011-08-02T09:00:25","slug":"lecturas-de-razonamiento-formalizado-del-27-oct-2010-al-1-jul-2011","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lecturas-de-razonamiento-formalizado-del-27-oct-2010-al-1-jul-2011\/","title":{"rendered":"Lecturas de razonamiento formalizado (del 27-Oct-2010 al 1-Jul-2011)"},"content":{"rendered":"

Esta entrada es una recopilaci\u00f3n de lecturas sobre razonamiento formalizado que hemos compartido este curso en la lista de correo del grupo de l\u00f3gica computacional<\/a>.\n<\/p>\n

\nLa recopilaci\u00f3n de los est\u00e1 ordenada seg\u00fan el sistema de razonamiento utilizado (ACL2, Agda, Coq, HOL, Isabelle, Matita, Mizar, Otter\/Prover9, PVS \u00f3 Twelfe) y, dentro de cada uno, por la fecha de su publicaci\u00f3n.\n<\/p>\n

<\/p>\n

ACL2<\/h2>\n
    \n
  1. \nL\u00f3gica Computacional en Sevilla (30 a\u00f1os en una hora)<\/a>\n<\/li>\n
  2. \nA Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free<\/a>\n<\/li>\n
  3. \nGesti\u00f3n mecanizada del conocimiento matem\u00e1tico en Topolog\u00eda algebraica<\/a>\n<\/li>\n
  4. \nIntegrating Testing and Interactive Theorem Proving<\/a>\n<\/li>\n<\/ol>\n

    Agda<\/h2>\n
      \n
    1. \nVerified Stack-Based Genetic Programming via Dependent Types<\/a>\n<\/li>\n<\/ol>\n

      Coq<\/h2>\n
        \n
      1. \nCertifying compilers using higher-order theorem provers as certificate checkers<\/a>\n<\/li>\n
      2. \nThe Dialectica interpertation in Coq<\/a>\n<\/li>\n
      3. \nA Formalization of the C99 Standard in HOL, Isabelle and Coq<\/a>\n<\/li>\n
      4. \nA Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry<\/a>\n<\/li>\n
      5. \nConstructive Formalization of Classical Modal Logic<\/a>\n<\/li>\n
      6. \nProving Equality between Streams<\/a>\n<\/li>\n
      7. \nA formal proof that \u03c0\u2081(S\u00b9)=Z<\/a>\n<\/li>\n
      8. \nBalancing Weight-Balanced Trees<\/a>\n<\/li>\n
      9. \nA Formal Programming Model of Orl\u00e9ans Skeleton Library<\/a>\n<\/li>\n
      10. \nComputer certified efficient exact reals in Coq<\/a>\n<\/li>\n
      11. \nTRX: A Formally Verified Parser Interpreter<\/a>\n<\/li>\n
      12. \nRationality and Escalation in Infinite Extensive Games<\/a>\n<\/li>\n
      13. \nInitial Semantics for higher-order typed syntax in Coq<\/a>\n<\/li>\n
      14. \nFormal proofs in real algebraic geometry: from ordered fields to quantifier elimination<\/a>\n<\/li>\n
      15. \nSpecification of imperative languages using operational semantics in Coq<\/a>\n<\/li>\n
      16. \nOn the Generation of Positivstellensatz Witnesses in Degenerate Cases<\/a>\n<\/li>\n
      17. \nDeciding Kleene Algebras in Coq<\/a>\n<\/li>\n
      18. \nType classes for efficient exact real arithmetic in Coq<\/a>\n<\/li>\n
      19. \nIncidence simplicial matrices formalized in Coq\/SSReflect<\/a>\n<\/li>\n<\/ol>\n

        HOL<\/h2>\n
          \n
        1. \nFormal reliability analysis of combinational circuits using theorem proving<\/a>\n<\/li>\n
        2. \nSMT solvers: new oracles for the HOL theorem prover<\/a>\n<\/li>\n
        3. \nA Formalization of the C99 Standard in HOL, Isabelle and Coq<\/a>\n<\/li>\n
        4. \nFormal Verification of Chess Endgames Tables<\/a>\n<\/li>\n
        5. \nA verified runtime for a verified theorem prover<\/a>\n<\/li>\n<\/ol>\n

          Isabelle<\/h2>\n
            \n
          1. \nL\u00f3gica Computacional en Sevilla (30 a\u00f1os en una hora)<\/a>\n<\/li>\n
          2. \nCertifying compilers using higher-order theorem provers as certificate checkers<\/a>\n<\/li>\n
          3. \nDeducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/Isar<\/a>\n<\/li>\n
          4. \nDeducci\u00f3n natural en l\u00f3gica de primer orden con Isabelle\/Isar<\/a>\n<\/li>\n
          5. \nA novel formalization of symbolic trajectory evaluation semantics in Isabelle\/HOL<\/a>\n<\/li>\n
          6. \nFunctional Binomial Queues<\/a>\n<\/li>\n
          7. \nLower Semicontinuous Functions<\/a>\n<\/li>\n
          8. \nFormalising, improving, and reusing the Java Module System<\/a>\n<\/li>\n
          9. \nIsabelle como un lenguaje funcional<\/a>\n<\/li>\n
          10. \nExecutable Transitive Closures of Finite Relations<\/a>\n<\/li>\n
          11. \nA Formalization of the C99 Standard in HOL, Isabelle and Coq<\/a>\n<\/li>\n
          12. \nVerified Firewall Policy Transformations for Test Case Generation<\/a>\n<\/li>\n
          13. \nAn Approach to Modular and Testable Security Models of Real-world Health-care Applications<\/a>\n<\/li>\n
          14. \nPsi-calculi: a framework for mobile processes with nominal data and logic<\/a>\n<\/li>\n
          15. \nExtending Sledgehammer with SMT Solvers<\/a>\n<\/li>\n
          16. \nThe General Triangle Is Unique<\/a>\n<\/li>\n
          17. \nMechanical Support for Ef\ufb01cient Dissemination on the CAN Overlay Network<\/a>\n<\/li>\n
          18. \nFormal Verification of a small real-time operating system<\/a>\n<\/li>\n
          19. \nKnowledge-Based Programs<\/a>\n<\/li>\n
          20. \nTermination of Isabelle Functions via Termination of Rewriting<\/a>\n<\/li>\n
          21. \nEfficient Interactive Construction of Machine-Checked Protocol Security Proofs in the Context of Dynamically Compromising Adversaries<\/a>\n<\/li>\n
          22. \nThree Chapters of Measure Theory in Isabelle\/HOL<\/a>\n<\/li>\n
          23. \nseL4 Enforces Integrity<\/a>\n<\/li>\n
          24. \nAutomated Engineering of Relational and Algebraic Methods in Isabelle\/HOL<\/a>\n<\/li>\n
          25. \nBDDs verified in a proof assistant<\/a>\n<\/li>\n
          26. \nIsabelle Repository for Relational and Algebraic Methods<\/a>\n<\/li>\n
          27. \nAutomated Engineering of Relational and Algebraic Methods in Isabelle\/HOL<\/a>\n<\/li>\n<\/ol>\n

            Matita<\/h2>\n
              \n
            1. \nFormal Metatheory of Programming Languages in the Matita Interactive Theorem Prover<\/a>\n<\/li>\n<\/ol>\n

              Mizar<\/h2>\n
                \n
              1. \nConway\u2019s Games and Some of Their Basic Properties<\/a>\n<\/li>\n<\/ol>\n

                Otter o Prover9<\/h2>\n
                  \n
                1. \nL\u00f3gica Computacional en Sevilla (30 a\u00f1os en una hora)<\/a>\n<\/li>\n
                2. \nRecent Developments in Computing and Philosophy<\/a>\n<\/li>\n
                3. \nComputational Meta-Ethics: Towards the Meta-Ethical Robot<\/a>\n<\/li>\n<\/ol>\n

                  PVS<\/h2>\n
                    \n
                  1. \nL\u00f3gica Computacional en Sevilla (30 a\u00f1os en una hora)<\/a>\n<\/li>\n
                  2. \nTowards a verification framework for faulty message passing systems in PVS<\/a>\n<\/li>\n
                  3. \nA Formal Proof Of The Riesz Representation Theorem<\/a>\n<\/li>\n
                  4. \nComputationally-Discovered Simplification of the Ontological Argument<\/a>\n<\/li>\n
                  5. \nFormaliza\u00e7\u00e3o da prova do teorema de exist\u00eancia de unificadores mais gerais em teorias de primeira-ordem<\/a>\n<\/li>\n
                  6. \nModelling Distributed Cognition Systems in PVS<\/a>\n<\/li>\n<\/ol>\n

                    Twelfe<\/h2>\n
                      \n
                    1. \nRepresenting model theory in a type-theoretical logical framework<\/a>\n<\/li>\n<\/ol>\n","protected":false},"excerpt":{"rendered":"

                      Esta entrada es una recopilaci\u00f3n de lecturas sobre razonamiento formalizado que hemos compartido este curso en la lista de correo del grupo de l\u00f3gica computacional. La recopilaci\u00f3n de los est\u00e1 ordenada seg\u00fan el sistema de razonamiento utilizado (ACL2, Agda, Coq, HOL, Isabelle, Matita, Mizar, Otter\/Prover9, PVS \u00f3 Twelfe) y, dentro de cada uno, por la…<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1451"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=1451"}],"version-history":[{"count":7,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1451\/revisions"}],"predecessor-version":[{"id":1494,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/1451\/revisions\/1494"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=1451"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=1451"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=1451"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}