Las lecturas compartidas en Mastodon el 24 de julio de 2024 son

• Lecturas compartidas el 23 de julio de 2024. #ITP #Lean4 #Math #FunctionalProgramming #OCaml
• Lean For Haskell developers. ~ Solomon. #ITP #Lean4 #FunctionalProgramming #Haskell
• A logic for veracity: Development and implementation. ~ Daniel Britten, Steve Reeves. #ITP #Coq #Logic
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue, Takafumi Saikawa. #ITP #Coq

Las lecturas compartidas en Mastodon el 23 de julio de 2024 son

• Lecturas compartidas el 22 de julio de 2024. #AI
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean. ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean (Code). ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• (Pro)Seminar on computer-assisted mathematics. ~ Judith Ludwig, Florent Schaffhauser. #CAS #Sage #ITP #LeanProver #Math
• Practical deductive verification of OCaml programs (Extended version). ~ Mário Pereira. #FunctionalProgramming #OCaml

Las lecturas compartidas en Mastodon el 22 de julio de 2024 son

• Lecturas compartidas el 21 de julio de 2024. #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell
• Un robot que resuelve rompecabezas 200 veces más rápido que las personas más hábiles. ~ @Alvy. #AI

Las lecturas compartidas en Mastodon el 21 de julio de 2024 son

• Lecturas compartidas el 20 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Logic #CompSci
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• A tree rewriting system for the Reflection Calculus. ~ Sofía Santiago-Fernández, Joost J. Joosten, David Fernández-Duque. #ITP #Coq #Logic
• Automated proof tactics for model transformation. ~ Julien Cohen, Massimo Tisi, Remi Douence. #ITP #Coq
• Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. #FunctionalProgramming #Haskell #LiquidHaskell
• Monumental proof settles geometric Langlands conjecture. ~ Erica Klarreich (@EricaKlarreich). #Math

Las lecturas compartidas en Mastodon el 20 de julio de 2024 son

• Lecturas compartidas el 19 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin, Zhiqing Sun, Yiming Yang, Sean Welleck. #ITP #Lean4 #LLMs
• PutnamBench: Evaluating neural theorem-provers on the Putnam mathematical competition. ~ George Tsoukalas et als. #LLMs #ITP #Lean4 #IsabelleHOL #Coq
• Haskelite: A tracing interpreter based on a pattern-matching calculus. ~ Pedro Vasconcelos, Rodrigo Marques. #FunctionalProgramming #Haskell
• Higher-order specifications for deductive synthesis of programs with pointers. ~ David Young et als. #FunctionalProgramming #Pika
• The significance of symbolic logic for scientific education. ~ André Platzer. #Logic #CompSci

Las lecturas compartidas en Mastodon el 19 de julio de 2024 son

• Lecturas compartidas el 18 de julio de 2024. #ITP #Coq #IsabelleHOL #FunctionalProgramming #Haskell #LiquidHaskell #AI #ChatGPT #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "El punto de acumulación de las sucesiones convergente es su límite". #ITP #Lean4 #IsabelleHOL #Math
• Categorical foundations of formalized condensed mathematics. ~ Dagur Asgeirsson et als. #ITP #Lean4 #Math
• Haskell for dilettantes, Part 1: Intro. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 2: Expressions, types, and functions. ~ Tea Leaves. #FunctionalProgramming #Haskell
• Haskell for dilettantes, Part 3a: Homework 1, Exercise 1. ~ Tea Leaves. #FunctionalProgramming #Haskell

Las lecturas compartidas en Mastodon el 18 de julio de 2024 son

• Lecturas compartidas el 16 de julio de 2024. #ITP #Lean4 #Coq #LLMs #Programming #Emacs
• Functional Pearl: Short and mechanized logical relation for dependent type theories. ~ Yiyun Liu, Stephanie Weirich. #ITP #Coq
• HHLPar: Automated theorem prover for parallel hybrid communicating sequential processes. ~ Xiangyu Jin, Bohua Zhan, Shuling Wang, Naijun Zhan. #ITP #IsabelleHOL
• Molly: A verified compiler for cryptographic roles. ~ Daniel J. Dougherty, Joshua D. Guttman. #ITP #Coq
• Formalizing operads for a categorical framework of DSL composition. ~ Zachary Flores, Angelo Taranto, Yakir Forman, Eric Bond. #ITP #Coq
• Modular implementation and formalization of dynamic policies (Work in progress). ~ Antonio Zegarelli, Niki Vazou, Marco Guarnieri. #FunctionalProgramming #LiquidHaskell
• Demystifying Artificial Intelligence (Symbolic, data-driven, statistical and ethical AI). ~ Emmanuel Gillain (ed.). #eBook #AI
• Using ChatGPT as a proof assistant in a mathematics pathways course. ~ Hyejin Park, Eric D. Manley. #ChatGPT #Math #Reasoning
• The Haskell Unfolder Episode 29: Exceptions, annotations and backtraces. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming

Las lecturas compartidas en Mastodon el 16 de julio de 2024 son

• Lecturas compartidas el 15 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #CompSci #Haskell #Prolog
• A term-patching framework for eliminating definitional equalities in Lean (Work-in-progress). ~ Rishikesh Vaishnav. #ITP #Lean4
• Guided proof search using large language models and lemma extraction in Coq. ~ Tarun Prasad. #ITP #Coq #LLMs
• Code completion with Google Gemini for Emacsen. ~ Hitoshi Uchida. #Programming #Emacs #Gemini

Las lecturas compartidas en Mastodon el 15 de julio de 2024 son

• Lecturas compartidas el 14 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #Haskell #Prolog
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las subsucesiones tienen el mismo límite que la sucesión". #ITP #Lean4 #IsabelleHOL #Math
• Formalizing implicational axiomatics for classical first-order logic with functions in Isabelle/HOL. ~ Jørgen Villadsen, Roberto Pettinau. #ITP #IsabelleHOL #Logic
• Mathematics in programming. ~ Xinyu Liu #Math #CompSci #Haskell
• Smart investment problem with Prolog. ~ Matteo Redaelli (@matteoredaelli). #Prolog

Las lecturas compartidas en Mastodon el 14 de julio de 2024 son

• Lecturas compartidas el 13 de julio de 2024. #ITP #Lean4 #Coq #Abella #Agda #Mizar #Logic #Math #IMO #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]". #ITP #Lean4 #IsabelleHOL #Math
• Implementing the Fatio protocol for multi-agent argumentation in LogiKEy. ~ Luca Pasetto, Christoph Benzmüller. #Logic #ITP #IsabelleHOL
• Implementing intermediate logics. ~ Bastiaan Haaksema, Jens Otten, Revantha Ramanayake. #ATP #Logic #Haskell #Prolog