Case study of over-engineered C++ code (Reimplementing C++ in Object Oriented C)
https://blog.kowalczyk.info/a-aiow/case-study-of-over-engineered-c-code.html
https://blog.kowalczyk.info/a-aiow/case-study-of-over-engineered-c-code.html
blog.kowalczyk.info
Case study of over-engineered C++ code
An example of how to simplify over-engineered C++ code
π3π€1
A Whirlwind Tutorial on Creating Really Teensy ELF Executables for Linux
https://www.muppetlabs.com/~breadbox/software/tiny/teensy.html
https://www.muppetlabs.com/~breadbox/software/tiny/teensy.html
Ryan Fleury β Cracking the Code: Realtime Debugger Visualization Architecture β BSC 2025
https://youtu.be/_9_bK_WjuYY?si=Me3aMV7c2jI4F0x4
https://youtu.be/_9_bK_WjuYY?si=Me3aMV7c2jI4F0x4
YouTube
Ryan Fleury β Cracking the Code: Realtime Debugger Visualization Architecture β BSC 2025
Ryan Fleury's talk at BSC 2025 on the work he's been doing for the Rad Debugger.
Ryan's links:
- https://rfleury.com
- https://x.com/ryanjfleury
- https://github.com/EpicGamesExt/raddebugger
BSC links:
- https://BetterSoftwareConference.com
- https://xβ¦
Ryan's links:
- https://rfleury.com
- https://x.com/ryanjfleury
- https://github.com/EpicGamesExt/raddebugger
BSC links:
- https://BetterSoftwareConference.com
- https://xβ¦
π₯4πΏ2
simpler-lambda-calculus.pdf
662.6 KB
A Simpler Lambda Calculus
https://dl.acm.org/doi/pdf/10.1145/3294032.3294085
https://dl.acm.org/doi/pdf/10.1145/3294032.3294085
β€3π2π2
Engineering for Slow Internet
https://brr.fyi/posts/engineering-for-slow-internet
https://brr.fyi/posts/engineering-for-slow-internet
brr.fyi
Engineering for Slow Internet β brr
How to minimize user frustration in Antarctica.
π7π2β€1
polynomial-complexity-typing.pdf
1.6 MB
Checking Polynomial Time Complexity With Types
https://rd.springer.com/content/pdf/10.1007/978-0-387-35608-2_31.pdf
https://rd.springer.com/content/pdf/10.1007/978-0-387-35608-2_31.pdf
π2π1
Resizable structs in Zig
https://tristanpemble.com/resizable-structs-in-zig/
https://tristanpemble.com/resizable-structs-in-zig/
π2π₯1
Synthesis of Heap-Manipulating Programs from Separation Logic
https://gopiandcode.uk/logs/log-certified-synthesis.html
https://gopiandcode.uk/logs/log-certified-synthesis.html
gopiandcode.uk
Gopiandcode > logs > Goodbye C developers: The future of programming with certified program synthesis
π₯7
plai-v325.pdf
4.7 MB
π₯2
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