#proofassistant — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #proofassistant, aggregated by home.social.
-
New blog post: Introduction to Coinduction in Agda Part 1: Coinductive Programming
jesper.cx/posts/coinduction-part-1.html
#Agda #ProofAssistant #DependentTypes #Coinduction -
Functional Data Structures and Algorithms: a Proof Assistant Approach
#HackerNews #FunctionalDataStructures #Algorithms #ProofAssistant #Programming #HN
-
🤓 Ah yes, the riveting saga of "normal-order syntax-rules" and the elusive call/cc fix-point, where syntax rules magically transform into a proof assistant. 🧙♂️ Because what better way to celebrate Daniel P. Friedman than with a marathon of indecipherable jargon and fewer common examples no one asked for. 🎉
https://okmij.org/ftp/Scheme/callcc-calc-page.html #normalordersyntax #syntaxrules #callcc #proofassistant #DanielPFriedman #programmingjargon #HackerNews #ngated -
Readings shared July 31, 2025. https://jaalonso.github.io/vestigium/posts/2025/08/01-readings_shared_08-01-25 FunctionalProgramming #Haskell #LeanProver #Math #ProofAssistant
-
The math is haunted. ~ Dan Abramov. https://overreacted.io/the-math-is-haunted/ #ProofAssistant #LeanProver #Math
-
Universal pairs for diophantine equations (in Isabelle/HOL). ~ Marco David et als. https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html #ITP #ProofAssistant #IsabelleHOL #Math
-
Harmonic's IMO 2025 results (Harmonic's model Aristotle achieved gold medal performance, solving 5 problems). https://github.com/harmonic-ai/IMO2025/ #FormalVerification #ProofAssistant #LeanProver #LLMs #Math #IMO
-
Formalized formal logic (in Lean4). https://formalizedformallogic.github.io/Book/ #FormalVerification #ProofAssistant #LeanProver #Logic #Math
-
Gödel's first incompleteness theorem (in Lean4). https://formalizedformallogic.github.io/Book/first_order/goedel1.html #FormalVerification #ProofAssistant #LeanProver #Logic #Math
-
Encoding finite state automata in Agda using coinduction (Evaluating the support for coinduction in Agda). ~ Noky Soekarman. https://repository.tudelft.nl/file/File_56e70e9e-4f41-429c-a383-20c1bf61c16a #FormalVerification #ProofAssistant #Agda
-
Modelling cyclic structures in Agda (Evaluating Agda’s coinduction through modelling graphs). ~ Faizel Mangroe. https://repository.tudelft.nl/file/File_6466eb89-91b7-4561-9933-236ae3f9e15b #ProofAssistant #Agda
-
CW: Not actually true
Fun fact: they wanted to rename the Coq proof assistant to "glocq", but since the username was already taken on mathstodon they settled on "rocq" instead.
-
There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!
-
There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!
-
There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!
-
There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!
-
There is a real lack of usability studies for doing program verification with dependently typed languages. But broadening our criteria a bit, there are a couple of very useful studies on the usability of other program verification systems such as Dafny, KeY, Frama-C, and others. You can find my attempt so far at a better overview of existing work here: https://researchr.org/bibliography/usability-of-verification-tools/publications. If there's anything that I missed, whether or not it's using dependent types, let me know!
-
I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.
Please boost this so this also finds an audience beyond the types community!
#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory
-
I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.
Please boost this so this also finds an audience beyond the types community!
#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory
-
I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.
Please boost this so this also finds an audience beyond the types community!
#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory
-
I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.
Please boost this so this also finds an audience beyond the types community!
#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory
-
I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.
Please boost this so this also finds an audience beyond the types community!
#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory
-
Liquid Tension Experiment
https://en.wikipedia.org/wiki/Liquid_Tension_Experiment"Liquid Tension Experiment" (self-titled first studio album)
https://songwhip.com/liquid-tension-experiment/liquid-tension-experimentI discovered this group when I read about
#PeterScholze “Liquid Tensor Experiment”: https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/
https://www.nature.com/articles/d41586-021-01627-2#nowlistening #music #InstrumentalRock #ProgressiveRock
#LiquidTensionExperiment
#mathematics #ProofAssistant