Record types unify environment and function handling in programming
Record Types Everywhere
Programming Languages
Summary
Programming languages need ways to organize information and run functions, like using boxes to hold tools and instructions. This paper shows that these boxes, called record types, can be used everywhere to represent both environments and how functions work, simplifying programming design. The authors prove their method is safe and behaves predictably, and they even add ways to change data over time. They've done all their proofs and code in a computer system that checks correctness, making their approach trustworthy.
What this means in practice
- •For programming language designers: Design language features that unify environment and function handling using standard record types to simplify and formalize semantics.
- •For formal verification engineers: Develop verified interpreters and semantics for languages supporting mutable state based on this core calculus formalization.
A theory result. No direct application yet.
Authors
Matthew Toohey, Ara Jamalzadeh, Ningning Xie
Abstract
This paper introduces a novel calculus that models first-class environments and function application paradigms using standard record types. By proposing new extensions to general record types, we achieve a design that is remarkably simple and principled. We formalise this design in a core calculus and prove several desirable properties, including type soundness, normalization, and a simulation of the simply typed lambda calculus. Additionally, we extend the design with mutable references. The calculus, its semantics, along with the extension, and all stated properties are fully mechanized in the Lean 4 proof assistant, alongside an interpreter formally verified to be equivalent to the operational semantics.