Resumen de lecturas compartidas durante agosto de 2021
Esta entrada es una recopilación de lecturas compartidas, durante agosto de 2021, 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.
- New Software Foundations release. ~ Benjamin C. Pierce et als. #ITP #Coq
- Modal logic S5 satisfiability in answer set programming. ~ Mario Alviano,a Sotiris Batsakis, George Baryannis. #Logic #ASP #LogicProgramming
- The Dao of Functional Programming (Last updated: August 30, 2021). ~ Bartosz Milewski (@BartoszMilewski). #Haskell #FunctionalProgramming #CategoryTheory
- HIW (The Haskell Implementors’ Workshop) 2021 videos. #Haskell #FunctionalProgramming
- A data-centered user study for proof assistant tools. ~ Hanneli C.A. Tavante. #ITP #Coq#LeanProver
- Latent effects for reusable language components: Extended version. ~ Birthe van den Berg, Tom Schrijvers, Casper Bach-Poulsen, Nicolas Wu. #Haskell #FunctionalProgramming
- Formalising algebraic effects with non-recoverable failure. ~ Timotej Tomandl, Dominic Orchard. #Haskell #FunctionalProgramming
- Sound and automated verification of real-world RTL multipliers. ~ Mertcan Temel, Warren A. Hunt Jr. #ITP #ACL2
- Computer algebra in Julia. ~ Dmitry S. Kulyabov, Anna V. Korolkova. #CAS #JuliaLang #Math
- Dijkstra: O homem que tornou a computação uma ciência. ~ Adriano Santos. #CompSci
- What is category theory and why is it trendy? ~ Katerina Hristova. #Math #CategoryTheory
- Geometry in Lean, a report for mathematicians. ~ Nicolò Cavalleri, Anthony Bordg. #ITP #LeanProver #Math
- Formalizing the Gromov-Hausdorff space. ~ Sébastien Gouëzel. #ITP #LeanProver #Math
- Leibniz equality in Haskell, part 1. ~ Ryan Scott. #Haskell #FunctionalProgramming
- Magical Haskell (modern functional programming and type theory in a fun and accessible way). ~ Anton Antich. #Haskell #FunctionalProgramming #eBook
- Nascent GHC proposal: Source rewrite rules and optional constraints. ~ Chris Smith. #Haskell #FunctionalProgramming
- Life as a logician (An interview with Martin Davis by Allyn Jackson). #Logic #Math #CompSci #AI #MachineLearning
- Une idée assez folle, l’Intelligence Artificielle … (un film sur le parcours d’Alain Colmerauer). #AI #LogicProgramming #Prolog
- Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. ~ Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
- Scalar actions in Lean’s mathlib. ~ Eric Wieser. #ITP #LeanProver #Math
- AI ethics: A call to faculty. ~ Illah Reza Nourbakhsh. #AI
- Multiplicative induction principles for ℕ. ~ Eric Rodriguez. #ITP #LeanProver #Math
- Formalizing Fibonacci squares. ~ Harun Khan. #ITP #LeanProver #Math
- Programación literaria para sysadmins / devops. ~ drymer. #Emacs #OrgMode
- Faster smarter proof by induction in Isabelle/HOL. ~ Yutaka Nagashima. #ITP #IsabelleHOL
- Formalization in Lean of IMO 2006 Q3. ~ Tian Chen. #ITP #LeanProver #Math #IMO
- Verifying C11-style weak memory libraries via refinement. ~ Sadegh Dalvandi, Brijesh Dongol. #ITP #IsabelleHOL
- The design of mathematical language. ~ Jeremy Avigad. #Logic #Math
- Verified optimization. ~ Alexander Bentkamp, Jeremy Avigad. #ITP #LeanProver #Math
- Automatically generalizing theorems using typeclasses. ~ Alexander Best. #ITP #LeanProver
- Formal ML: A LEAN library for proving foundational results in measure theory, probability, statistics, and machine learning, based upon mathlib. #ITP #LeanProver #Math #MachineLearning
- Formalization of Ostrowski theorems in Lean theorem prover. ~ Ryan Lahfad†, Julien Marquet, Hadrien Barral. #ITP #LeanProver #Math
- On correctness and completeness of an n queens program. ~ Włodzimierz Drabent. #LogicProgramming #Prolog
- Colisiones matemáticas que muestran cómo confundir al algoritmo Neural Hash. ~ @Alvy. #AI #MachineLearning
- XAI methods for neural time series classification: A brief review. ~ Ilija Šimić, Vedran Sabol, Eduardo Veas. #DeepLearning #XAI
- A framework for understanding AI-induced field change: How AI technologies are legitimized and institutionalized. ~ Benjamin Cedric Larsen. #AI
- A first course in Artificial Intelligence. ~ Osondu Oguike #eBook #AI
- Machine learning and the continuum hypothesis (How the unprovable concerns the unlearnable). ~ Robert Passmann. #MachineLearning #Math
- Announcing Spectacle – A language for writing and checking formal specifications in Haskell. ~ Jacob Leach. #Haskell #FunctionalProgramming
- The Oxford Invariants Puzzle Challenges (Summer 2021, Week 3, Problem 1) in Lean. ~ Yaël Dillies, Bhavik Mehta. #ITP #LeanProver #Math
- Ideas that created the future: Classic papers of Computer Science. ~ Harry R. Lewis. #eBook #CompSci
- Core Haskell tools. ~ Gil Mizrahi. #Haskell #FunctionalProgramming
- How Lisp became God’s own programming language. ~ @TwoBitHistory. #Lisp #Programming
- Natural deduction calculus for first-order logic. ~ Yazeed Alrubyli. #Logic #Math
- Assimilating the structure of formal and informal proof. ~ Kensho Tsurusaki, Akiko Aizawa. #ITP #LeanProver
- Balancing the formal and the informal in user-centred design. ~ JC Campos, MD Harrison, P Masci. #ITP #PVS
- Extracting functional programs from Coq, in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
- Formal methods for security knowledge area. ~ David Basin. #FormalMethods
- HaskellFL: A tool for detecting logical errors in Haskell. ~ Vanessa Vasconcelos, Mariza A. S. Bigonha. #Haskell #FunctionalProgramming
- Abstraction in Reflex and CodeWorld. ~ Chris Smith. #Haskell #CodeWorld #FunctionalProgramming
- That one cool reader trick. ~ Solomon. #Haskell #FunctionalProgramming
- Namespaced De Bruijn indices. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
- Deep Learning: A critical appraisal. ~ Gary Marcus. #DeepLearning
- A functional reboot for Deep Learning. ~ Conal Elliott. #DeepLearning #FunctionalProgramming #Haskell
- Symbolic and automatic differentiation of languages. ~ Conal Elliott. #Agda #FunctionalProgramming
- What is the point of Lean’s maths library? ~ Kevin Buzzard. #ITP #LeanProver #Math
- Counting cardinalities. ~ Mitchell Vitez. #Haskell #FunctionalProgramming
- Skipping the binder bureaucracy with mixed embeddings in a semantics course (Functional Pearl). ~ Adam Chlipala. #ITP #Coq
- The Hoare State Monad (Proof Pearl). ~ Wouter Swierstra. #ITP #Coq
- Competitive programming in Haskell: monoidal accumulation. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Formalization in Lean of IMO 2001 Q6. ~ Sara Díaz, Johan Commelin. #ITP #LeanProver #Math #IMO
- Reasoning about iteration and recursion uniformly based on big-step semantics. ~ Ximeng Li, Qianying Zhang, Guohui Wang, Zhiping Shi, Yong Guan. #ITP #Coq
- A secure and formally verified commodity multiprocessor hypervisor. ~ Shih-Wei Li. #PhD_Thesis #ITP #Coq
- Kronecker product of matrices (in Lean). ~ Filippo A. E. Nuccio, Eric Wieser. #ITP #LeanProver #Math
- Depth-first and breadth-first search in Haskell. ~ Malvin Gattinger. #Haskell #FunctionalProgramming
- Left and right folds (Comparison of a mathematical definition and a programmatic one). ~ Philip Schwarz. #Haskell #Scala #FunctionalProgramming
- Elementary recursive algorithms. ~ Yiannis N. Moschovakis. #Algorithms #Logic #Math #CompSci
- Extracting functional programs from Coq, in Coq. ~ Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters. #ITP #Coq
- A toy WASM symbolic interpreter. ~ Simon Marechal et als. #Haskell #FunctionalProgramming
- Relational forests (in Isabelle/HOL). ~ Walter Guttmann. #ITP #IsabelleHOL
- Theorem proving in classical logic. ~ David Davies. #Haskell #FunctionalProgramming #Logic
- Automatically generalizing theorems using typeclasses. ~ Alex J. Best. #ITP #LeanProver
- A brief intro to monad transformers. ~ Solomon. #Haskell #FunctionalProgramming
- Elements of differential geometry in Lean: A report for mathematicians. ~ Anthony Bordg, Nicolò Cavalleri. #ITP #LeanProver #Math
- Plotting in a formally verified way. ~ Guillaume Melquiond. #ITP #Coq
- Edukera: Teach Logic and Math with a proof assistant. #ITP #Coq #Edukera #Logic #Math
- Archetype, a DSL for Tezos. ~ Benoit Rognier. #ITP #Coq #Edukera #Archetype
- A logic theory pattern for linearized control systems. ~ Andrea Domenici, Cinzia Bernardeschi. #ITP #PVS
- Verifying time complexity of binary search using Dafny. ~ Shiri Morshtein, Ran Ettinger, Shmuel Tyszberowicz. #ATP #FormalVerification #Dafny
- Explaining counterexamples with giant-step assertion checking. ~ Benedikt Becker, Cláudio Belo Lourenço, Claude Marché. #ATP #Why3 #FormalVerification
- VeriFly: On-the-fly assertion checking with CiaoPP (extended abstract). ~ Miguel A. Sanchez-Ordaz, Isabel Garcia-Contreras, Víctor Pérez, Jose F. Morales, Pedro Lopez-Garcia, Manuel V. Hermenegildo./#EPTCS338.13 #Prolog #CiaoPP
- Haskell for the Elm enthusiast. ~ No Red Ink. #Haskell #Elm #FunctionalProgramming
- Haskell series part 2 (This is the second article of a series on the functional language Haskell for beginners). ~ Pierre Guillemot. #Haskell #FunctionalProgramming
- fromMaybe is Just a fold. ~ Dan Soucy. #Haskell #FunctionalProgramming
- When Howard Met Curry. ~ Rob Rix. #Haskell #FunctionalProgramming
- Axiomatic Minkowski spacetime in Isabelle/HOL. ~ Richard Schmoetten. #MSc_Thesis #ITP #IsabelleHOL
- Archive of Formal Proofs. #ITP #IsabelleHOL
- Archive of Formal Proofs redesign. ~ Carlin MacKenzie. #ITP #IsabelleHOL
- Lean proof of Thomaes (popcorn) function. ~ Ender Doe. #ITP #LeanProver #Math
- Proof and computation: Perspectives for mathematics, computer science, and philosophy. ~ Klaus Mainzer. #Logic #Math #CompSci #ITP
- Oblivious Algebraic Data Types. ~ Qianchuan Ye, Benjamin Delaware. #ITP #Coq
- GHC curiosities: Equality constraints in kinds. ~ Ryan Scott. #Haskell #FunctionalProgramming
- Egglog 2: Automatically proving the pullback of a monic is monic. ~ Philip Zucke. #CategoryTheory
- Writing academic papers with org-mode. ~ Wouter Spekkink. #Emacs #OrgMode
- Tying shoes with GADTs. ~ MorrowM. #Haskell #FunctionalProgramming