arXiv subjects

Nils Gesbert

Publications and source records attributed to Nils Gesbert.

6 recordsLinked to original sources

arXiv2026

Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications

Modern web applications combine persistent state updates, concurrent interactions, and unreliable communication with external services. Failures such as timeouts can occur after partial state changes, producing temporary inconsistencies whose resolution depends on liveness properties that are often not verified in practice. Although formal methods offer rigorous guarantees for reasoning about complex software, they remain rarely adopted in enterprise settings due to their perceived complexity and lack of practical automation. Multiparty Session Types (MPST) offer strong guarantees for communication safety, yet they do not account for the interplay between state evolution, dynamic workflow structure, and failure behaviour that are essential for reasoning about the correctness of real web applications. This paper introduces a global-type framework that equips MPST with explicit failure semantics and dynamic participation. We define the syntax and operational semantics of these enriched global types and establish core properties, including coherence preservation. This foundation enables formal reasoning about communications in web applications where failures may occur, and lays the groundwork for future stateful extensions and automated verification of liveness properties.

cs.PL↗

arXiv2026

Optimizing Relational Queries over Array-Valued Data in Columnar Systems

Modern analytical workloads increasingly combine relational data with array-valued attributes. While columnar database systems efficiently process such workloads, their ability to optimize queries that interleave relational operators with array manipulations remains limited. This paper introduces A3D-RA, an extended relational algebra supporting array-valued attributes, together with a comprehensive framework for algebraic reasoning and optimization. We formalize its data model and semantics, develop a complete set of equivalence-preserving transformation rules capturing pairwise interactions between relational and array operators, and propose a plan enumeration strategy with an optimality guarantee that remains polynomial in all non-join operators. We design A3D-RA as a modular, backend-independent optimization layer that can be instantiated over existing analytical database systems. Experimental results across three high-performance engines on a real-world workload show consistent performance gains enabled by the proposed algebraic optimization layer.

cs.DB↗

arXiv2024

Schema-Based Query Optimisation for Graph Databases

Recursive graph queries are increasingly popular for extracting information from interconnected data found in various domains such as social networks, life sciences, and business analytics. Graph data often come with schema information that describe how nodes and edges are organized. We propose a type inference mechanism that enriches recursive graph queries with relevant structural information contained in a graph schema. We show that this schema information can be useful in order to improve the performance when evaluating acylic recursive graph queries. Furthermore, we prove that the proposed method is sound and complete, ensuring that the semantics of the query is preserved during the schema-enrichment process.

cs.DB↗

arXiv2023

Efficient Iterative Programs with Distributed Data Collections

Big data programming frameworks have become increasingly important for the development of applications for which performance and scalability are critical. In those complex frameworks, optimizing code by hand is hard and time-consuming, making automated optimization particularly necessary. In order to automate optimization, a prerequisite is to find suitable abstractions to represent programs; for instance, algebras based on monads or monoids to represent distributed data collections. Currently, however, such algebras do not represent recursive programs in a way which allows for analyzing or rewriting them. In this paper, we extend a monoid algebra with a fixpoint operator for representing recursion as a first class citizen and show how it enables new optimizations. Experiments with the Spark platform illustrate performance gains brought by these systematic optimizations.

cs.LO↗

arXiv2015

Modular session types for objects

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestate supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational se-mantics, a sound type system, and a sound and complete type checking algorithm for a small distributed class-based object-oriented language with structural subtyping. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state.

cs.PL↗

arXiv2014

Session Types as Generic Process Types

Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility to race-freedom, lock-freedom, or even responsiveness. Two successful, although rather different, approaches, are session types and process types. The former allows to specify and verify (distributed) communication protocols using specific type (proof) systems; the latter allows to infer from a system specification a process abstraction on which it is simpler to verify properties, using a generic type (proof) system. What is the relationship between these approaches? Can the generic one subsume the specific one? At what price? And can the former be used as a compiler for the latter? The work presented herein is a step towards answers to such questions. Concretely, we define a stepwise encoding of a pi-calculus with sessions and session types (the system of Gay and Hole) into a pi-calculus with process types (the Generic Type System of Igarashi and Kobayashi). We encode session type environments, polarities (which distinguish session channels end-points), and labelled sums. We show forward and reverse operational correspondences for the encodings, as well as typing correspondences. To faithfully encode session subtyping in process types subtyping, one needs to add to the target language record constructors and new subtyping rules. In conclusion, the programming convenience of session types as protocol abstractions can be combined with the simplicity and power of the pi-calculus, taking advantage in particular of the framework provided by the Generic Type System.

cs.PL↗