-
Coqoban: Sokoban (In Coq)
-
Typed Programming Analysis without Encodings (2024) [pdf]
-
Tree Calculus (2021) [pdf]
-
How do modern compilers choose which variables to put in registers?
-
The Illustrated Guide to a PhD
-
How concurrecy works: A visual guide
-
Natural Number Game: build the basic theory of the natural numbers from scratch
-
Tree Calculus
-
Verified Matching of Regular Expressions with Lookarounds
-
CompCert: Formally verified compilers usable for critical embedded software
-
Breaking Bad: How Compilers Break Constant-Time~Implementations
-
A formalization of μμ͂ and classical realizability (2023)
-
With fifth busy beaver, researchers approach computation's limits
-
Show HN: I made a puzzle game and it gently introduces my fav math mysteries
-
Translation of the Rust's core and alloc crates to Coq for formal verification
-
Proving with Coq the 5th Busy Beaver number, BB(5)=47,176,870
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
-
Stalin Sort Algorithm
-
So you think you know C?
-
Kami: A Platform for Hardware Specification and Verification
-
bfcoq: Brainfuck compiler in Coq
-
Bfcoq: Brainfuck Compiler in Coq
-
Can the language of proof assistants be used for general purpose programming?
-
Arm’s Cortex A510: Two Kids in a Trench Coat
-
A Taste of Coq and Correct Code by Construction
-
RISC-V CPU formal specification F# edition
-
Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think?
-
Will Computers Redefine the Roots of Math?
-
Dilemma: very unhappy with a highly-paying tech job. What to do?
-
Which proof assistant is the best to formalize real analysis/probability/statistics?
-
Basics of Proofs [pdf]
-
All??
-
Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?
-
Discussion Thread
-
Inspiring OOP examples?
-
I’ve seen a trend of many right wingers in paradox games so let’s see if that’s true
-
Announcing Magmide Month! (proof language for/using Rust)
-
Relationship between category theory and HoTt?
-
There is such thing called bugfree code.
-
Proofs about Programs
-
Is "my version" of quick-sort incorrect?
-
AI Language Models Are Struggling to “Get” Math
-
What are some possible research questions on compiler construction
-
Is it possible to make C as safe as Rust?
-
Aneris: Program logic for developing and verifying distributed systems
-
What is the need of formally verified compilers? Where are they used? Do verified compiler support all features that unverified compiler do?
-
I made repository containing the sorting and searching algorithms a developer must know
-
Development Environment with guix shell for Coq Package
-
Formally Verifying Rust's Opaque Types
-
New Coq tutorial