{"id":6920,"date":"2020-01-01T07:13:50","date_gmt":"2020-01-01T06:13:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6920"},"modified":"2020-01-07T07:16:31","modified_gmt":"2020-01-07T06:16:31","slug":"resumen-de-lecturas-compartidas-durante-diciembre-de-2019","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resumen-de-lecturas-compartidas-durante-diciembre-de-2019\/","title":{"rendered":"Resumen de lecturas compartidas durante diciembre de 2019"},"content":{"rendered":"<div id=\"content\">\n<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2019, en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a> fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador.<\/p>\n<p>Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en <a href=\"https:\/\/twitter.com\/Jose_A_Alonso\">Twitter<\/a>.<\/p>\n<p>Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.<\/p>\n<p>Una recopilaci\u00f3n de todas las lecturas compartidas se encuentra en <a href=\"https:\/\/github.com\/jaalonso\/Lecturas_GLC\">GitHub<\/a>.<\/p>\n<p><!--more--><\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/flypitch.github.io\/assets\/flypitch-cpp.pdf\">A formal proof of the independence of the continuum hypothesis<\/a>. ~ Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02380196\/document\">Coq Coq correct! Verification of type checking and erasure for Coq, in Coq<\/a>. ~ M. Sozeau et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/openresearch-repository.anu.edu.au\/bitstream\/1885\/176977\/1\/MyThesisFinal.pdf\">Verified and verifiable computation with STV algorithms<\/a>. ~ M.K. Ghale. #PhD_Thesis #ITP #Coq #HOL4<\/li>\n<li><a href=\"https:\/\/project-archive.inf.ed.ac.uk\/msc\/20193307\/msc_proj.pdf\">Exploring Euler\u2019s foundations of differential calculus in Isabelle\/HOL using nonstandard analysis<\/a>. ~ J. Rockel. #MsC_Thesis #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/pdfs.semanticscholar.org\/a1ce\/e17fc0fbe24b2da553fd72b44cd62fbacf61.pdf\">Learning functional programming<\/a>. ~ S. Thompson. #FunctionalProgramming #Haskell<\/li>\n<li><a href=\"https:\/\/www.sciencenews.org\/article\/how-julia-robinson-helped-define-limits-mathematical-knowledge\">How Julia Robinson helped define the limits of mathematical knowledge<\/a>. ~ Evelyn Lamb (@evelynjlamb). #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1911.00385\">A formal proof of PAC learnability for decision stumps<\/a>. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/williamyaoh.com\/posts\/2019-11-30-how-does-haskell-make-life-easier.html\">How does Haskell make your life easier?<\/a> ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/notxor.nueva-actitud.org\/blog\/2019\/11\/30\/trabajo-con-ventanas-y-buffers\/\">Introducci\u00f3n de Emacs: Trabajo con ventanas y buffers<\/a>. #Emacs<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/what-maths-is-in-lean\/\">What maths is in Lean?<\/a> ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/scm.iis.sinica.edu.tw\/home\/2019\/deriving-monadic-programs\/\">Deriving monadic programs<\/a>. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ozanerdem.github.io\/jekyll\/update\/2019\/12\/01\/representation-in-csp.html\">Formulating the Hamiltonian Path problem as a constraint satisfaction problem<\/a>. ~ Ozan Erdem (@ozanerdem). #CSP<\/li>\n<li><a href=\"https:\/\/www.quora.com\/What-are-the-advantages-and-disadvantages-of-using-Haskell-to-implement-a-domain-specific-language\/answer\/Tikhon-Jelvis?ch=2&amp;srid=p9P3\">What are the advantages and disadvantages of using Haskell to implement a domain specific language?<\/a> ~ Tikhon Jelvis. #Haskell #FunctionalProgramming #DSL<\/li>\n<li><a href=\"https:\/\/medium.com\/cantors-paradise\/a-computability-proof-of-g%C3%B6dels-first-incompleteness-theorem-2d685899117c\">A computability proof of G\u00f6del\u2019s first incompleteness theorem<\/a>. ~ J\u00f8rgen Veisdal (@JorgenVeisdal). #Logic #Math<\/li>\n<li><a href=\"https:\/\/research.chalmers.se\/publication\/508494\/file\/508494_Fulltext.pdf\">Verifying information flow control libraries<\/a>. ~ M. Vassena. #PhD_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/nbviewer.jupyter.org\/github\/CatTheoryByExample\/book\/blob\/master\/cattheory.pdf\">Category theory by example<\/a>. ~ I. Murashko, A. Radkov, M, Minshin. #CategoryTheory #Haskell #Scala #Cpp<\/li>\n<li><a href=\"https:\/\/hal.archives-ouvertes.fr\/hal-02385110\/document\">An implementation of polygraphs<\/a>. ~ Maxime Lucas. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/codeblock.fedorapeople.org\/chapter.pdf\">The lambda calculus: A historical and practical tour<\/a>. ~ R.B. Elrod. #LambdaCalculus<\/li>\n<li><a href=\"https:\/\/francis.naukas.com\/2019\/12\/03\/se-logra-factorizar-el-semiprimo-rsa-240-de-795-bits\/\">Se logra factorizar el semiprimo RSA-240 de 795 bits<\/a>. ~ Francisco R. Villatoro (@emulenews). #Matem\u00e1ticas #Computaci\u00f3n<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.01412\">Deep learning for symbolic mathematics<\/a>. ~ Guillaume Lample (@GuillaumeLample), Fran\u00e7ois Charton. #DeepLearning via @__josejuan__<\/li>\n<li><a href=\"http:\/\/www.imm.dtu.dk\/~dibj\/2019\/45years\/45years.pdf\">45 years of formal methods: Challenges and trends<\/a>. ~ D. Bj\u00f8rner, K. Havelund. #FormalMethods<\/li>\n<li><a href=\"https:\/\/eccc.weizmann.ac.il\/report\/2019\/106\/%20\">Semialgebraic proofs and efficient algorithm design<\/a>. ~ Noah Fleming, Pravesh Kothari, Toniann Pitassi. #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.01032\">FourierSAT: A Fourier expansion-based algebraic framework for solving hybrid boolean constraints<\/a>. ~ A. Kyrillidis, A. Shrivastava, M.Y. Vardi, Z. Zhang. #ATP #Logic #SAT_solving<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.02150\">A probabilistic approach to satisfiability of propositional logic formulae<\/a>. ~ Reazul Hasan Russel. #Logic #ATP #SAT<\/li>\n<li><a href=\"https:\/\/youtu.be\/NfdP6wwjsGk\">Correctness proofs of distributed systems with Isabelle<\/a>. ~ Martin Kleppmann. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/mitadmissions.org\/blogs\/entry\/mathematics-for-computer-science-top-10-proof-techniques-not-allowed\/\">Mathematics for Computer Science: &#8220;Top 10 proof techniques NOT allowed&#8221;<\/a>. #Logic<\/li>\n<li><a href=\"http:\/\/www21.in.tum.de\/~ballarin\/publications\/jar2019.pdf\">Exploring the structure of an algebra text with locales<\/a>. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"http:\/\/conal.net\/papers\/higher-order-ad\/higher-order-ad.pdf\">Higher-order, higher-order automatic differentiation<\/a>. ~ Conal Elliott (@conal). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/jules-hedges\/open-games-hs\">Haskell implementation of open games<\/a>. ~ Jules Hedges (@_julesh_). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/ryanglscott.github.io\/2019\/11\/30\/four-ways-to-partially-apply-constraint-tuples\/\">Four ways to partially apply constraint tuples<\/a>. ~ Ryan Scott. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/gallium.inria.fr\/~agueneau\/phd\/manuscript.pdf\">Mechanized verification of the correctness and asymptotic complexity of programs<\/a>. ~ Arma\u00ebl Gu\u00e9neau. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.irif.fr\/_media\/users\/theo\/memoirthesis.pdf\">Challenges in the collaborative evolution of a proof language and its ecosystem<\/a>. ~ Th\u00e9o Zimmermann. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/markkarpov.com\/post\/haskell-vs-ocaml.html\">Haskell vs OCaml<\/a>. ~ Mark Karpov (@mrkkrp). #Haskell #OCaml #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.mpi-sws.org\/\">Non-reformist reform for Haskell modularity<\/a>. ~ Scott Kilpatrick. #PhD_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/people.eecs.berkeley.edu\/~rtd\/PhD%20Rafael%20Tupynamb%C3%A1%20Dutra.pdf\">Efficient sampling of SAT and SMT solutions for testing and verification<\/a>. ~ Rafael Tupynamb\u00e1 Dutra. #PhD_Thesis #SAT #SMT<\/li>\n<li><a href=\"https:\/\/www.onikudaki.net\/blog\/wp-content\/uploads\/2019\/12\/HaskellArticles-1.pdf\">A list of Haskell articles on good design, good testing<\/a>. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/\">An online JavaScript\/WebAssembly version of Lean<\/a>. #ITP #LeanProver<\/li>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/2019\/12\/07\/rigorous-mathematics\/\">Rigorous mathematics<\/a>. ~ Kevin Buzzard (@XenaProject). #ITP #Math<\/li>\n<li><a href=\"https:\/\/www.fosskers.ca\/blog\/container-sizes-en.html\">Measuring Haskell container sizes<\/a>. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/mmhaskell.com\/blog\/2019\/12\/9\/data-types-in-rust-borrowing-from-both-worlds\">Data types in Rust: Borrowing from both worlds<\/a>. ~ James Bowen (@james_OWA). #Rust #Haskell<\/li>\n<li><a href=\"https:\/\/reanimate.readthedocs.io\/en\/latest\/glue_tut\/\">Reanimate: a library for programmatically generating animations with a twist towards mathematics \/ vector drawings<\/a>. #Haskell<\/li>\n<li><a href=\"https:\/\/chrisdone.com\/posts\/ghost-of-departed-proofs-conveniences\/\">Ghosts of departed proofs convenience<\/a>. ~ Chris Done (@christopherdone). #Haskell<\/li>\n<li><a href=\"https:\/\/pdxscholar.library.pdx.edu\/cgi\/viewcontent.cgi?article=6344&amp;context=open_access_etds\">Correct-by-construction typechecking with scope graphs<\/a>. ~ Katherine Imhoff Casamento. #MSc_Thesis #ITP #Agda<\/li>\n<li><a href=\"https:\/\/www.forbes.com\/sites\/robtoews\/2019\/11\/17\/to-understand-the-future-of-ai-study-its-past\/\">To understand the future of AI, study its past<\/a>. ~ Rob Toews. #AI<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.02636\">Exploration of neural machine translation in autoformalization of mathematics in Mizar<\/a>. ~ Q. Wang, C. Brown, C. Kaliszyk, J. Urban. #MachineLearning #ITP #Mizar<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.02211\">A constructive formalization of the weak perfect graph theorem<\/a>. ~ A.K. Singh, R. Natarajan. #ITP #Coq #Math<\/li>\n<li><a href=\"https:\/\/rdu.unc.edu.ar\/handle\/11086\/14324\">Biortogonalidad para correcci\u00f3n de compiladores y adecuaci\u00f3n computacional<\/a>. ~ Alejandro E. Gadea. #PhD_Thesis #ITP #Coq<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.00237\">Introduction to computational thinking: a new high school curriculum using CodeWorld<\/a>. ~ F. Alegre, J. Underwoood, J. Moreno, M. Alegre. #CodeWorld #Haskel #FunctionalProgramming #Teaching<\/li>\n<li><a href=\"https:\/\/martin.desharnais.me\/public\/documents\/jfla2020-framework-CertComp.pdf\">A generic framework for verified compilers using Isabelle\/HOL&#8217;s locales<\/a>. ~ M. Desharnais, S. Brunthaler. #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/web.stanford.edu\/~vinayc\/intrologic\/html\/full.html\">Logic in secondary education<\/a>. ~ Michael Genesereth, Vinay Chaudhri. #Logic #Teaching<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.03028\">A survey on theorem provers in formal methods<\/a>. ~ M.S. Nawaz, M. Malik, Y. Li, M. Sun, M. Lali. #ITP #ATP<\/li>\n<li><a href=\"http:\/\/conal.net\/papers\/higher-order-ad\/higher-order-ad.pdf\">Higher-order, higher-order automatic differentiation<\/a>. ~ Conal Elliott (@conal). #Haskell<\/li>\n<li><a href=\"http:\/\/www.ps.uni-saarland.de\/courses\/sem-ws19\/lambda-intro.pdf\">Introduction to lambda calculus<\/a>. ~ G. Smolka. #LambdaCalculus<\/li>\n<li><a href=\"http:\/\/www.ps.uni-saarland.de\/~smolka\/drafts\/icl2019.pdf\">Computational type theory and interactive theorem proving with Coq<\/a>. ~ G. Smolka. #eBook #ITP #Coq<\/li>\n<li><a href=\"https:\/\/www.quantamagazine.org\/mathematician-terence-tao-and-the-collatz-conjecture-20191211\/\">Mathematician proves huge result on \u2018dangerous\u2019 problem<\/a>. ~ Kevin Hartnett. #Math<\/li>\n<li><a href=\"https:\/\/doisinkidney.com\/posts\/2019-12-14-stern-brocot.html\">Lazy constructive numbers and the Stern-Brocot tree<\/a>. ~ Donnacha Ois\u00edn Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1703.10977\">Formalization of some central theorems in combinatorics of finite sets<\/a>. ~ Abhishek Kr Singh. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/lisp-univ-etc.blogspot.com\/2019\/12\/programming-algorithms-dp.html\">Programming algorithms: dynamic programming<\/a>. ~ Vsevolod Dyomkin. #Programming #CommonLisp<\/li>\n<li><a href=\"https:\/\/youtu.be\/Q6PKdRDKcKA\">Dependently typed Haskell in industry (experience report)<\/a>. ~ David Thrane Christiansen. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.davidchristiansen.dk\/pubs\/dependent-haskell-experience-report.pdf\">Dependently typed Haskell in industry (experience report)<\/a>. ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/monografias.ufrn.br:8080\/jspui\/bitstream\/123456789\/9912\/1\/Monografia__Joel_Felipe.pdf\">Automatic extraction of Hilbert Calculi associated to fragments of classical logic<\/a>. ~ Joel Felipe Ferreira Gomes. #BSc_Thesis #Haskell #Logic<\/li>\n<li><a href=\"https:\/\/observablehq.com\/@bryangingechen\/fibonacci-formalized-1-some-sums\">Fibonacci formalized 1: some sums<\/a>. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/observablehq.com\/@bryangingechen\/fibonacci-formalized-2-bees-and-cars\">Fibonacci formalized 2: bees and cars<\/a>. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math<\/li>\n<li><a href=\"http:\/\/www.staff.science.uu.nl\/~swier004\/publications\/2019-icfp-submission-a.pdf\">A predicate transformer semantics for effects<\/a>. ~ Wouter Swierstra, Tim Baanen. #Agda #FunctionalProgramming #ITP<\/li>\n<li><a href=\"https:\/\/tech.grammarly.com\/blog\/running-lisp-in-production\">Running Lisp in production<\/a>. ~ Vsevolod Dyomkin. #CommonLisp<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.06611\">A formal proof of the irrationality of \u03b6(3)<\/a>. ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/tlringer.github.io\/pdf\/analytics.pdf\">REPLica: REPL instrumentation for Coq analysis<\/a>. ~ Talia Ringer (@TaliaRinger) et als. #ITP #Coq<\/li>\n<li><a href=\"https:\/\/blog.sigplan.org\/2019\/12\/16\/runtime-support-for-multicore-haskell-a-retrospective\/\">Runtime support for multicore Haskell: a retrospective<\/a>. ~ Simon Marlowe, Simon Peyton Jones, and Satnam Singh. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/tech.fpcomplete.com\/blog\/casa-and-stack\">Casa and Stack<\/a>. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/alhassy\/PrologCheatSheet\">PrologCheatSheet: Basics of relational programming with Prolog<\/a>. ~ Musa Al-hassy. #Prolog #LogicProgramming<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/incomplete-and-utter-introduction-to-modal-logic\">Incomplete and utter introduction to modal logic, Pt<\/a>. 1. ~ Danya Rogozin. #Logic<\/li>\n<li><a href=\"https:\/\/fmfun.github.io\/Papers-2019\/Shilov-Muravev-Shilova.pdf\">Fun with formal methods for better education<\/a>. ~ N. Shilov, E. Muravev, S. Shilova. #FormalMethods #Math<\/li>\n<li><a href=\"https:\/\/oxij.org\/thesis\/PhD\/PhD.xetex.pdf\">On the expressive power of indexed applicative and monadic structures<\/a>. ~ Jan Malakhovski. #PhD_Thesis #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/dentondaily.com\/donald-knuth-reflects-on-50-years-of-the-art-of-computer-programming\/\">Donald Knuth reflects on 50 years of \u2018The Art of Computer Programming\u2018<\/a>. #Programming<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Poincare_Bendixson.html\">The Poincar\u00e9-Bendixson theorem in Isabelle\/HOL<\/a>. ~ Fabian Immler and Yong Kiam Tan. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1910.09336\">The Lean mathematical library<\/a>. ~ The mathlib Community. #ITP #LeanProver #Math<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/top-haskell-open-source-projects-for-linux\">Top 10 Haskell open-source projects for Linux users<\/a>. ~ Jonn Mostovoy. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/github.com\/rrgalvan\/numerical_python_course\">Course about numerical Python<\/a>. ~ Rafa Rodr\u00edguez Galv\u00e1n (@cucharro). #Programming #Python #Math<\/li>\n<li><a href=\"https:\/\/www.the-tls.co.uk\/articles\/kurt-godel-incompleteness-theorems\/\">Kurt G\u00f6del and the mechanization of mathematics<\/a>. ~ Juliette Kennedy. #Math #Logic<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1904.12763\">Logic for exact real arithmetic<\/a>. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Math #Minlog #Haskell<\/li>\n<li><a href=\"https:\/\/www.isa-afp.org\/entries\/Isabelle_C.html\">Isabelle\/C: a framework for C code in C11 syntax deeply integrated into the Isabelle\/PIDE development environment<\/a>. ~ F. Tuong, B. Wolff. #ITP #Isabelle<\/li>\n<li><a href=\"https:\/\/byorgey.wordpress.com\/2019\/12\/18\/counting-inversions-via-rank-queries\/\">Counting inversions via rank queries<\/a>. ~ Brent Yorgey. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/chrispenner.ca\/posts\/algebraic\">Algebraic lenses<\/a>. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/www.tweag.io\/posts\/2019-12-19-asterius-diagrams.html\">Haskell art in your browser with Asterius<\/a>. ~ Sylvain Henry, Shao Cheng. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/prezi.com\/0wifreih-iwe\/como-plantear-y-resolver-problemas-g-polya\/\">Presentaci\u00f3n del m\u00e9todo de Polya para la resoluci\u00f3n de problemas<\/a>. ~ Jimena Fern\u00e1ndez Garc\u00eda. #Heur\u00edstica<\/li>\n<li><a href=\"https:\/\/cs-syd.eu\/posts\/2019-12-14-pretty-relative-time\">pretty-relative-time: a little library to describe dates and times in the future or in the past in a nice, human readable, familiar feeling way<\/a>. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.haskellforall.com\/2019\/12\/prefer-to-use-fail-for-io-exceptions.html\">Prefer to use fail for IO exceptions<\/a>. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/asrjetsjournal.org\/index.php\/American_Scientific_Journal\/article\/view\/5418\">Automated reasoning and robotics<\/a>. ~ Zainab Al Kashari, Fatma Al Taheri. #ATP<\/li>\n<li><a href=\"https:\/\/www.americanscientist.org\/article\/calculemus%20CompSci\">Calculemus!<\/a> ~ Brian Hayes (@bit_player). #Programming #Math<\/li>\n<li><a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/fun_rp_paper.pdf\">A verified prover based on ordered resolution<\/a>. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/eprint.iacr.org\/2019\/926.pdf\">Formal verification of a constant-time preserving C compiler<\/a>. ~ G. Barthe et als. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/programming-and-interactive-proving-with-z3py\/\">Programming and interactive proving with Z3Py<\/a>. ~ Philip Zucker (@SandMouth). #ITP #Z3<\/li>\n<li><a href=\"http:\/\/www.cs.nott.ac.uk\/~psxmah\/liquidate.pdf\">Liquidate your assets: reasoning about resource usage in Liquid Haskell<\/a>. ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #FunctionalProgramming #LiquidHaskell<\/li>\n<li><a href=\"http:\/\/degoes.net\/articles\/fp-glossary\">A glossary of functional programming<\/a>. ~ John A De Goes #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.10642\">Notes on Category Theory with examples from basic mathematics<\/a>. ~ Paolo Perrone (@PaoloPerrone8). #CategoryTheory #Math<\/li>\n<li><a href=\"https:\/\/hackernoon.com\/justice-in-a-world-without-time-tp1p33a2\">Functional programming and justice in a world without time<\/a>. ~ Anirudh Eka (@anirudh_eka). #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/www.math.jhu.edu\/~eriehl\/compose.pdf\">A categorical view of computational effects<\/a>. ~ Emily Riehl. #CategoryTheory #Math #Programming<\/li>\n<li><a href=\"https:\/\/www.researchgate.net\/publication\/334549483_FORMALISING_MATHEMATICS_-IN_PRAXIS_A_MATHEMATICIAN%27S_FIRST_EXPERIENCES_WITH_ISABELLEHOL_AND_THE_WHY_AND_HOW_OF_GETTING_STARTED\">Formalising Mathematics in praxis: a mathematician&#8217;s first experiences with Isabelle\/HOL and the why and how of getting started<\/a>. ~ Angeliki Koutsoukou-Argyraki (@AngelikiKoutso1). #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/depositonce.tu-berlin.de\/bitstream\/11303\/10372\/4\/schneider_sven.pdf\">Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle<\/a>. ~ Sven Schneider. #PhD_Thesis #ITP #IsabelleHOL<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/stupid-z3py-tricks-verifying-sorting-networks-off-of-wikipedia\/\">Stupid Z3Py tricks: verifying sorting networks off of Wikipedia<\/a>. ~ Philip Zucker (@SandMouth). #Z3 #SMT<\/li>\n<li><a href=\"https:\/\/typista.org\/categories-in-dotty\/\">Notes on Category Theory in Scala 3 (Dotty)<\/a>. ~ Juan Pablo Romero (@1jpablo1). #CategoryTheory #Scala #FunctionalProgramming<\/li>\n<li><a href=\"http:\/\/poleiro.info\/posts\/2019-12-25-quotients-in-coq.html\">Quotients in Coq<\/a>. ~ Arthur Azevedo de Amorim. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/poleiro.info\/posts\/2019-12-24-a-verification-challenge.html\">A verification challenge<\/a>. ~ Arthur Azevedo de Amorim. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/blog.deinding.net\/maths\/cohomology.html\">Cohomology for kids<\/a>. ~ @RAnachro. #Math<\/li>\n<li><a href=\"https:\/\/serokell.io\/blog\/haskell-highlights-2019\">A few Haskell highlights of 2019<\/a>. ~ Gints Dreimanis. #Haskell #FunctionalProgramming<\/li>\n<li><a href=\"https:\/\/kunigami.blog\/2019\/12\/26\/python-type-hints\/\">Python type hints<\/a>. ~ Guilherme Kunigami (@kunigami). #Python #Programming<\/li>\n<li><a href=\"https:\/\/personal.cis.strath.ac.uk\/fredrik.nordvall-forsberg\/papers\/ord_cpp2020.pdf\">Three equivalent ordinal notation systems in cubical Agda<\/a>. ~ F.N. Forsberg, C. Xu, N. Ghani. #ITP #Agda<\/li>\n<li><a href=\"https:\/\/eelcovisser.org\/publications\/2020\/RouvoetPKV20-preprint.pdf\">Intrinsically-typed definitional interpreters for linear, session-typed languages<\/a>. ~ A. Rouvoet et als. #ITP #Agda<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/more-stupid-z3py-tricks-simple-proofs\/\">More stupid Z3Py tricks: Simple proofs<\/a>. ~ Philip Zucker (@SandMouth). #Z3 #SMT<\/li>\n<li><a href=\"http:\/\/bit.ly\/2Q5RAbB\">12 beautiful mathematical theorems with short proofs<\/a>. ~ J\u00f6rg Neunh\u00e4userer. #Math<\/li>\n<li><a href=\"http:\/\/people.math.harvard.edu\/~knill\/graphgeometry\/papers\/fundamental.pdf\">Some fundamental theorems in mathematics<\/a>. ~ Oliver Knill. #Math<\/li>\n<li><a href=\"http:\/\/link.springer.com\/content\/pdf\/bbm%253A978-1-4614-6636-9%252F1.pdf\">Famous conjectures in mathematics<\/a>. ~ B\u00e9la Bajnok. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/math\/0010143\">Thirty-six unsolved problems in number theory<\/a>. ~ F. Smarandache. #Math<\/li>\n<li><a href=\"http:\/\/logic.amu.edu.pl\/images\/c\/c6\/Aalcsxxjp.pdf\">Famous mistakes in mathematics<\/a>. ~ J. Pogonowski. #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.09741\">Formalizing determinacy of concurrent revisions<\/a>. ~ Roy Overbeek. #ITP #IsabelleHOL<\/li>\n<li><a href=\"https:\/\/drops.dagstuhl.de\/opus\/volltexte\/2020\/11654\/pdf\/LIPIcs-CSL-2020-11.pdf\">A complete axiomatisation of a fragment of language algebra<\/a>. ~ Paul Brunet. #ITP #Coq #Math<\/li>\n<li><a href=\"http:\/\/pleiad.dcc.uchile.cl\/papers\/2020\/diazAl-cpp2020.pdf\">A mechanized formalization of GraphQL<\/a>. ~ T. D\u00edaz, F. Olmedo, \u00c9. Tanter. #ITP #Coq<\/li>\n<li><a href=\"http:\/\/www.philipzucker.com\/stupid-z3py-tricks-strikes-back-verifying-a-keras-neural-network\/\">Stupid Z3Py tricks strikes back: Verifying a Keras neural network<\/a>. ~ Philip Zucker (@SandMouth). #Z3 #SMT #Keras #NeuralNetworks<\/li>\n<li><a href=\"https:\/\/tech.fpcomplete.com\/blog\/teaching-haskell-with-duet\">Teaching Haskell with Duet<\/a>. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming #Duet<\/li>\n<li><a href=\"http:\/\/www.cs.cmu.edu\/~yongkiat\/files\/poincarebendixson.pdf\">The Poincar\u00e9-Bendixson theorem in Isabelle\/HOL<\/a>. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math<\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/1912.10285\">Verifying x86 instruction implementations<\/a>. ~ S. Goel et als. #ITP #ACL2<\/li>\n<\/ul>\n<\/div>\n<div id=\"postamble\" class=\"status\">\n<p class=\"date\">\n<\/div>\n","protected":false},"excerpt":{"rendered":"<p>Esta entrada es una recopilaci\u00f3n de lecturas compartidas, durante diciembre de 2019, en Twitter fundamentalmente sobre programaci\u00f3n funcional y demostraci\u00f3n asistida por ordenador. Las lecturas est\u00e1n ordenadas seg\u00fan su fecha de publicaci\u00f3n en Twitter. Al final de cada art\u00edculo se encuentran etiquetas relativas a los sistemas que usa o a su contenido. Una recopilaci\u00f3n de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","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":[6],"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\/6920"}],"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=6920"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6920\/revisions"}],"predecessor-version":[{"id":6921,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6920\/revisions\/6921"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6920"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6920"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6920"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}