arXiv subjects

Raymond Hu

Publications and source records attributed to Raymond Hu.

10 recordsLinked to original sources

arXiv2026

Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)

Go's unique combination of structural subtyping between generics and types with non-uniform runtime representations presents significant challenges for formalising the language. We introduce WG (Welterweight Go), a core model of Go that captures key features excluded by prior work, including underlying types, type unions and type sets, and proposed new features, such as generic methods. We also develop LWG, a lower-level language that models Go's runtime mechanisms, notably the distinction between raw struct values and interface values that carry runtime type information (RTTI). We give a type-directed compilation from WG to LWG that demonstrates how the proposed features can be implemented while observing important design and implementation goals for Go: compatibility with separate compilation, and no runtime code generation. Unlike existing approaches based on static monomorphisation, our compilation strategy uses runtime type conversions and adaptor methods to handle the complex interactions between structural subtyping, generics, and Go's runtime infrastructure.

cs.PL↗

arXiv2026

Mixed Choice in Asynchronous Multiparty Session Types

We present a multiparty session type (MST) framework with asynchronous mixed choice (MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.

cs.DC↗

arXiv2026

Speak Now: Safe Actor Programming with Multiparty Session Types (Extended Version)

Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. Multiparty session types (MPSTs) rule out communication errors early in the development process, but until now, the many-sender, single-receiver nature of actor communication has made it difficult for actor languages to benefit from session types. This paper introduces Maty, the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions. Maty therefore combines the error prevention mechanism of session types with the scalability and fault tolerance of actor languages. Our main insight is to enforce session typing through a flow-sensitive effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will a session get stuck because an actor is waiting for a message that will never be sent. We extend Maty to support Erlang-style supervision and cascading failure, and show that this preserves Maty's strong metatheory. We implement Maty in Scala using an API generation approach, and demonstrate the expressiveness of our model by implementing a representative sample of the widely-used Savina actor benchmark suite; an industry-supplied factory scenario; and a chat server.

cs.PL↗

arXiv2025

Design and initial results from the "Junior" Levitated Dipole Experiment

OpenStar Technologies is a private fusion company exploring the levitated dipole concept for commercial fusion energy production. OpenStar has manufactured a new generation of levitated dipole experiment, called "Junior", leveraging recent advances made in high-temperature superconducting magnet technologies. Junior houses a ~5.6 T REBCO high-temperature superconducting magnet in a 5.2 m vacuum chamber, with plasma heating achieved via < 50 kW of electron cyclotron resonance heating power. Importantly, this experiment integrates novel high temperature superconductor power supply technology on board the dipole magnet. Recently OpenStar has completed first experimental campaigns with the Junior experiment, achieving first plasmas in late 2024. Experiments conducted with the full levitated system are planned for 2025. This article provides an overview of the main results from these experiments and details improvements planned for future campaigns.

physics.plasm-ph↗

arXiv2024

Proceedings 15th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software

This volume contains the proceedings of PLACES 2024, the 15th edition of the Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The PLACES workshop series offers a forum for researchers from different fields to exchange new ideas about the challenges of modern and future programming, where concurrency and distribution are the norm rather than a marginal concern. PLACES 2024 was held on 6 April 2024 in Luxembourg City, Luxembourg. The programme included keynote talks by Mariangiola Dezani-Ciancaglini and Peter M\"uller, presentations of five research papers, and three talks about preliminary or already-published work that could foster interesting discussion during the workshop. These proceedings contain the five accepted research papers, the abstracts of the keynote talks, and a list of the other contributions.

cs.PL↗

arXiv2020

Statically Verified Refinements for Multiparty Protocols

With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom. While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types. We provide an implementation of RMPST, in a toolchain called Session*, using Scribble, a multiparty protocol description toolchain, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in Scribble and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a na\"ive implementation, while guaranteeing safety properties from the underlying theory.

cs.PL↗

arXiv2020

Featherweight Go

We describe a design for generics in Go inspired by previous work on Featherweight Java by Igarashi, Pierce, and Wadler. Whereas subtyping in Java is nominal, in Go it is structural, and whereas generics in Java are defined via erasure, in Go we use monomorphisation. Although monomorphisation is widely used, we are one of the first to formalise it. Our design also supports a solution to The Expression Problem.

cs.PL↗

arXiv2012

Parameterised Multiparty Session Types

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from G\"odel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

cs.LO↗

arXiv2011

Secure Execution of Distributed Session Programs

The development of the SJ Framework for session-based distributed programming is part of recent and ongoing research into integrating session types and practical, real-world programming languages. SJ programs featuring session types (protocols) are statically checked by the SJ compiler to verify the key property of communication safety, meaning that parties engaged in a session only communicate messages, including higher-order communications via session delegation, that are compatible with the message types expected by the recipient. This paper presents current work on security aspects of the SJ Framework. Firstly, we discuss our implementation experience from improving the SJ Runtime platform with security measures to protect and augment communication safety at runtime. We implement a transport component for secure session execution that uses a modified TLS connection with authentication based on the Secure Remote Password (SRP) protocol. The key technical point is the delicate treatment of secure session delegation to counter a previous vulnerability. We find that the modular design of the SJ Runtime, based on the notion of an Abstract Transport for session communication, supports rapid extension to utilise additional transports whilst separating this concern from the application-level session programming task. In the second part of this abstract, we formally prove the target security properties by modelling the extended SJ delegation protocols in the pi-calculus.

cs.DC↗

arXiv2010

Session-Based Programming for Parallel Algorithms: Expressiveness and Performance

This paper investigates session programming and typing of benchmark examples to compare productivity, safety and performance with other communications programming languages. Parallel algorithms are used to examine the above aspects due to their extensive use of message passing for interaction, and their increasing prominence in algorithmic research with the rising availability of hardware resources such as multicore machines and clusters. We contribute new benchmark results for SJ, an extension of Java for type-safe, binary session programming, against MPJ Express, a Java messaging system based on the MPI standard. In conclusion, we observe that (1) despite rich libraries and functionality, MPI remains a low-level API, and can suffer from commonly perceived disadvantages of explicit message passing such as deadlocks and unexpected message types, and (2) the benefits of high-level session abstraction, which has significant impact on program structure to improve readability and reliability, and session type-safety can greatly facilitate the task of communications programming whilst retaining competitive performance.

cs.PL↗