Resumen de lecturas compartidas durante julio de 2019
Esta entrada es una recopilación de lecturas compartidas, durante julio 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.
- Bar-Hillel theorem mechanization in Coq. ~ S. Bozhko, L. Khatbullina, S.Grigorev. #ITP #Coq
- Jupyter adaptation of “Learn you a Haskell for great good!” ~ James Brock. #Haskell #FunctionalProgramming #Jupyter
- Property-based testing. ~ J. Fowler. #PhD_Thesis #Haskell #FunctionalProgramming
- An introduction to computer science research: selected papers with commentary. ~ Camille Akmut. #CompSci
- Formal proof and analysis of an incremental cycle detection algorithm. ~ A. Guéneau, J.H. Jourdan, A. Charguéraud, F. Pottier. #ITP #Coq
- Formal verification of memory preservation of x86-64 binaries. ~ J.A. Bockenek, F. Verbeek, P. Lammich, B. Ravindran. #ITP #IsabelleHOL
- Monday Morning Haskell: Gloss review! ~ James Bowen. #Haskell #FunctionalProgramming
- Secure compilation. ~ C. Hritcu et als. #Programming
- The Ramanujan machine: Automatically generated conjectures on fundamental constants. ~ G. Raayoni et als. #MachineLearning #Math
- Proving tree algorithms for succinct data structures. ~ R. Affeldt, J. Garrigue, X. Qi, K. Tanaka. #ITP #Coq
- Formalizing the solution to the cap set problem. ~ S.R. Dahmen, J. Hölzl, R.Y. Lewis. #ITP #LeanProver
- Various new theorems in constructive univalent mathematics written in Agda. ~ Martin Escardo. #ITP #Agda #Math
- On solving word equations using SAT. ~ Joel D. Day et als. #ATP #SAT
- A story told by type errors. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- 10 days of neural networks in Haskell. Bogdan Penkovsky. #Haskell #FunctionalProgramming #NeuralNetworks
- A taste of type theory. ~ Bartosz Milewski. #TypeTheory #FunctionalProgramming
- Neural network verification for the masses (of AI graduates). ~ E. Komendantskaya et als. #AI #Verification #ITP #Coq #ATP #SMT #Z3 #NeuralNetworks
- Formalization of a monitoring algorithm for metric first-order temporal logic. ~ J. Schneider, D. Traytel. #ITP #IsabelleHOL #Logic
- Proving for Fun: July 2019. #ITP #IsabelleHOL #Coq
- Formalization of Rice’s theorem over a functional language model. ~ T.M.F. Ramos, A.A- Almeida, M. Ayala-Rincón. #ITP #PVS
- Improving Haskell. ~ M.A.T. Handley, G. Hutton. #Haskell #FunctionalProgramming
- Lightweight invertible enumerations in Haskell. ~ Brent Yorgey. #Haskell #FunctionalProgramming
- Coding with asymmetric numeral systems. ~ J. Gibbons. #Haskell #FunctionalProgramming
- Learn Haskell to be a better programmer. ~ Kwang Yul Seo. #Haskell #FunctionalProgramming
- Cutting through the smog: making an air quality bot with Haskell. ~ A. Moreno. #Haskell #FunctionalProgramming
- Microsmos: Writing a simple tree-editor with brick. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- Examples and results from a BSc-level course on domain specific languages of mathematics. ~ P. Jansson, S.H. Einarsdóttir, C. Ionescu. #Haskell #FunctionalProgramming #Math
- Generic diffing and merging of mutually recursive datatypes in Haskell. ~ A. van Putten. #Msc_Thesis #Haskell #FunctionalProgramming
- S Stands for Shock: The European funders’ proposal for Open Access. ~ Jeremy Gibbons.
- Abstraction and subsumption in modular verification of C programs. ~ A.W. Appel, L. Beringer. #ITP #Coq
- Separation-logic-based program verification in Coq. ~ Qinxiang Cao. #PhD_Thesis #ITP #Coq
- A computer-generated proof that nobody understands. ~ Kevin Buzzard. #ATP #Math
- Write you a Haskell (Building a modern functional compiler from first principles). ~ Stephen Diehl. #Haskell #FunctionalProgramming
- A continuation of Stephen Diehl’s “Write you a Haskell”. #Haskell #FunctionalProgramming
- Lemma discovery for induction: A survey. ~ Moa Johansson. #Haskell
- From LCF to Isabelle/HOL. ~ L.C. Paulson, T. Nipkow, M. Wenzel. #ITP #IsabelleHOL
- Domain-specific language to encode induction heuristics. ~ Yutaka Nagashima. #ITP #IsabelleHOL
- Preparing for simulation: Player AI. ~ James Bowen. #Haskell #FunctionalProgramming
- Scripting in Haskell and PureScript. ~ Riccardo Odone. #Haskell #PureScript
- A formal proof of the termination of Zielonka’s algorithm for solving parity games. ~ R. Abraham. #ITP #IsabelleHOL
- Mechanizing Principia Logico-Metaphysica in functional type theory. ~ D. Kirchner, C. Benzmüller, E.N. Zalta. #ITP #IsabelleHOL
- Dependently-typed Montague semantics in the proof assistant Agda-flat. ~ C. Zwanziger. #ITP #Agda
- I/O logic in HOL. ~ C. Benzmüller, A. Farjami, P. Meder, X. Parent. #ITP #IsabelleHOL
- SAT solvers and computer algebra systems: A powerful combination for mathematics. ~ C. Bright, I. Kotsireas, V. Ganesh. #SAT #CAS #Math
- Open Sum Types in Haskell with world-peace. ~ Dennis Gosnell (Dennis Gosnell). #Haskell #FunctionalProgramming
- Trees as monads. ~ Dimitrios Kalemis. #Haskell #FunctionalProgramming
- Lambda calculus. ~ Ben Lynn. #LambdaCalculus #Haskell #FunctionalProgramming
- REBA: A refinement-based architecture for knowledge representation and reasoning in robotics. ~ M. Sridharan, M. Gelfond, S. Zhang, J. Wyatt. #AI #KRR #ASP
- Dependency learning for QBF. ~ T. Peitl, F. Slivovsky, S. Szeider. #AI
- My first fifteen compilers. ~ Lindsey Kuper. #Programming #Compilers #Nanopass
- A verified compiler from Isabelle/HOL to CakeML. ~ L. Hupel, T. Nipkow. #ITP #Isabelle/HOL
- Multi stage programming in context. ~ M. Pickering, N. Wu, C. Kiss. #Haskell #FunctionalProgramming
- Working with source plugins. ~ M. Pickering, N. Wu, B. Németh. #Haskell #FunctionalProgramming
- Trustworthy graph algorithms. ~ M. Abdulaziz, K. Mehlhorn, T. Nipkow. #ITP #IsabelleHOL
- Certified semantics for miniKanren. ~ D. Rozplokhas, A. Vyatkin, D. Boulytchev. #ITP #Coq
- (Co) inductive proof systems for compositional proofs in reachability logic. ~ V. Rusu, D. Nowak. #ITP #IsabelleHOL #Coq
- Gradual typing from theory to practice. ~ Sam Tobin-Hochstadt. #Programming
- Walker: Automated assessment of Haskell code using syntax tree analysis. ~ R.H. de Vries. #Haskell #FunctionalProgramming
- BioShake: a Haskell EDSL for bioinformatics workflows. ~ J. Bedő. #Haskell #FunctionalProgramming
- Music as language (Putting probabilistic temporal graph grammars to good use). ~ O. Melkonian #Haskell #FunctionalProgramming #Music
- A bridge anchored on both sides: Formal deduction in introductory CS, and code proofs in discrete math. ~ D.G. Wonnacott, P.M. Osera. #Logic #Math #ITP #Coq #Haskell
- Experimental evaluation of formal software development using dependently typed languages. ~ F. Tamasi. #ITP #Coq #Agda
- Evaluation of function calls in Haskell. ~ Laszlo Treszkai. #Haskell #FunctionalProgramming
- Automatically and efficiently illustrating polynomial equalities in Agda. ~ Donnacha Oisín Kidney. #Bachelor_Thesis #ITP #Agda
- Building and debugging FRP with CodeWorld and Reflex. ~ Chris Smith. #Haskell #CodeWorld
- El zen de Python: Explicado y con ejemplos. ~ Javier Daza. #Programación #Python
- A brief analysis of “The zen of Python”. ~ Jonathan Hammond #Programming #Python
- Genetic algorithms as shrinkers in property-based testing. ~ F.Y. Lo, C.H. Chen, Y. Chen. #ITP #Coq
- Julia’s efficient algorithm for subtyping unions and covariant tuples. ~ B Chung, F. Zappa Nardelli, J. Vitek. #ITP #Coq #JuliaLang
- Closure conversion is safe for space. ~ Z. Paraskevopoulou, A.W. Appel. #ITP #Coq
- Advanced search with drilling! ~ James Bowen. #Haskell #FunctionalProgramming
- Writing a PhD thesis with Org Mode. ~ Daniel Gomez. #Emacs #Org_mode
- Writing a Ph.D. thesis with Org Mode (emplate repository). ~ Daniel Gomez. #Emacs #Org_mode
- ebib: A BibTeX database manager for Emacs. #Emacs #LaTeX
- Summer reading in theory. R.J. Lipton, K.W. Regan. #CompSci
- Revelations from repetition: Source code headers in Haskell and Python. ~ S. Carstens, M. Meschede. #Haskell #Python
- Una interesante introducción a la lógica difusa. ~ Carlos Bejines. #Lógica #Matemáticas
- A sequent calculus for first-order logic in Isabelle/HOL. ~ Andreas Halkjær From. #ITP #IsabelleHOL
- Formal verification of trading in financial markets. #ITP #Coq
- Decompose ContT. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming
- Dimensions and Haskell: Singletons in action. ~ R. Stryungis, D. Rogozin. #Haskell #FunctionalProgramming
- Elements of functional programming in Python. ~ Parul Pandey. #Python #FunctionalProgramming
- Hybrid relations in Isabelle/UTP. ~ S.D. Foster. #ITP #IsabelleHOL
- Formal verification of quantum algorithms using quantum Hoare logic. ~ J. Liu et als. #ITP #IsabelleHOL
- Towards a verified model of the Algorand consensus protocol in Coq. ~ M.A. Alturki, J. Chen, V. Luchangco, B. Moore. #ITP #Coq
- A certified functional nominal C-unification. ~ M. Ayala-Rincón et als. #ITP #PVS
- A predicate transformer semantics for effects (Functional pearl). ~ W. Swierstra, T. Baanen. #ITP #Agda
- Kind inference for datatypes. ~ N. Xie, R.A. Eisenberg, B.C.D.S. Oliveira. #Haskell #FunctionalProgramming
- Generic enumerators. ~ C. van der Rest, W. Swierstra, M. Chakravarty. #Haskell #FunctionalProgramming
- Haskell I/O tutorial. ~ Albert Y. C. Lai. #Haskell #FunctionalProgramming
- Mathematical proof of algorithm correctness and efficiency. ~ Vladimir Batoćanin. #CompSci #Algorithms
- A curious associativity of the <$> operator. ~ Roman Cheplyaka. #Haskell #FunctionalProgramming
- Analyzing our parameters. ~ James Bowen #Haskell #FunctionalProgramming
- Insane in the Membrain. ~ Veronika Romashkina. #Haskell #FunctionalProgramming
- Rediscovering constructive type theory with Cedille. ~ Aaron Stump. #Haskell #Cedille
- Making it easier to program and protect the Web. #CompSci
- “Programming Algorithms” Book. ~ Vsevolod Dyomkin. #Programming #Lisp #Algorithms
- How to use Binder and Python for reproducible research. ~ Erik Marsja. #Binder #Docker #Jupyter #Python
- Generating correctness proofs with neural networks. ~ A. Sanchez-Stern et als. #ITP #NeuralNetworks
- Towards a smart contract verification framework in Coq. ~ D. Annenkov, B. Spitters. #ITP #Coq
- Building a blog in Haskell with Yesod–using a database. ~ R. Odone. #Haskell #FunctionalProgramming
- Euclidean rhythms and Haskell. ~ Erich Grunewald. #Haskell #FunctionalProgramming
- A weekend replication of STOKE, a stochastic superoptimiser. #Haskell #FunctionalProgramming
- Haskell Dockerfile linter: A smarter Dockerfile linter that helps you build best practice Docker images. #Docker #Haskell #FunctionalProgramming
- In praise of strong FP. ~ Aaron Stump. #FunctionalProgramming
- Fast polynomial arithmetic in Haskell. #Haskell #FunctionalProgramming
- The AI metamorphosis. ~ Henry A. Kissinger, Eric Schmidt, Daniel Huttenlocher. #AI
- Langages des maths, langages de l’informatique. #Math #CompSi
- Decades-old computer science conjecture solved in two pages. ~ Erica Klarreich. #Math #CompSci
- Coq Coq Codet! (Towards a Verified Toolchain for Coq in MetaCoq). ~ M. Sozeau et als. #ITP #Coq
- Formalization of the MRDP theorem in the Mizar system. ~ K. Pąk. #ITP #Mizar #Math
- Partial correctness of a factorial algorithm. ~ A. Jaszczak, A. Korniłowicz. #ITP #Mizar
- Natural addition of ordinals. ~ S. Koch. #ITP #Mizar #Math
- Modular effects in Haskell through effect polymorphism and explicit dictionary applications. ~ D. Devriese. #Haskell #FunctionalProgramming
- idris-ct: A library to do category theory in Idris. ~ F. Genovese et als.. #Idris #CategoryTheory
- Szpilrajn extension theorem in Isabelle/HOL. ~ P. Zeller. #ITP #IsabelleHOL #Math
- Fibonacci formalized 1: some sums. ~ Bryan Gin-ge Chen. #ITP #LeanProver #Math
- Generating castles for Minecraft using Haskell. ~ Tim Philip Williams. #Haskell #FunctionalProgramming
- Cursors, part 6: The forest cursor. ~ Tom Sydney Kerckhove. #Haskell #FunctionalProgramming
- Testing bipartiteness with monad transformers. ~ Vasily Alferov. #Haskell #FunctionalProgramming
- Solving a puzzle in Haskell. ~ Chris Smith. #Haskell #FunctionalProgramming #CodeWorld
- The power of RecordWildCards. ~ Dmitrii Kovanikov. #Haskell #FunctionalProgramming
- Programming algorithms: A crash course in Lisp. ~ Vsevolod Dyomkin. #CommonLisp
- Formalizing extended UTxO and BitML calculus in Agda. ~ O Melkonian. #ITP #Agda
- Extensional higher-order paramodulation in Leo-III. ~ A. Steen, C. Benzmüller. #ITP #Leo_III
- Functional programming in Scala. ~ P. Chiusano, R. Bjarnason. #eBook #FunctionalProgramming #Scala
- Attack trees in Isabelle. ~ F. Kammüller. #ITP #IsabelleHOL
- Introducing the Haskell Phrasebook. ~ Chris Martin. #Haskell #FunctionalProgramming
- The Haskell Phrasebook. ~ Chris Martin, Julie Moronuki. #Haskell #FunctionalProgramming
- Arithmetic on algebraic data types. ~ Boro Sitnikovski. #Haskell #FunctionalProgramming #Math
- Julia: come for the syntax, stay for the speed. ~ J.M. Perkel. #Programming #JuliaLang
- Les algorithmes du nouveau lycée technologique, en Python. ~ Alain Busser. #Programming #Python