🦞🌯 Lobster Roll

Thread

Automated Lean Proofs for Every Type (galois.com)
L 6 pts 0 comments by repl Oct 10, 2025 formalmethods thread

Stories related to "Automated Lean Proofs for Every Type" across the full archive.

Automated Lean Proofs for Every Type (galois.com)
HN 40 pts 4 comments by surprisetalk Oct 6, 2025 thread
Automated Lean Proofs for Every Type (galois.com)
L 6 pts 0 comments by repl Oct 10, 2025 formalmethods Programming Languages / CS Theory thread
Automated Lean Proofs for Every Type (galois.com)
HN 1 pts 0 comments by Bogdanp Oct 10, 2025 thread
Lean Forward: Usable Computer-Checked Proofs and Computations for Number Theorists (lean-forward.github.io)
L 7 pts 0 comments by pushcx Aug 7, 2018 formalmethodsmath Programming Languages / CS TheoryScience / Math / Physics thread
Yalep - Micro language based on Lean for teaching mathematical high-school proofs (gricad-gitlab.univ-grenoble-alpes.fr)
L 16 pts 0 comments by jeanthomas Jul 28, 2025 educationformalmethods Programming Languages / CS TheoryScience / Math / Physics thread
Show HN: Lingua Universale – session types and Lean 4 proofs for AI agents (github.com)
HN 1 pts 1 comments by rafapra Feb 26, 2026 AI / Machine Learning thread
Clean Up Your Mess - A Guide to Visual Design for Everyone (visualmess.com)
L 2 pts 0 comments by SeanTAllen Apr 3, 2015 design Design / UX / Visualization thread
Servant, Type Families, and Type-level Everything (arow.info)
L 8 pts 0 comments by pushcx Jul 30, 2015 haskellprogrammingweb Web DevelopmentProgramming (General)Programming Languages / CS Theory thread
Android Defect Reboots Phone Every Time You Type "Reboot" (2008) (gizmodo.com)
L 0 pts 1 comments by kb Oct 28, 2015 android thread
Session Types for Me and You and Everyone We Know! (youtube.com)
L 7 pts 1 comments by unbalancedparentheses Nov 15, 2016 programmingvideo Programming (General) thread
Unit testing, Lean Startup, and everything in-between (codewithoutrules.com)
L 1 pts 2 comments by itamarst Mar 12, 2017 practicestesting Programming (General)Productivity / Career / Business thread
Big picture software testing: unit testing, Lean Startup, and everything in-between (PyCon 2017) (youtube.com)
L 2 pts 2 comments by itamarst May 24, 2017 practicestestingvideo Programming (General)Productivity / Career / Business thread
This is a much improved iteration of the prose version I posted a few weeks (months?) ago.
Programs and Proofs: Mechanizing Mathematics with Dependent Types (ilyasergey.net)
L 6 pts 2 comments by pushcx Jun 9, 2017 formalmethods Programming (General)Programming Languages / CS TheoryScience / Math / Physics thread
Cleanroom Haskell Notes (infohost.nmt.edu)
L 6 pts 1 comments by nickpsecurity Jul 4, 2017 formalmethodshaskellprogramming Programming (General)Programming Languages / CS Theory thread
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System (microsoft.com)
L 22 pts 4 comments by friendlysock Jul 9, 2017 formalmethodspdf Programming Languages / CS Theory thread
Proofs of correctness of the TLS handshake merged to s2n (github.com)
L 10 pts 3 comments by sanxiyn Aug 30, 2017 formalmethodssecurity Programming Languages / CS TheorySecurity / Privacy thread
On The Notion Of Interestingness In Automated Mathematical Discovery (2000) (spiral.imperial.ac.uk)
L 4 pts 3 comments by mjn Oct 30, 2017 aiformalmethodsmathpdf AI / Machine LearningProgramming Languages / CS TheoryScience / Math / Physics thread
Proofsweeper: Play Minesweeper by formally proving your moves in Idris (github.com)
L 10 pts 0 comments by kel Dec 30, 2017 formalmethods Programming Languages / CS Theory thread
Writing basic proofs in ATS (bluishcoder.co.nz)
L 17 pts 0 comments by doublec Jan 3, 2018 formalmethodsprogramming Programming (General)Programming Languages / CS Theory thread
Automated Verification of RISC-V Kernel Code (2016) (courses.cs.washington.edu)
L 2 pts 0 comments by nickpsecurity Jan 26, 2018 assemblyformalmethodspdf Systems / Low-Level / OSProgramming (General)Programming Languages / CS Theory thread
Proofs (and Refutations) using Z3 (blog.janestreet.com)
L 11 pts 0 comments by pushcx Feb 15, 2018 formalmethods Programming Languages / CS Theory thread
Social Processes and Proofs of Theorems and Programs (1979) (cs.cmu.edu)
L 7 pts 5 comments by nickpsecurity Feb 19, 2018 formalmethodspdfpractices Programming (General)Programming Languages / CS TheoryProductivity / Career / Business thread
The original study saying formal verification was useless. In Section 6 of [this paper](http://www.cl.cam.ac.uk/archive/mjcg/papers/AvraProofPaper.pdf), Avra Cohn gave a similar reality check when attempting to mechanize a hardware proof. Also, Guttman summarizes [here](http://www.cypherpunks.to/~pe...
Vulcan: A Javascript Automated Proof System (rmarcus.info)
L 4 pts 0 comments by nickpsecurity Feb 24, 2018 formalmethodsjavascript Web DevelopmentProgramming Languages / CS Theory thread
A resolution-prover in Javascript demo that people can experiment with. Also, gives explanation of CNF and resolution that could aid those building a similar tool in another language.
Automated Verification of Functional Correctness of Race-Free GPU Programs (2017) (fos.kuis.kyoto-u.ac.jp)
L 1 pts 0 comments by nickpsecurity Feb 28, 2018 cformalmethodsgraphicspdf Systems / Low-Level / OSProgramming (General)Programming Languages / CS Theory thread
Abstract: "We study an automated verification method for functional correctness of parallel programs running on GPUs. Our method is based on Kojima and Igarashi’s Hoare logic for GPU programs. Our algorithm generates verification conditions (VCs) from a program annotated by specifications and loop ...
Sum Types Are Coming: What Everyone Should Know (2015) (chadaustin.me)
L 8 pts 2 comments by nickpsecurity Apr 3, 2018 pltpracticesprogramming Programming (General)Programming Languages / CS TheoryProductivity / Career / Business thread
Explains what sum types are and their utility in a way intended to be accessible to wide audience. Includes examples in multiple, programming languages.
Easy CI with fastlane: How we automated everything iOS from running tests to distributing a build (medium.com)
L 1 pts 0 comments by kathleenyanolatos Apr 17, 2018 iosmobiletesting Programming (General)Apple / macOS / iOS thread
Toward a Framework for Highly Automated Vehicle Safety Validation, Philip Koopman & Michael Wagner (users.ece.cmu.edu)
L 4 pts 0 comments by trn Apr 25, 2018 formalmethodspdfpracticestesting Programming (General)Programming Languages / CS TheoryProductivity / Career / Business thread
From Unit Testing to Formal Proofs (adampalay.com)
L 11 pts 1 comments by pushcx May 7, 2018 formalmethodspythontesting Programming (General)Programming Languages / CS Theory thread
Theorem Proving in Lean (leanprover.github.io)
L 14 pts 1 comments by bwr May 28, 2018 formalmethodsmath Programming Languages / CS TheoryScience / Math / Physics thread
I've been finding this a really great intro to automated theorem proving and dependent types, after having wandered for a week or so in the wilderness that is Coq tutorials and books.
The Surprising Security Benefits of End-to-End Formal Proofs (cccblog.org)
L 6 pts 0 comments by GeoffWozniak Jun 14, 2018 formalmethodssecurity Programming Languages / CS TheorySecurity / Privacy thread