CN separation logic refinement type system for C. Contribute to rems-project/cn development by creating an account on GitHub.

This article describes a variadic extension to the default fixed-point combinator – namely the Y-combinator. We do this by translating the Scheme code from a paper to bruijn (pure lambda calculus).

:books: Interaction net resources. Contribute to marvinborner/interaction-net-resources development by creating an account on GitHub.

The power of Zig's comptime code execution

This study explores the neural and behavioral consequences of LLM-assisted essay writing. Participants were divided into three groups: LLM, Search Engine, and Brain-only (no tools). Each completed...

Cambridge Core - Programming Languages and Applied Logic - Handbook of Practical Logic and Automated Reasoning

A Lévy-optimal lambda calculus reducer with a backdoor to C - etiams/optiscope

It seems to me that telescopes https://ncatlab.org/nlab/show/type+telescope , the dependently typed notion of context, is more central to the topic of dependent types than the dependent types are.