Jose_A_Alonso, 18 days ago to random

Guided equality saturation. ~ Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer. https://michel.steuwer.info/files/publications/2024/POPL-2024-2.pdf #ITP #Lean4

Jose_A_Alonso, 21 days ago to ai

Learning guided automated reasoning: A brief survey. ~ Lasse Blaauwbroek, David Cerna, Thibault Gauthier, Jan Jakubův, Cezary Kaliszyk, Martin Suda, Josef Urban. https://arxiv.org/abs/2403.04017 #ATP #ITP #AI #MachineLearning

Jose_A_Alonso, 1 month ago to math

A comprehensive overview of the Lebesgue differentiation theorem in Coq. ~ Reynald Affeldt, Zachary Stone. https://arxiv.org/abs/2403.18229 #ITP #Coq #Math

adbrucker, 2 months ago to golang

We have an exciting opportunity for PhD study with myself and Prof. Burkhart Wolff form the Université Paris-Saclay on developing a formal semantics for Go (lang) in Isabelle/HOL. This new 'double PhD' programme leading to a PhD award from both universities.
More information and application details at: https://www.exeter.ac.uk/study/pg-research/funding/phdfunding/paris-saclay/ and https://adum.fr/as/ed/voirproposition.pl?site=adumR&matricule_prop=53822#version (application deadline: 31st of March 2024). Please contact me for more details.
#Isabelle #PhD #FediHire #Golang #Verification #ITP #Semantics

Jose_A_Alonso, 4 months ago to random

The functional essence of imperative binary search trees. ~ Anton Lorenzen, Daan Leijen, Wouter Swierstra & Sam Lindley. https://www.microsoft.com/en-us/research/uploads/prod/2023/07/fiptree-tr-v4.pdf #ITP #Coq

Jose_A_Alonso, 4 months ago to math

Formalisation of combinatorics. ~ Bhavik Mehta. https://youtu.be/_lBFks9lI2k #ITP #LeanProver #Math

Jose_A_Alonso, 4 months ago to FunctionalProgramming

Polynomial functors in Agda: Theory and Practice (A formalization and collection of applications of categories of polynomial functors). ~ André Muricy Santos Marcus Jörgensson. https://odr.chalmers.se/server/api/core/bitstreams/774ba4a2-58b4-407f-aa6b-b0209b6c7d70/content #ITP #Agda #FunctionalProgramming

Jose_A_Alonso, 4 months ago to math

A computer-checked proof of the Four Color Theorem. ~ Georges Gonthier. https://bit.ly/4aK0e6O #ITP #Coq #Math

Jose_A_Alonso, 5 months ago to random

Folding left and right matters: Direct style, accumulators, and continuations. ~ Olivier Danvy. https://bit.ly/41oDc1f #ITP #Coq

Jose_A_Alonso, 5 months ago to math

'A-team' of math proves a critical link between addition and sets. ~ Leila Sloman. https://www.quantamagazine.org/a-team-of-math-proves-a-critical-link-between-addition-and-sets-20231206/ #ITP #LeanProver #Math

Jose_A_Alonso, 6 months ago to math Spanish

#Calculemus: Demostraciones con Lean4: "Si a divide a b y a c, entonces divide a b+c". https://www.glc.us.es/~jalonso/calculemus/07-nov-23/ #ITP #LeanProver #Lean4 #Math

Jose_A_Alonso, 7 months ago to random

Lean FRO: Monthly Community Meeting Oct 13, 2023. https://youtu.be/jaibFnoMDSw #ITP #LeanProver

Jose_A_Alonso, 7 months ago to random

Martin-Löf à la Coq. ~ Arthur Adjedj et als. https://arxiv.org/abs/2310.06376 #ITP #Coq

Jose_A_Alonso, 7 months ago to philosophy

The concept of proof within the context of machine mathematics. ~ Lawrence C. Paulson (@lawrpaulson). https://lawrencecpaulson.github.io/2023/10/04/Ochigame.html #Philosophy #Math #ITP

Jose_A_Alonso, 7 months ago to Logic

Modal type theories. ~ Michael Shulman. https://itp-school-2023.github.io/slides/slides_shulman.pdf #ITP #Agda #Logic

rml, 8 months ago to random

A proof checker for Axiomatic Language
http://www.axiomaticlanguage.org/proof_checker.htm

#scheme #itp

Jose_A_Alonso, 8 months ago to math

Lean on Goldbach's conjecture. ~ Frank Vega. https://easychair.org/publications/preprint_download/MBd4 #ITP #LeanProver #Math

Jose_A_Alonso, 8 months ago to random

Loogle: a search tool for Lean/Mathlib. https://loogle.lean-fro.org #ITP #LeanProver #Mathlib

RanaldClouston, 9 months ago to Cambridge

I'm enjoying the #Pittsposium in #Cambridge , a workshop in honour of my PhD supervisor Andy Pitts. Loved this talk by Larry Paulson, who advocated for mathematicians to use proof assistants with liberal use of sorry / admitted for parts of proofs they are confident in to avoid burning time on small details, for example the many lines of code required when verifying one sentence proofs in a standard textbook. #ITP

Jose_A_Alonso, 9 months ago to random

Using ACL2 to teach students about software testing. ~ Ruben Gamboa, Alicia Thoney. https://cgi.cse.unsw.edu.au/~eptcs/paper.cgi?ACL22022.4.pdf #ITP #ACL2

Jose_A_Alonso, 10 months ago to random

Courses using Lean. https://leanprover-community.github.io/courses.html #ITP #LeanProver

Jose_A_Alonso, 11 months ago to random

An interactive SMT tactic in Coq using abductive reasoning. ~ Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark Barrett. https://easychair.org/publications/open/lNvq #ITP #Coq #SMT