An Elementary Introduction to
Curry Howard de Bruijn Correspondence
https://patternatlas.com/v0/curry-howard-de-bruijn/
Curry Howard de Bruijn Correspondence
https://patternatlas.com/v0/curry-howard-de-bruijn/
PatternAtlas: An Elementary Introduction to the Curry Howard de Bruijn Correspondence
An Elementary Introduction to the Curry Howard de Bruijn Correspondence
An elementary introduction to the Curry Howard de Bruijn Correspondence.
Learn TT: A collection of resources for learning type theory and type theory adjacent fields
https://github.com/jozefg/learn-tt
https://github.com/jozefg/learn-tt
GitHub
GitHub - jozefg/learn-tt: A collection of resources for learning type theory and type theory adjacent fields.
A collection of resources for learning type theory and type theory adjacent fields. - jozefg/learn-tt
👍2
TLA+: A high-level language for modeling programs and systems, especially concurrent and distributed ones
https://lamport.azurewebsites.net/tla/tla.html
https://lamport.azurewebsites.net/tla/tla.html
👍2
Unwinding through a signal handler
https://maskray.me/blog/2022-04-10-unwinding-through-signal-handler
https://maskray.me/blog/2022-04-10-unwinding-through-signal-handler
MaskRay
Unwinding through a signal handler
This post has some notes about unwinding through a signal handler. You may want to read Stack unwinding first. 12345678910111213141516171819202122232425262728293031// a.c#define _GNU_SOURCE#include &l
Deterministic builds with clang and lld
https://blog.llvm.org/2019/11/deterministic-builds-with-clang-and-lld.html
https://blog.llvm.org/2019/11/deterministic-builds-with-clang-and-lld.html
The LLVM Project Blog
Deterministic builds with clang and lld
Deterministic builds can lower continuous integration costs and give you more confidence in your build and test process. This post outlines what it means for a build to be deterministic, the advantages of deterministic builds, and how to achieve them using…
Analysis and introspection options in linkers
https://maskray.me/blog/2022-02-27-analysis-and-introspection-options-in-linkers
https://maskray.me/blog/2022-02-27-analysis-and-introspection-options-in-linkers
MaskRay
Analysis and introspection options in linkers
Updated in 2025-05. Reproduce tarball LLD offers a convenient feature to bundle all input files into a tarball, making it easier to experiment with different linker options. Use either of these comman
All about thread-local storage
https://maskray.me/blog/2021-02-14-all-about-thread-local-storage
https://maskray.me/blog/2021-02-14-all-about-thread-local-storage
MaskRay
All about thread-local storage
Updated in 2025-02. Thread-local storage (TLS) provides a mechanism allocating distinct objects for different threads. It is the usual implementation for GCC extension __thread, C11 _Thread_local, and
Async-signal-safe access to __thread variables from dlopen()ed libraries?
https://sourceware.org/legacy-ml/libc-alpha/2012-06/msg00335.html
https://sourceware.org/legacy-ml/libc-alpha/2012-06/msg00335.html
ELF interposition and -Bsymbolic
https://maskray.me/blog/2021-05-16-elf-interposition-and-bsymbolic
https://maskray.me/blog/2021-05-16-elf-interposition-and-bsymbolic
MaskRay
ELF interposition and -Bsymbolic
This article describes ELF interposition, the linker option -Bsymbolic, and its friends. In the end, it will discuss an ambitious plan which I dubbed "the Last Alliance of ELF and Men". Motivated by a
All about symbol versioning
https://maskray.me/blog/2020-11-26-all-about-symbol-versioning
https://maskray.me/blog/2020-11-26-all-about-symbol-versioning
MaskRay
All about symbol versioning
中文版 Updated in 2023-08. Many people just want to know how to define or reference versioned symbols properly. You may jump to Recommended usage below. In 1995, Solaris' link editor and ld.so introduced
Explaining thread local storage
https://maskray.me/blog/2021-02-14-explaining-thread-local-storage
https://maskray.me/blog/2021-02-14-explaining-thread-local-storage
MaskRay
Explaining thread local storage
Thread local storage provides a mechanism allocating separate objects for different threads. It is the usual implementation for C11 _Thread_local, C++11 thread_local and vendor extension __thread on E
GNU Indirect Function
https://maskray.me/blog/2021-01-18-gnu-indirect-function
https://maskray.me/blog/2021-01-18-gnu-indirect-function
MaskRay
GNU indirect function
Updated in 2024-04. GNU indirect function (ifunc) is a mechanism making a direct function call resolve to an implementation picked by a resolver. It is mainly used in glibc but has adoption in FreeBSD
Cosmopolitan Libc: makes C a build-once run-anywhere language, like Java, except it doesn't need an interpreter or virtual machine. Instead, it reconfigures stock GCC and Clang to output a POSIX-approved polyglot format that runs natively on Linux + Mac + Windows + FreeBSD + OpenBSD + NetBSD + BIOS with the best possible performance and the tiniest footprint imaginable.https://github.com/jart/cosmopolitan
GitHub
GitHub - jart/cosmopolitan: build-once run-anywhere c library
build-once run-anywhere c library. Contribute to jart/cosmopolitan development by creating an account on GitHub.
👍1🤔1
The Sandboxed API project (SAPI) makes sandboxing of C/C++ libraries less burdensome: after initial setup of security policies and generation of library interfaces, a stub API is generated, transparently forwarding calls using a custom RPC layer to the real library running inside a sandboxed environment.
https://github.com/google/sandboxed-api
https://github.com/google/sandboxed-api
GitHub
GitHub - google/sandboxed-api: Generate sandboxes for C/C++ libraries automatically
Generate sandboxes for C/C++ libraries automatically - google/sandboxed-api