Resumen de lecturas compartidas durante julio de 2018
Esta entrada es una recopilación de lecturas compartidas, durante julio de 2018, en Twitter sobre programación funcional y demostración asistida por ordenador fundamentalmente.
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.
- Computational reverse mathematics and foundational analysis. ~ Benedict Eastaugh #Logic #Math
- GLC: Resumen de lecturas compartidas (octubre de 2017).
- GLC: Resumen de lecturas compartidas (noviembre de 2017).
- GLC: Resumen de lecturas compartidas (diciembre de 2017).
- GLC: Resumen de lecturas compartidas (enero de 2018).
- GLC: Resumen de lecturas compartidas (febrero de 2018).
- IsaK: A complete semantics of K. ~ L. Li, E.L. Gunter #ITP #IsabelleHOL #Logic
- A real-world application with a comonadic user interface. ~ Arthur Xavier #FunctionalProgramming #Haskell #PureScript
- Google Sheets and Haskell. ~ Laurence Emms #Haskell
- Zamansky 50: Presentations. #Emacs
- GLC: Resumen de lecturas compartidas durante marzo de 2018.
- GLC: Resumen de lecturas compartidas durante abril de 2018.
- GLC: Resumen de lecturas compartidas durante mayo de 2018.
- GLC: Resumen de lecturas compartidas durante junio de 2018.
- GLC: Resumen de lecturas compartidas durante el curso 2017-18.
- Compiling an Haskell EDSL to C (A new C back-end for the Copilot runtime verification framework). ~ Frank Dedden Haskell
- Implementing analytic tableaux for justification logic. ~ N. Steenbergen #Haskell #Logic
- judge: Tableau-based theorem prover for justification logic. ~ N. Steenbergen #Haskell #Logic
- Redis data modeling with rank 2 types. #Haskell
- El problema del cambio de moneda. R. Ibáñez #Matemáticas
- A brief history of AI (An outline of what happened in the last 60 years in AI). ~ Francesco Corea #AI
- The machine that builds itself: how the strengths of Lisp family languages facilitate building complex and flexible bioinformatic models. ~ B.B. Khomtchouk, E. Weitz, C. Wahlestedt #Lisp
- Computational reverse mathematics and foundational analysis. ~ B. Eastaugh #Logic #Math
- Toward a more expressive pattern matching in Haskell. ~ G. Servadei #Haskell
- The 11th conference of PhD students in Computer Science (Volume of short papers).
- Scope of Artificial Intelligence in Law. ~ J. Dabass, B.S. Dabass #AI #MachineLearning #DeepLearning
- PVS embeddings of propositional and quantified modal logic. ~ J. Rushby #ITP #PVS #Logic
- Para qué le sirve a un investigador científico estar en Twitter. ~ Francisco R. Villatoro (#Ciencia
- How the scientific community reacts to newly submitted preprints: article downloads, Twitter mentions, and citations. ~ X. Shuai, A. Pepe, J. Bollen #Science
- Papers on programming languages: ideas from 70’s for today. ~ Mikhail Barash #Programming
- Why I love Haskell. ~ @PLT_cheater #Haskell
- A formalisation of nominal α-equivalence with A, C, and AC function symbols. ~ M. Ayala et als. #ITP #Coq
- A purely functional computer algebra system embedded in Haskell. ~ Hiromi Ishii #Haskell #CAS #Math
- Computational algebra system in Haskell (Dependently-typed computational algebra system written in Haskell). ~ Hiromi Ishii #Haskell #CAS #Math
- Benchmarks on various Fibonacci computation. ~ Hiromi Ishii #Haskell #Algorithms #Math
- Simple proof assistant for LK calculus (First-Order logic). ~ Hiromi Ishii #Haskell #Logic
- Probability 5 ways. ~ Donnacha Oisín Kidney #Haskell
- Formalization in constructive type theory of the standardization theorem for the lambda calculus using multiple substitution. ~ M. Copes, N. Szasz, A. Tasistro #ITP #Agda
- Matemática misteriosa. ~ Juan Arias de Reyna #Matemáticas
- Sharing a library between proof assistants: reaching out to the HOL family. ~ F. Thiré #ITP #OpenTheory # Coq #Matita
- Theory exploration in Hipster (or how to automate an undergraduate AI&CS student). ~ Moa Johansson #IsabelleHOL #Haskell
- From algebra to abstract machine. ~ W. Swierstra, C. Tomé Cortiñas #Haskell
- Specifications in small and large contexts. ~ N. Botta [Slides] #Idris
- Kuifje: Quantified information flow with monads in Haskell. ~ Tom Schrijvers #Haskell
- Static analysis of free monads. #Haskell
- Compiling quantamorphisms for the IBM Q-Experience. ~ J.N. Oliveira, A. Neri, R.S. Barbosa #Haskell
- Examples and results from a BSc-level course on domain specific languages of mathematics. ~ P. Jansson et als. #Haskell #Math
- Michael John Caldwell Gordon (FRS 1994), 28 February 1948 – 22 August 2017. ~ Lawrence C Paulson #ITP #Biography
- Differentiable functional programming. ~ Noel Welsh #DeepLearning #FunctionalProgramming #Scala
- A thought experiment: category theory and quantum computing. ~ Laurence Emms #Haskell #CategoryTheory #QuantumComputing
- Alan Turing, el genio que descodificó la naturaleza. ~ Núria Jar #Turing #Biografía #Computación vía @lavanguardia
- Inside the paper: Build systems à la carte. ~ Neil Mitchell #Haskell
- Deriving instances with a twist. ~ Xia Li-yao #Haskell
- A constructive formalisation of the modular strong normalisation theorem. ~ FLC de Moura et als. #ITP #Coq
- Using SMT engine to generate symbolic automata. ~ X. Qin et als. #SMT
- Von-Neumann-Morgenstern utility theorem in Isabelle/HOL. ~ J. Parsert, C. Kaliszyk #ITP #IsabelleHOL
- Weakening the requirements of a group. ~ J.D. Cook #Math
- A survey of knowledge representation and retrieval for learning in service robotics. ~ D. Paulius, Y. Sun #KRR
- Scaling-up reasoning and advanced analytics on BigData. ~ T. Condie et als. #LogicProgramming #BigData
- Type is an extensible GADT. ~ Xia Li-yao #Haskell
- Otro millón de dólares te espera: ¿Es P = NP? ~ Alfonso J. Población #Matemáticas #Computación
- Towards certified meta-programming with typed template-Coq. ~ A. Anand et als. #ITP #Coq
- Relating idioms, arrows and monads from monoidal adjunctions. ~ E. Rivas #Haskell
- Backward induction for repeated games. ~ J. Hedges #FunctionalProgramming #Haskell
- Everybody’s got to be somewhere. ~ C. McBride #Agda
- Daily coding puzzles. ~ Ali Spittel #CodingPuzzle
- The coinductive formulation of common knowledge. ~ C. Baston, V. Capretta #ITP #Coq #Agda
- La nacionalización de la estrategia en torno a la inteligencia artificial. (Estado, política y futuro). ~ Juan Luis Suárez #IA
- Fast Sudoku solver in Haskell #2: A 200x faster solution. ~ Abhinav Sarkar #Haskell
- Funflow example: emulating make. ~ Divesh Otwani, Nicholas Clarke #Haskell
- Categories for (Big) Data models and optimization. ~ L. Thiry, H. Zhao, M. Hassenforder #BigData #CategoryTheory #FunctionalProgramming #Haskell
- Verified analysis of random binary tree structures. ~ M. Eberl, M.W. Haslbeck, T. Nipkow #ITP #IsabelleHOL
- A formally verified cryptographic extension to a RISC-V processor. ~ J.R. Kiniry et als. #FormalVerification
- Artificial Intelligence. ~ Selmer Bringsjord #AI
- Reification by parametricity (Fast setup for proof by reflection, in two lines of Ltac). ~ J. Gross, A. Erbsen, A. Chlipala #ITP #Coq
- Mtac2: Typed tactics for backward reasoning in Coq. ~ J. Kaiser et als. #ITP #Coq
- A verified automatic prover based on ordered resolution. ~ A. Schlichtkrull, J.C .Blanchette, D. Traytel #ITP #IsabelleHOL #SML #Logic
- A formal proof in Coq of a control function for the inverted pendulum. ~ D. Rouhling #ITP #Coq
- Verifying the LTL to Büchi automata translation via very weak alternating automata. ~ S. Jantsch, M. Norrish #ITP #HOL4
- Eliminating unstable tests in floating-point programs. ~ L. Titolo, C. Muñoz, M.A. Feliú, M.M. Moscato #ITP #PVS
- Reo2PVS: Formal specification and verification of component connectors. ~ M.S. Nawaz, M. Sun #ITP #PVS
- Differential program semantics. ~ T. Girka #ITP #Coq
- Lisp and Haskell. ~ Mark Karpov #Lisp #Haskell
- Type-safe observable sharing in Haskell. ~ Andy Gill #Haskell
- Algorithms have been around for 4,000 years. ~ Herbert Bruderer #Algorithms
- Fast machine words in Isabelle/HOL. ~ A. Lochbihler #ITP #IsabelleHOL
- Compositional soundness proofs of abstract interpreters. ~ S. Keidel, C.B. Poulsen, S. Erdweg #Haskell
- Relational parametricity and quotient preservation for modular (co)datatypes. ~ A. Lochbihler, J. Schneider #ITP #IsabelleHOL
- First steps towards a formalization of Forcing. ~ E. Gunther, M. Pagano, P. Sánchez #ITP #Isabelle #Logic
- AI reasoning systems: PAC and applied methods. ~ J. Cheng #AI #Logic
- Taming the C monster (Haskell FFI techniques). #Haskell
- Competitive proving for fun. ~ M.P.L Haslbeck, S. Wimmer #ITP #IsabelleHOL
- Computational artifacts: Towards a philosophy of computer science. ~ R. Turner #CompSci
- A formally verified solver for homogeneous linear diophantine equations. ~ F. Meßner et als. #ITP #IsabelleHOL
- Probabilistic functional programming. ~ Donnacha Oisín Kidney #FunctionalProgramming #Haskell
- The consistency of arithmetic. ~ T.Y. Chow #Logic
- SAT encodings for sorting networks, single-exception sorting networks and ε−halvers. ~ J.A.R. Fonollosa #Logic #SAT
- SMCDEL: An implementation of symbolic model checking for dynamic epistemic logic with binary decision diagrams. ~ M. Gattinger #Logic #Haskell
- Type theory. ~ Thierry Coquand #Logic
- Formalizing implicative algebras in Coq. ~ É. Miquey #ITP #Coq
- Building an initial Emacs configuration. #Emacs
- Generic deriving of generic traversals. ~ C. Kiss, M. Pickering, N. Wu #FunctionalProgramming #Haskell
- CodeWorld update — July 14, 2018. ~ Chris Smith #Haskell #CodeWorld
- Teaching algebraic expressions with tracking arithmetic. ~ Chris Smith #Teaching #Math #Haskell #CodeWorld
- Mathematics and computation. ~ A. Bonato #Math #CompSci
- Test automáticos con QuickCheck ¿Cómo analizar nuestro código en busca de bugs?. ~ @__josejuan__ #Programación #QuickCheck
- Functor, Applicative and why. ~ Leo Zhang #FunctionalProgramming #Haskell
- The rise of mixed precision arithmetic. ~ Nick Higham #Programming
- The limits of classical and quantum computing. ~ Scott Aaronson #CompSci
- Intuitive mathematics. ~ Marianne Freiberger #Logic #Math
- Paradise lost and rescued. ~ Marianne Freiberger #Logic #Math
- Mathematics and computation. ~ Anthony Bonato #Math #CompSci
- Boosting the reuse of formal specifications. ~ M.M. Moscato et als. #ITP #PVS
- Closing the gap between correctness and efficiency. ~ G. Hutton #FunctionalProgramming #Haskell
- Towards formal modeling and verification of probabilistic connectors in Coq. ~ X. Zhang, M. Sun #ITP #Coq
- Pricing in discrete financial models. ~ M. Echenim #ITP #IsabelleHOL
- Towards a verified Smith normal form algorithm in Isabelle/HOL. ~ J. Divasón, J. Aransay #ITP #IsabelleHOL #Math
- A bridge too far: E.W. Dijkstra and logic. ~ Maarten van Emden #Logic #CompSci
- A practical introduction to finger trees. ~ Chris Penner #Haskell
- Exercitium: Tren de potencias. #Haskell
- A systematic approach for developing cyber physical systems. ~ X. He, Z. Dong, Y. Fu #ITP #Coq
- Dependent typing and existential (de)serialization. #Haskell
- WebGL, Fragment Shader, GHCJS and reflex-dom. ~ Joachim Breitner #Haskell
- Haskell & AppVeyor Chocolatey introduction. ~ Tamar Christina #Haskell
- ~ Chris Penner #Haskell
- Popularity of Haskell extensions. ~ Anish Tondwalkar #Haskell
- Mathematical reasoning. Writing and proof. ~ Ted Sundstrom #eBook #Math
- Supercompilation: ideas and methods. ~ I. Klyuchnikov, D. Krustev #Haskell
- Exercitium: Número medio. #Haskell
- The remote monad. ~ Justin Dawson #PhD_Thesis #Haskell
- A simple semi-automated proof assistant for first-order modal logics. ~ T. Libal #Logic #ATP #Prolog
- Implementations of natural logics. ~ Lawrence S. Moss #Logic #AutomatedReasoning
- Some thoughts about FOL-translations in Vampire. ~ Giles Reger #AutomatedReasoning #Vampir
- Using the Isabelle Ontology Framework (Linking the formal with the informal). ~ A.D. Brucker et als. #ITP #Isabelle
- Formal reasoning about the security of AWS (Amazon Web Services). ~ Byron Cook #AutomatedReasoning
- Into the infinite-theory exploration for coinduction. ~ S.H. Einarsdóttir, M. Johansson, J.Å. Pohjola #IsabelleHOL
- Interdisciplinary programming language design. ~ Michael Coblenz et als. #Programming
- Constructive Galois connections. ~ D. Darais, D. van Horn #ITP #Agda #Math
- Learning heuristics for automated reasoning through deep reinforcement learning. ~ G. Lederman et als. #MachineLearnig #AutomatedReasoning
- Towards neural theorem proving at scale. ~ P. Minervini et als. #AutomatedReasoning #MachineLearning
- Teaching programming languages. ~ Michael Hicks #Programming #Teaching
- Reference comparing R, Python, and MATLAB syntax. #Python #Rstats #MatLAB
- Using apt-get commands in Linux (complete beginners guide). ~ A. Prakash #Linux
- CoqTL: an internal DSL for model transformation in Coq. ~ M. Tisi, Z. Cheng #ITP #Coq
- Regular language representations in the constructive type theory of Coq. ~ C. Doczkal, G. Smolka #ITP #Coq
- Quadratic reciprocity and (p^2-1)/8. ~ The Xena Project #ITP #Lean #Math
- Automating verification of state machines with reactive designs and Isabelle/UTP. ~ S. Foster et als. #ITP #IsabelleHOL
- DAOconCoq: Demostración Asistida por Ordenador con Coq. #DAO #Coq
- DAOconCoq: Programación funcional y métodos elementales de demostración en Coq. #DAO #Coq
- Patience in K-8 Computer Science. ~ Chris Smith #Teaching #Programming #CodeWorld
- Formally verified Montgomery multiplication. ~ C. Walther #ITP #VeriFun #Math
- Teoría de categorías y programación funcional. ~ Diego Pedraza #Haskell #Matemáticas
- Why purely functional programming is a great idea with a misleading name. ~ Tikhon Jelvis #FunctionalProgramming
- Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. ~ M. Echenim, H. Guiol, N. Peltier #ITP #IsabelleHOL
- Declarative GUIs: simple, consistent, and verified. ~ S. Adelsberger, A. Setzer, E. Walkingshaw #Agda
- Bindings are functors. ~ J.C. Blanchette, L. Gheri, A. Popescu, D. Traytel #ITP #IsabelleHOL
- Novices and motivation when learning to code. ~ Chris Smith #Teaching #CodeWorld
- Gamifying propositional logic: QED, an interactive textbook. ~ Terence Tao #Teaching #Logic
- QED: a short interactive text in propositional logic arranged in the format of a computer game. ~ Terence Tao #Teaching #Logic
- Une histoire de la logique mathématique (de la philosophie à l’informatique). ~ Christian Retoré #Logic
- Course: Data structures and functional programming. ~ Michael Clarkson #FunctionalProgramming #OCaml #ITP #Coq
- Formal reasoning in Coq: a beginner’s guide. ~ Ray Wang #ITP #Coq
- Coq cheatsheet. ~ Eddie Kohler #ITP #Coq
- Python the future of programming? ~ Mike James #Programming #Python
- GHCinception: Running GHCi in GHCi. ~ Michael Sloan #Haskell
- Un error informático envía información confidencial a 1.500 criminales. #Programación
- List of software bugs. ~ Wikipedia #Programming
- Company-coq: A collection of extensions for Proof General’s Coq mode. #Emacs #Coq
- Bridging the gap between programming languages and hardware weak memory models. ~ A. Podkopaev, O. Lahav, V. Vafeiadis #ITP #Coq
- Haskell for JavaScript developers. ~ Anthony N Cipriano #Haskell #JavaScript
- HAMTs (Hash Array Mapped Tries) from scratch. ~ Vaibhav Sagar #Haskell
- Constructivism: An expert’s view. ~ Harvey Friedman #Logic #Math
- Computational logic: artificial intelligence in mathematical reasoning. ~ S. Graham-Lengrand and R. Blanco #Course #Logic #FunctionalProgramming #OCaml #ITP #Coq
- Verifying programs and proofs (Part I. describe algorithms). ~ Yves Bertot #ITP #Coq
- Coq Winter School 2018. ~ Yves Bertot #Course #ITP #Coq
- “The art of computer programming” by Donald Knuth. ~ Carl Tashian #Programming
- DAOconCoq T2: Demostraciones por inducción sobre los números naturales en Coq. #ITP #Coq
- Beyond polynomials and Peano arithmetic: automation of elementary and ordinal interpretations. ~ H. Zankl, S. Winkler, A. Middeldorp #Logic #Math #ATP
- Copying vs. sharing in functional languages. ~ Dan Ghica #FunctionalProgramming
- Verified AVL trees in Haskell and Agda. ~ Donnacha Oisín Kidney #Haskell #Agda
- Haskell: If monads are the solution, what is the problem? ~ Dan Ghica #FunctionalProgramming #Haskell
- Free Monoid from Free Algebra, Part 1: Free Algebras. ~ Bartosz Milewski #Haskell #CategoryTheory
- Free Monoid from Free Algebra, Part 2: Free Monoids. ~ Bartosz Milewski #Haskell #CategoryTheory
- Grain: a strongly-typed functional programming language built for the modern web. #FunctionalProgramming
- Learning Elm in 2018: comprehensive list of resources. #FunctionalProgramming #Elm
Una recopilación de las anteriores lecturas se encuentra en GitHub.