A resource for learning Standard ML

This is an excellent little resource for the language. A great text to accompany Purely Functional Data Structures.

Yet another case of a bright researcher getting consumed by the corporate world…

Ballerina is an open-source programming language for the cloud that makes it easier to use, combine and create network services.

A very interesting idea for a programming language which, for better or worse, I never got around to using. Would likely be a lot more interesting if I actually had infra to maintain.

Met him through the Interact Fellowship in summer 2023. Very cool programming dude. Seems to basically fallen off the face of the earth: his Twitter no longer exists, his website is extremely barren, and he hasn’t committed on GitHub in at least a year. Hope he’s doing alright.

see: https://github.com/maxkrieger

Multi-language programs are ubiquitous and language designers have long been designing programming languages to support interoperability. We’ve had platforms such as .NET, JVM, and COM that facilitate interoperability, and languages such as Scala, F#, SML.NET, and many more that treat it as a central design feature. In a 2007 paper, Matthews and Findler pointed out that most multi-language research was focused almost exclusively on how to implement interoperability efficiently and not on the quite subtle semantics of these features. They presented a multi-language semantics framework that gives language designers a methodology for taking two languages, adding interoperability boundaries between them, and giving an operational semantics to those boundaries. I’ll describe the mechanics of multi-language semantics, how they support reasoning about the behavior of mixed-language programs, and discuss the impact that this tool has had in the last 15 years […]

see: https://dl.acm.org/doi/10.1145/1190216.1190220

This talk is about how to change the status quo to make it easier to build multi-language software.  I’ll argue that language designers should equip their “core” language with extensions, dubbed linking types, that allow programmers to annotate how their components should interact with features missing from their core language.  Moreover, toolchain developers should devise compilers and linkers that prevent linking with external code that violates safety or security properties provided by the core language, unless the programmer uses linking-type annotations to request such linking.

I am a Chancellor’s Fellow and Lecturer in the department of Computer and Information Sciences at the University of Strathclyde. I am a member the department’s Mathematically Structured Programming (MSP) group.

My research is on the design and analysis of programming languages. I use mathematical ideas and structure from logic, category theory, type theory, and denotational semantics to study programming languages and the systems they describe.

Extremely cracked.

A lot of really interesting ideas in here. Unfortunately got lost in the notation since there isn’t a recording. Lots of great links within!

Our vision is to use mathematics to understand the nature of computation, and to turn that understanding into the next generation of programming languages.

We see the mathematical foundations of computation and programming as inextricably linked. We study one so as to develop the other. This reflects the symbiotic relationship between mathematics, programming, and the design of programming languages — any attempt to sever this connection will diminish each component.

How Rust prevents data races, and how languages like it could influence future code generation.

Bidirectional tools can often be used for unidirectional use cases, but they are also usually designed with those two specific languages in mind, which constrains the utility of the underlying bindings for work with other languages. You can’t use the bindings as a neutral “hub” that many languages radiate out from.

Too many programming languages researchers dismiss concrete syntax as an afterthought […] This received view ignores a critical factor: the human at the computer. Concrete syntax defines the principal interface through which programmers interact with the vast majority of programming languages. Moreover, this interface is hardly decoupled from semantics; even trivial-seeming differences in keywords, sigils, and indentation can affect how programmers utilize and reason about language behavior. Using examples from asynchronous control flow, gradual subtyping, first-class functions, and more, I will make a case for the importance of concrete syntax, why language designers often overlook it, and what this implies for those of us who care about the usability of abstractions. Finally, I will describe some preliminary work evaluating the role of lexical ambiguity in programmer comprehension of type system features.

A return to an old flame of mine.

see: https://slim.computer/concrete-syntax/

Some nice patterns, both in the main body and the comments, for implementing lenses with a light sprinkling of category theory.

via: https://haskellforall.com/2026/06/ergonomic-overrides-for-nixpkgs

What I enjoy most about these (semantic) editor combinators is that their use is type-directed and so doesn’t require much imagination. When I have the type of a complex value, and I want to edit some piece buried inside, I just read off the path in the containing type, on the way to the buried value.

via: https://haskellforall.com/2026/06/ergonomic-overrides-for-nixpkgs

Announcement post for the override-utils Nix package

A very compelling application of lenses!

Lookin’ at you, JSON

This talk will focus on one such verification approach that takes as input a design under verification (DUV), modest architect-friendly DUV metadata, and a HW-SW contract. The approach automatically generates many simple formal properties that provably compose to imply the contract, and then evaluates them against the DUV to assess contract compliance. The enabling insight is that many important HW-SW contracts decompose into instantiations of a small, finite set of property templates, fillable automatically from the supplied metadata or from the results of evaluating other generated properties. This verification approach eliminates manual property writing, targets full HW-SW contracts rather than coverage metrics, and yields properties simple enough that commercial formal model checkers can produce unbounded proofs for most, even on complex designs.

One consequence of this is that checking whether assumptions hold is a different problem from verifying that your code works given the assumptions. Like to make sure “all unsafe blocks are safe” can’t use the Rust compiler, you need a second tool like Miri. I wonder if checking assumptions is, in practice, generally more difficult than checking everything else.