Resumen de lecturas compartidas durante diciembre de 2019
Esta entrada es una recopilación de lecturas compartidas, durante diciembre de 2019, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
- A formal proof of the independence of the continuum hypothesis. ~ Jesse Michael Han, Floris van Doorn. #ITP #LeanProver #Math
- Coq Coq correct! Verification of type checking and erasure for Coq, in Coq. ~ M. Sozeau et als. #ITP #Coq
- Verified and verifiable computation with STV algorithms. ~ M.K. Ghale. #PhD_Thesis #ITP #Coq #HOL4
- Exploring Euler’s foundations of differential calculus in Isabelle/HOL using nonstandard analysis. ~ J. Rockel. #MsC_Thesis #ITP #IsabelleHOL #Math
- Learning functional programming. ~ S. Thompson. #FunctionalProgramming #Haskell
- How Julia Robinson helped define the limits of mathematical knowledge. ~ Evelyn Lamb (@evelynjlamb). #Math
- A formal proof of PAC learnability for decision stumps. ~ J. Tassarotti, J.B. Tristan, K. Vajjha. #ITP #LeanProver
- How does Haskell make your life easier? ~ William Yao (@williamyaoh). #Haskell #FunctionalProgramming
- Introducción de Emacs: Trabajo con ventanas y buffers. #Emacs
- What maths is in Lean? ~ Kevin Buzzard (@XenaProject). #ITP #LeanProver #Math
- Deriving monadic programs. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
- Formulating the Hamiltonian Path problem as a constraint satisfaction problem. ~ Ozan Erdem (@ozanerdem). #CSP
- What are the advantages and disadvantages of using Haskell to implement a domain specific language? ~ Tikhon Jelvis. #Haskell #FunctionalProgramming #DSL
- A computability proof of Gödel’s first incompleteness theorem. ~ Jørgen Veisdal (@JorgenVeisdal). #Logic #Math
- Verifying information flow control libraries. ~ M. Vassena. #PhD_Thesis #ITP #Agda
- Category theory by example. ~ I. Murashko, A. Radkov, M, Minshin. #CategoryTheory #Haskell #Scala #Cpp
- An implementation of polygraphs. ~ Maxime Lucas. #ITP #Coq
- The lambda calculus: A historical and practical tour. ~ R.B. Elrod. #LambdaCalculus
- Se logra factorizar el semiprimo RSA-240 de 795 bits. ~ Francisco R. Villatoro (@emulenews). #Matemáticas #Computación
- Deep learning for symbolic mathematics. ~ Guillaume Lample (@GuillaumeLample), François Charton. #DeepLearning via @__josejuan__
- 45 years of formal methods: Challenges and trends. ~ D. Bjørner, K. Havelund. #FormalMethods
- Semialgebraic proofs and efficient algorithm design. ~ Noah Fleming, Pravesh Kothari, Toniann Pitassi. #Logic
- FourierSAT: A Fourier expansion-based algebraic framework for solving hybrid boolean constraints. ~ A. Kyrillidis, A. Shrivastava, M.Y. Vardi, Z. Zhang. #ATP #Logic #SAT_solving
- A probabilistic approach to satisfiability of propositional logic formulae. ~ Reazul Hasan Russel. #Logic #ATP #SAT
- Correctness proofs of distributed systems with Isabelle. ~ Martin Kleppmann. #ITP #IsabelleHOL
- Mathematics for Computer Science: “Top 10 proof techniques NOT allowed”. #Logic
- Exploring the structure of an algebra text with locales. ~ Clemens Ballarin. #ITP #IsabelleHOL #Math
- Higher-order, higher-order automatic differentiation. ~ Conal Elliott (@conal). #Haskell #FunctionalProgramming
- Haskell implementation of open games. ~ Jules Hedges (@_julesh_). #Haskell #FunctionalProgramming
- Four ways to partially apply constraint tuples. ~ Ryan Scott. #Haskell #FunctionalProgramming
- Mechanized verification of the correctness and asymptotic complexity of programs. ~ Armaël Guéneau. #PhD_Thesis #ITP #Coq
- Challenges in the collaborative evolution of a proof language and its ecosystem. ~ Théo Zimmermann. #PhD_Thesis #ITP #Coq
- Haskell vs OCaml. ~ Mark Karpov (@mrkkrp). #Haskell #OCaml #FunctionalProgramming
- Non-reformist reform for Haskell modularity. ~ Scott Kilpatrick. #PhD_Thesis #Haskell #FunctionalProgramming
- Efficient sampling of SAT and SMT solutions for testing and verification. ~ Rafael Tupynambá Dutra. #PhD_Thesis #SAT #SMT
- A list of Haskell articles on good design, good testing. ~ Michael Oswald (@OswaldChocolate). #Haskell #FunctionalProgramming
- An online JavaScript/WebAssembly version of Lean. #ITP #LeanProver
- Rigorous mathematics. ~ Kevin Buzzard (@XenaProject). #ITP #Math
- Measuring Haskell container sizes. ~ Colin Woodbury (@fosskers). #Haskell #FunctionalProgramming
- Data types in Rust: Borrowing from both worlds. ~ James Bowen (@james_OWA). #Rust #Haskell
- Reanimate: a library for programmatically generating animations with a twist towards mathematics / vector drawings. #Haskell
- Ghosts of departed proofs convenience. ~ Chris Done (@christopherdone). #Haskell
- Correct-by-construction typechecking with scope graphs. ~ Katherine Imhoff Casamento. #MSc_Thesis #ITP #Agda
- To understand the future of AI, study its past. ~ Rob Toews. #AI
- Exploration of neural machine translation in autoformalization of mathematics in Mizar. ~ Q. Wang, C. Brown, C. Kaliszyk, J. Urban. #MachineLearning #ITP #Mizar
- A constructive formalization of the weak perfect graph theorem. ~ A.K. Singh, R. Natarajan. #ITP #Coq #Math
- Biortogonalidad para corrección de compiladores y adecuación computacional. ~ Alejandro E. Gadea. #PhD_Thesis #ITP #Coq
- Introduction to computational thinking: a new high school curriculum using CodeWorld. ~ F. Alegre, J. Underwoood, J. Moreno, M. Alegre. #CodeWorld #Haskel #FunctionalProgramming #Teaching
- A generic framework for verified compilers using Isabelle/HOL’s locales. ~ M. Desharnais, S. Brunthaler. #ITP #IsabelleHOL
- Logic in secondary education. ~ Michael Genesereth, Vinay Chaudhri. #Logic #Teaching
- A survey on theorem provers in formal methods. ~ M.S. Nawaz, M. Malik, Y. Li, M. Sun, M. Lali. #ITP #ATP
- Higher-order, higher-order automatic differentiation. ~ Conal Elliott (@conal). #Haskell
- Introduction to lambda calculus. ~ G. Smolka. #LambdaCalculus
- Computational type theory and interactive theorem proving with Coq. ~ G. Smolka. #eBook #ITP #Coq
- Mathematician proves huge result on ‘dangerous’ problem. ~ Kevin Hartnett. #Math
- Lazy constructive numbers and the Stern-Brocot tree. ~ Donnacha Oisín Kidney (@oisdk). #Haskell #Agda #FunctionalProgramming
- Formalization of some central theorems in combinatorics of finite sets. ~ Abhishek Kr Singh. #ITP #Coq #Math
- Programming algorithms: dynamic programming. ~ Vsevolod Dyomkin. #Programming #CommonLisp
- Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen. #Haskell #FunctionalProgramming
- Dependently typed Haskell in industry (experience report). ~ David Thrane Christiansen et als. #Haskell #FunctionalProgramming
- Automatic extraction of Hilbert Calculi associated to fragments of classical logic. ~ Joel Felipe Ferreira Gomes. #BSc_Thesis #Haskell #Logic
- Fibonacci formalized 1: some sums. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math
- Fibonacci formalized 2: bees and cars. ~ Bryan Gin-ge Chen (@blockspins). #ITP #LeanProver #Math
- A predicate transformer semantics for effects. ~ Wouter Swierstra, Tim Baanen. #Agda #FunctionalProgramming #ITP
- Running Lisp in production. ~ Vsevolod Dyomkin. #CommonLisp
- A formal proof of the irrationality of ζ(3). ~ Assia Mahboubi, Thomas Sibut-Pinote. #ITP #Coq #Math
- REPLica: REPL instrumentation for Coq analysis. ~ Talia Ringer (@TaliaRinger) et als. #ITP #Coq
- Runtime support for multicore Haskell: a retrospective. ~ Simon Marlowe, Simon Peyton Jones, and Satnam Singh. #Haskell #FunctionalProgramming
- Casa and Stack. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming
- PrologCheatSheet: Basics of relational programming with Prolog. ~ Musa Al-hassy. #Prolog #LogicProgramming
- Incomplete and utter introduction to modal logic, Pt. 1. ~ Danya Rogozin. #Logic
- Fun with formal methods for better education. ~ N. Shilov, E. Muravev, S. Shilova. #FormalMethods #Math
- On the expressive power of indexed applicative and monadic structures. ~ Jan Malakhovski. #PhD_Thesis #Haskell #FunctionalProgramming
- Donald Knuth reflects on 50 years of ‘The Art of Computer Programming‘. #Programming
- The Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler and Yong Kiam Tan. #ITP #IsabelleHOL #Math
- The Lean mathematical library. ~ The mathlib Community. #ITP #LeanProver #Math
- Top 10 Haskell open-source projects for Linux users. ~ Jonn Mostovoy. #Haskell #FunctionalProgramming
- Course about numerical Python. ~ Rafa Rodríguez Galván (@cucharro). #Programming #Python #Math
- Kurt Gödel and the mechanization of mathematics. ~ Juliette Kennedy. #Math #Logic
- Logic for exact real arithmetic. ~ H. Schwichtenberg, F. Wiesnet. #Logic #Math #Minlog #Haskell
- Isabelle/C: a framework for C code in C11 syntax deeply integrated into the Isabelle/PIDE development environment. ~ F. Tuong, B. Wolff. #ITP #Isabelle
- Counting inversions via rank queries. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Algebraic lenses. ~ Chris Penner (@chrislpenner). #Haskell #FunctionalProgramming
- Haskell art in your browser with Asterius. ~ Sylvain Henry, Shao Cheng. #Haskell #FunctionalProgramming
- Presentación del método de Polya para la resolución de problemas. ~ Jimena Fernández García. #Heurística
- 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. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- Prefer to use fail for IO exceptions. ~ G. Gonzalez (@GabrielG439). #Haskell #FunctionalProgramming
- Automated reasoning and robotics. ~ Zainab Al Kashari, Fatma Al Taheri. #ATP
- Calculemus! ~ Brian Hayes (@bit_player). #Programming #Math
- A verified prover based on ordered resolution. ~ A. Schlichtkrull, J.C. Blanchette, D. Traytel. #ITP #IsabelleHOL
- Formal verification of a constant-time preserving C compiler. ~ G. Barthe et als. #ITP #Coq
- Programming and interactive proving with Z3Py. ~ Philip Zucker (@SandMouth). #ITP #Z3
- Liquidate your assets: reasoning about resource usage in Liquid Haskell. ~ M.A.T. Handley, N. Vazou, G. Hutton. #Haskell #FunctionalProgramming #LiquidHaskell
- A glossary of functional programming. ~ John A De Goes #FunctionalProgramming
- Notes on Category Theory with examples from basic mathematics. ~ Paolo Perrone (@PaoloPerrone8). #CategoryTheory #Math
- Functional programming and justice in a world without time. ~ Anirudh Eka (@anirudh_eka). #FunctionalProgramming
- A categorical view of computational effects. ~ Emily Riehl. #CategoryTheory #Math #Programming
- Formalising Mathematics in praxis: a mathematician’s first experiences with Isabelle/HOL and the why and how of getting started. ~ Angeliki Koutsoukou-Argyraki (@AngelikiKoutso1). #ITP #IsabelleHOL #Math
- Deterministic pushdown automata as specifications for discrete event supervisory control in Isabelle. ~ Sven Schneider. #PhD_Thesis #ITP #IsabelleHOL
- Stupid Z3Py tricks: verifying sorting networks off of Wikipedia. ~ Philip Zucker (@SandMouth). #Z3 #SMT
- Notes on Category Theory in Scala 3 (Dotty). ~ Juan Pablo Romero (@1jpablo1). #CategoryTheory #Scala #FunctionalProgramming
- Quotients in Coq. ~ Arthur Azevedo de Amorim. #ITP #Coq
- A verification challenge. ~ Arthur Azevedo de Amorim. #ITP #Coq
- Cohomology for kids. ~ @RAnachro. #Math
- A few Haskell highlights of 2019. ~ Gints Dreimanis. #Haskell #FunctionalProgramming
- Python type hints. ~ Guilherme Kunigami (@kunigami). #Python #Programming
- Three equivalent ordinal notation systems in cubical Agda. ~ F.N. Forsberg, C. Xu, N. Ghani. #ITP #Agda
- Intrinsically-typed definitional interpreters for linear, session-typed languages. ~ A. Rouvoet et als. #ITP #Agda
- More stupid Z3Py tricks: Simple proofs. ~ Philip Zucker (@SandMouth). #Z3 #SMT
- 12 beautiful mathematical theorems with short proofs. ~ Jörg Neunhäuserer. #Math
- Some fundamental theorems in mathematics. ~ Oliver Knill. #Math
- Famous conjectures in mathematics. ~ Béla Bajnok. #Math
- Thirty-six unsolved problems in number theory. ~ F. Smarandache. #Math
- Famous mistakes in mathematics. ~ J. Pogonowski. #Math
- Formalizing determinacy of concurrent revisions. ~ Roy Overbeek. #ITP #IsabelleHOL
- A complete axiomatisation of a fragment of language algebra. ~ Paul Brunet. #ITP #Coq #Math
- A mechanized formalization of GraphQL. ~ T. Díaz, F. Olmedo, É. Tanter. #ITP #Coq
- Stupid Z3Py tricks strikes back: Verifying a Keras neural network. ~ Philip Zucker (@SandMouth). #Z3 #SMT #Keras #NeuralNetworks
- Teaching Haskell with Duet. ~ Chris Done (@christopherdone). #Haskell #FunctionalProgramming #Duet
- The Poincaré-Bendixson theorem in Isabelle/HOL. ~ Fabian Immler, Yong Kiam Tan. #ITP #IsabelleHOL #Math
- Verifying x86 instruction implementations. ~ S. Goel et als. #ITP #ACL2