RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Typeshttps://plv.mpi-sws.org/refinedc/
🔥2
A Minimalistic Verified Bootstrapped Compiler
https://popl21.sigplan.org/details/CPP-2021/6/A-Minimalistic-Verified-Bootstrapped-Compiler-Proof-Pearl-
https://popl21.sigplan.org/details/CPP-2021/6/A-Minimalistic-Verified-Bootstrapped-Compiler-Proof-Pearl-
popl21.sigplan.org
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) (CPP 2021 - Certified Programs and Proofs) - POPL 2021
Certified Programs and Proofs (CPP) is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics…
🔥3
girard-simplification.pdf
1.1 MB
A Simplification of Girard's Paradox
https://www.cs.cmu.edu/afs/cs.cmu.edu/Web/People/kw/scans/hurkens95tlca.pdf
https://www.cs.cmu.edu/afs/cs.cmu.edu/Web/People/kw/scans/hurkens95tlca.pdf
👍3
dlnl-paper.pdf
342.8 KB
Integrating Dependent and Linear Types
https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf
https://www.cl.cam.ac.uk/~nk480/dlnl-paper.pdf
🙏4
A Fast, Growable Array With Stable Pointers in C
https://danielchasehooper.com/posts/segment_array/
https://danielchasehooper.com/posts/segment_array/
Danielchasehooper
A Fast, Growable Array With Stable Pointers in C
My last article about generic data structures in C was written to set the stage for today’s topic: A data structure with constant time indexing, stable pointers, and works well with arena allocators. Its been independently discovered by multiple programmers…
👍5😍2💅1
2504.17033v2.pdf
371.2 KB
Breaking the Sorting Barrier for Directed Single-Source Shortest Paths
https://arxiv.org/abs/2504.17033
https://arxiv.org/abs/2504.17033
❤1😱1
Category Theory for Programmers
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
Bartosz Milewski's Programming Cafe
Category Theory for Programmers: The Preface
Table of Contents Part One Category: The Essence of Composition Types and Functions Categories Great and Small Kleisli Categories Products and Coproducts Simple Algebraic Data Types Functors Functo…
❤7🙏2🤨2
LambdaPi.pdf
185.5 KB
A tutorial implementation of a dependently typed Lambda Calculus
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
❤8🔥1
frama-c-wp-tutorial-en.pdf
3.1 MB
C program proofs with Frama-C and its weakest-precondition plugin
https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
https://allan-blanchard.fr/publis/frama-c-wp-tutorial-en.pdf
❤2👍2
Linear types for programmers
https://twey.io/for-programmers/linear-types/
https://twey.io/for-programmers/linear-types/
❤1
TLA+ in Practice and Theory
https://pron.github.io/posts/tlaplus_part1
https://pron.github.io/posts/tlaplus_part1
Ron Pressler
TLA+ in Practice and Theory
Part 1: The Principles of TLA+
Part 1: The Principles of TLA+
TLA+ is a formal specification and verification language intended to help engineers specify, design and reason about complex, real-life algorithms and software or hardware systems. We explore its motivation, application and principles of design.
❤3
2406.17455v2.pdf
498.7 KB
Smart Casual Verification of the Confidential Consortium Framework
https://arxiv.org/abs/2406.17455
https://arxiv.org/abs/2406.17455
Compiler Bug Causes Compiler Bug: How a 12-Year-Old G++ Bug Took Down Solidityhttps://osec.io/blog/2025-08-11-compiler-bug-causes-compiler-bug
OtterSec
Compiler Bug Causes Compiler Bug: How a 12-Year-Old G++ Bug Took Down Solidity
A subtle G++ bug from 2012, C++20's new comparison rules, and legacy Boost code can collide to crash Solidity's compiler on valid code. We unpack the surprising chain reaction and how to fix it.
😱4
Without the futex, it's futile
https://h4x0r.org/futex/
https://h4x0r.org/futex/
h4x0r.org
Without the futex, it's futile | H4X0R****
Review: It's a history text, not a CS text
😭1
self-reflecting-language.pdf
192.8 KB
A Self-Reflecting Formal Language
https://arxiv.org/pdf/2302.09077v7
https://arxiv.org/pdf/2302.09077v7
👍3
AWS in 2025: The Stuff You Think You Know That’s Now Wronghttps://www.lastweekinaws.com/blog/aws-in-2025-the-stuff-you-think-you-know-thats-now-wrong/
Last Week in AWS
AWS in 2025: The Stuff You Think You Know That’s Now Wrong
One of the neat things about AWS is that it's almost twenty years old. One of the unfortunate things about AWS is... that it's almost twenty years old
🤔1🤯1
Vector Clock: A data structure used for determining the partial ordering of events in a distributed system and detecting causality violationshttps://en.wikipedia.org/wiki/Vector_clock
👍3🤔2
We need to seriously think about what to do with C++ modules
https://nibblestew.blogspot.com/2025/08/we-need-to-seriously-think-about-what.html?m=1
https://nibblestew.blogspot.com/2025/08/we-need-to-seriously-think-about-what.html?m=1
Blogspot
We need to seriously think about what to do with C++ modules
Note: Everything that follows is purely my personal opinion as an individual. It should not be seen as any sort of policy of the Meson buil...
😢1🥴1💅1
Memory Order: The Story Of Strongly Happens Before (C++)https://nekrozqliphort.github.io/posts/happens-b4/
Ryan Chung
Learner’s Notes: Memory Order Side Chapter - The Story Of Strongly Happens Before
Strongly Happens Before? It started innocently enough. I just wanted to brush up on C++ memory orderings. It’s been a while since I last stared into the abyss of std::atomic, so I figured, why not revisit some good ol’ std::memory_order mayhem?
🙏2