Defunctionalization with Dependent Types
https://dl.acm.org/doi/pdf/10.1145/3591241
https://dl.acm.org/doi/pdf/10.1145/3591241
Revisiting the DOS memory models
https://blogsystem5.substack.com/p/dos-memory-models
https://blogsystem5.substack.com/p/dos-memory-models
Substack
Revisiting the DOS memory models
At the beginning of the year, I wrote a bunch of articles on the various tricks DOS played to overcome the tight memory limits of x86’s real mode. There was one question that came up and remained unanswered: what were the various “models” that the compilers…
Structural abstract interpretation, A formal study using Coq
https://inria.hal.science/inria-00329572v2/
https://inria.hal.science/inria-00329572v2/
inria.hal.science
Structural abstract interpretation, A formal study using Coq
Abstract interpreters are tools to compute approximations for behaviors of a program. These approximations can then be used for optimisation or for error detection. In this paper, we show how to describe an abstract interpreter using the type-theory based…
Functional programming self-affirmations
https://norikitech.com/posts/functional-affirmations/
https://norikitech.com/posts/functional-affirmations/
NorikiTech
Functional programming self-affirmations
Defunctionalization at Work
https://www.cs.cornell.edu/courses/cs6110/2012sp/Defunctionalization-at-work-Danvy.pdf
https://www.cs.cornell.edu/courses/cs6110/2012sp/Defunctionalization-at-work-Danvy.pdf
Modular Polymorphic Defunctionalization
https://pdfs.semanticscholar.org/4035/76fd488b34418bccd446b7abaee80f4176f5.pdf
https://pdfs.semanticscholar.org/4035/76fd488b34418bccd446b7abaee80f4176f5.pdf
Deriving Dependently-Typed OOP from First Principles
https://dl.acm.org/doi/pdf/10.1145/3649846
https://dl.acm.org/doi/pdf/10.1145/3649846
This equation will change how you see the world (the logistic map)
https://youtu.be/ovJcsL7vyrk?si=XuE-Rdd8qgD8g14I
https://youtu.be/ovJcsL7vyrk?si=XuE-Rdd8qgD8g14I
YouTube
This equation will change how you see the world (the logistic map)
The logistic map connects fluid convection, neuron firing, the Mandelbrot set and so much more. Fasthosts Techie Test competition is now closed! Learn more about Fasthosts here: https://www.fasthosts.co.uk/veritasium Code for interactives is available below...…
The 70% problem
: Hard truths about AI-assisted codinghttps://addyo.substack.com/p/the-70-problem-hard-truths-about
Substack
The 70% problem: Hard truths about AI-assisted coding
A field guide and why we need to rethink our expectations
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism
https://www.sciencedirect.com/science/article/pii/S0304397522000317
https://www.sciencedirect.com/science/article/pii/S0304397522000317
800088.802823.pdf
409.2 KB
The consequences of one's first programming language
A Verified Implementation of Dijkstra's Algorithm
https://github.com/fetburner/coq-dijkstra
https://github.com/fetburner/coq-dijkstra
GitHub
GitHub - fetburner/coq-dijkstra: A Verified Implementation of Dijkstra's Algorithm
A Verified Implementation of Dijkstra's Algorithm. Contribute to fetburner/coq-dijkstra development by creating an account on GitHub.
Making memcpy(NULL, NULL, 0) well-defined
https://developers.redhat.com/articles/2024/12/11/making-memcpynull-null-0-well-defined#compiler_builtins
https://developers.redhat.com/articles/2024/12/11/making-memcpynull-null-0-well-defined#compiler_builtins
Red Hat Developer
Making memcpy(NULL, NULL, 0) well-defined | Red Hat Developer
Undefined behavior (UB) in the C programming language is a regular source of heated discussions among programmers. On the one hand, UB can be important for compiler optimizations. On the other hand
Tail recursion for macros in C
https://gustedt.wordpress.com/2024/07/19/tail-recursion-for-macros-in-c/
https://gustedt.wordpress.com/2024/07/19/tail-recursion-for-macros-in-c/
Jens Gustedt's Blog
Tail recursion for macros in C
In view of the addition of __VA_OPT__ first to C++ and now to C23, there had been interest in extending the C preprocessor to include recursion. The basic idea would be that __VA_OPT__ can be used …
Curiously Cumbersome Rust
: Type-level Programminghttps://geo-ant.github.io/blog/2023/rust-type-level-programming/
geo-ant.github.io
Curiously Cumbersome Rust: Type-level Programming
The moment that spawned this article was when I asked myself how hard
can it be to make sure two types have the same size at compile time? Well…
it’s complicated. In here, we’ll do a deep dive into the limits of compile
time metaprogamming in today’s (and…
can it be to make sure two types have the same size at compile time? Well…
it’s complicated. In here, we’ll do a deep dive into the limits of compile
time metaprogamming in today’s (and…
Free Monads, Intrinsic Scoping, and Higher-Order Preunification
https://arxiv.org/pdf/2204.05653
https://arxiv.org/pdf/2204.05653
c11comp.pdf
581.1 KB
Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it