Александр Куклев написал два текста про языки программирования. Первый будет скорее интересен любителям вэлью, второй — академикам

https://akuklev.github.io/objects/

https://akuklev.github.io/HOCC/

BOB Conference 2023

https://www.youtube.com/playlist?list=PLHvf3gk-RdgVuOMnM0Pn8cfEeAEUVeald

Homotopy Type Theory for Sewn Quilts

C. Clark, R. Bohrer

This paper introduces PieceWork, an imperative programming language for the construction of designs for sewn quilts, whose semantics are inspired by Homotopy Type Theory.

https://users.wpi.edu/~rbohrer/pub/farm23.pdf

This is a special topics course in software engineering. The idea that we will explore is that we can now import ongoing advances in the formalization of abstract mathematics (in type theory and to a significant extent around the Lean prover and its mathematics libraries) as new foundations for engineering software programs for systems that inhabit domains that have such abstract mathematical underpinnings.

https://www.computingfoundations.org/index.html

интересную темку рабочий чатик подогнал: https://charm.sh

Explaining Competitive-Level Programming Solutions using LLMs https://arxiv.org/abs/2307.05337

Restrictable Variants: A Simple and Practical Alternative to Extensible Variants
M. Madsen, J.L. Starup, M. Lutze

https://drops-beta.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.17

In the #ECOOP23 paper 'Programming with Purity Reflection: Peaceful Coexistence of Effects, Laziness, and Parallelism,' we present a new programming construct that enables selective lazy and/or parallel evaluation.

In a nutshell, purity reflection enables a higher-order function to inspect the purity of a function argument and to vary its behavior based on this information.
For example, a function like Set.count can use parallel evaluation when given a pure predicate and revert to sequential evaluation when given an impure predicate.

The full paper is available here: https://drops-beta.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.18

You can read more about purity reflection in Flix here: https://doc.flix.dev/purity-reflection.html

MacoCaml: Staging Composable and Compilable Macros
N. Xie, L. White, O. Nicole, J. Yallop

We introduce MacoCaml, a new design and implementation of compile-time code generation for the OCaml language. MacoCaml features a novel combination of macros with phase separation and quotation-based staging, where macros are considered as compile-time bindings, expression cross evaluation phases using staging annotations, and compile-time evaluation happens inside top-level splices. We provide a theoretical foundation for MacoCaml by formalizing a typed source calculus 𝑚𝑎𝑐𝑜 that supports interleaving typing and compile-time code generation, references with explicit compile-time heaps, and modules. We study various crucial properties including soundness and phase distinction. We have implemented MacoCaml in the OCaml compiler, and ported two substantial existing libraries to validate our implementation.

https://xnning.github.io/papers/icfp23.pdf

The First Room-Temperature Ambient-Pressure Superconductor

https://arxiv.org/abs/2307.12008

Воспроизведения пока нет, но на данный момент звучит и выглядит достаточно правдоподобно.

Looking for some interesting summer reading? JFP has just published the latest batch of PhD abstracts for your reading pleasure, with links to the full dissertations. https://www.cambridge.org/core/journals/journal-of-functional-programming/article/phd-abstracts/A32EE036508B4F3B309230D342DA7C2C source

https://arxiv.org/abs/2308.08347

Continuing WebAssembly with Effect Handlers
L. Phipps-Costin, A. Rossberg, A. Guha, D. Leijen, D. Hillerström, KC Sivaramakrishnan, S. Lindley

All OOPSLA’23 papers https://2023.splashcon.org/track/splash-2023-oopsla#event-overview

A Grounded Conceptual Model for Ownership Types in Rust

The blogpost: https://blog.brownplt.org/2023/09/17/rust-ownership.html

The paper: https://cs.brown.edu/~sk/Publications/Papers/Published/cgk-grounded-model-rust-ownership/