Showing 1–20 of 20 results for author: Heuvel, B v d

Information Flow Control in Cyclic Process Networks

Authors: Bas van den Heuvel, Farzaneh Derakhshan, Stephanie Balzer

Abstract: Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC ty… ▽ More Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today's applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session ty** and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work. △ Less

Submitted 2 July, 2024; originally announced July 2024.

Comments: Extended version of ECOOP24 paper

Correctly Communicating Software: Distributed, Asynchronous, and Beyond (extended version)

Authors: Bas van den Heuvel

Abstract: Much of the software we use in everyday life consists of distributed components (running on separate cores or even computers) that collaborate through communication (by exchanging messages). It is crucial to develop robust methods that can give reliable guarantees about the behavior of such message-passing software. With a focus on session types as communication protocols and their foundations in… ▽ More Much of the software we use in everyday life consists of distributed components (running on separate cores or even computers) that collaborate through communication (by exchanging messages). It is crucial to develop robust methods that can give reliable guarantees about the behavior of such message-passing software. With a focus on session types as communication protocols and their foundations in logic, this thesis revolves around the following question: How can we push the boundaries of the logical foundations of session types (binary and multiparty), extending their expressiveness and applicability, while preserving fundamental correctness properties? In this context, this thesis studies several intertwined aspects of message-passing. △ Less

Submitted 1 March, 2024; v1 submitted 14 February, 2024; originally announced February 2024.

Comments: PhD thesis

Comparing Session Type Systems derived from Linear Logic

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (static… ▽ More Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (statically) verify message-passing processes. In this paper, we rigorously compare different type systems for concurrency derived from the Curry-Howard correspondence between linear logic and session types. We address the main divide between these type systems: the classical and intuitionistic presentations of linear logic. Along the years, these presentations have given rise to separate research strands on logical foundations for concurrency; the differences between their derived type systems have only been addressed informally. To formally assess these differences, we develop $π\mathsf{ULL}$, a session type system that encompasses type systems derived from classical and intuitionistic interpretations of linear logic. Based on a fragment of Girard's Logic of Unity, $π\mathsf{ULL}$ provides a basic reference framework: we compare existing session type systems by characterizing fragments of $π\mathsf{ULL}$ that coincide with classical and intuitionistic formulations. We analyze the significance of our characterizations by considering the locality principle (enforced by intuitionistic interpretations but not by classical ones) and forms of process composition induced by the interpretations. △ Less

Submitted 26 January, 2024; originally announced January 2024.

Comments: Revised/extended version of https://doi.org/10.4204/EPTCS.314.1

Monitoring Blackbox Implementations of Multiparty Session Protocols

Authors: Bas van den Heuvel, Jorge A. Pérez, Rares A. Dobre

Abstract: We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for syn… ▽ More We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for synthesizing monitors for blackboxes from global types, and precisely define when a blackbox correctly satisfies its global type. Then, we prove that monitored blackboxes are sound (they correctly follow the protocol) and transparent (blackboxes with and without monitors are behaviorally equivalent). △ Less

Submitted 3 October, 2023; v1 submitted 7 June, 2023; originally announced June 2023.

Comments: Full version with appendices of our RV'23 paper

Asynchronous Functional Sessions: Cyclic and Concurrent

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type syste… ▽ More We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system. △ Less

Submitted 6 September, 2022; originally announced September 2022.

Comments: In Proceedings EXPRESS/SOS 2022, arXiv:2208.14777. arXiv admin note: substantial text overlap with arXiv:2208.07644

Journal ref: EPTCS 368, 2022, pp. 75-94

A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency

Authors: Dan Frumin, Emanuele D'Osualdo, Bas van den Heuvel, Jorge A. Pérez

Abstract: The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems fo… ▽ More The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O'Hearn and Pym's Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new $π$-calculus with sessions, called $π$BI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of $π$BI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine $λ$-calculus; and a non-interference result for access of resources. △ Less

Submitted 12 September, 2022; originally announced September 2022.

Comments: 27 pages + the appendices

Asynchronous Functional Sessions: Cyclic and Concurrent (Extended Version)

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type syste… ▽ More We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system. △ Less

Submitted 19 September, 2022; v1 submitted 16 August, 2022; originally announced August 2022.

Comments: Extended version of a paper accepted at EXPRESS'22. arXiv admin note: substantial text overlap with arXiv:2111.13091

Typed Non-determinism in Functional and Concurrent Calculi

Authors: Bas van den Heuvel, Joseph W. N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez

Abstract: We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are… ▽ More We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a $π$-calculus with non-deterministic choice, governed by session types. Second, we introduce a resource $λ$-calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation. △ Less

Submitted 29 September, 2023; v1 submitted 2 May, 2022; originally announced May 2022.

Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building… ▽ More We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $λ$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence. △ Less

Submitted 4 July, 2024; v1 submitted 25 November, 2021; originally announced November 2021.

Comments: Extended version of arXiv:2110.00146, doi:10.4204/EPTCS.347.3 and arXiv:2209.06820, doi:10.4204/EPTCS.368.5

Deadlock Freedom for Asynchronous and Cyclic Process Networks

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: This paper considers the challenging problem of establishing deadlock freedom for message-passing processes using behavioral type systems. In particular, we consider the case of processes that implement session types by communicating asynchronously in cyclic process networks. We present APCP, a typed process framework for deadlock freedom which supports asynchronous communication, delegation, recu… ▽ More This paper considers the challenging problem of establishing deadlock freedom for message-passing processes using behavioral type systems. In particular, we consider the case of processes that implement session types by communicating asynchronously in cyclic process networks. We present APCP, a typed process framework for deadlock freedom which supports asynchronous communication, delegation, recursion, and a general form of process composition that enables specifying cyclic process networks. We discuss the main decisions involved in the design of APCP and illustrate its expressiveness and flexibility using several examples. △ Less

Submitted 30 September, 2021; originally announced October 2021.

Comments: In Proceedings ICE 2021, arXiv:2109.14908. arXiv admin note: text overlap with arXiv:2101.09038

Journal ref: EPTCS 347, 2021, pp. 38-56

A Decentralized Analysis of Multiparty Protocols

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadl… ▽ More Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadlock freedom for implementations with interleaved and delegated protocols. We propose a decentralized analysis of multiparty protocols, specified as global types and implemented as interacting processes in an asynchronous $π$-calculus. Our solution rests upon two novel notions: router processes and relative types. While router processes use the global type to enable the composition of participant implementations in arbitrary process networks, relative types extract from the global type the intended interactions and dependencies between pairs of participants. In our analysis, processes are typed using APCP, a type system that ensures protocol conformance and deadlock freedom with respect to binary protocols, developed in prior work. Our decentralized, router-based analysis enables the sound and complete transference of protocol conformance and deadlock freedom from APCP to multiparty protocols. △ Less

Submitted 23 May, 2022; v1 submitted 22 January, 2021; originally announced January 2021.

Comments: extended proofs following anonymous reviews

Session Type Systems based on Linear Logic: Classical versus Intuitionistic

Authors: Bas van den Heuvel, Jorge A. Pérez

Abstract: Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same class of pi-calculus processes, but they are significantly different. Caires, Pfenning and Toninho informally observed that, unlike the classical type system, the… ▽ More Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same class of pi-calculus processes, but they are significantly different. Caires, Pfenning and Toninho informally observed that, unlike the classical type system, the intuitionistic type system enforces locality for shared channels, i.e. received channels cannot be used for replicated input. In this paper, we revisit this observation from a formal standpoint. We develop United Linear Logic (ULL), a logic encompassing both classical and intuitionistic linear logic. Then, following the Curry-Howard correspondences for session types, we define piULL, a session type system for the pi-calculus based on ULL. Using piULL we can formally assess the difference between the intuitionistic and classical type systems, and justify the role of locality and symmetry therein. △ Less

Submitted 2 April, 2020; originally announced April 2020.

Comments: In Proceedings PLACES 2020, arXiv:2004.01062

Journal ref: EPTCS 314, 2020, pp. 1-11

The process of purely event-driven programs

Authors: Bas van den Heuvel

Abstract: Using process algebra, this paper describes the formalisation of the process/semantics behind the purely event-driven programming language. Using process algebra, this paper describes the formalisation of the process/semantics behind the purely event-driven programming language. △ Less

Submitted 24 August, 2018; v1 submitted 29 March, 2018; originally announced March 2018.

Comments: Supervisors: Dr. A. Ponse and Dr. ir. B. Diertens; 15 pages, 3 figures in appendix; Updated most process descriptions to the style of PSF. Also fixed some design errors that came to light during testing

On pulse broadening for optical solitons

Authors: H. J. S. Dorren, J. J. B. van den Heuvel

Abstract: Pulse broadening for optical solitons due to birefringence is investigated. We present an analytical solution which describes the propagation of solitons in birefringent optical fibers. The special solutions consist of a combination of purely solitonic terms propagating along the principal birefringence axes and soliton-soliton interaction terms. The solitonic part of the solutions indicates tha… ▽ More Pulse broadening for optical solitons due to birefringence is investigated. We present an analytical solution which describes the propagation of solitons in birefringent optical fibers. The special solutions consist of a combination of purely solitonic terms propagating along the principal birefringence axes and soliton-soliton interaction terms. The solitonic part of the solutions indicates that the decay of initially localized pulses could be due to different propagation velocities along the birefringence axes. We show that the disintegration of solitonic pulses in birefringent optical fibers can be caused by two effects. The first effect is similar as in linear birefringence and is related to the unequal propagation velocities of the modes along the birefringence axes. The second effect is related to the nonlinear soliton-soliton interaction between the modes, which makes the solitonic pulse-shape blurred. △ Less

Submitted 14 October, 1999; v1 submitted 26 May, 1999; originally announced May 1999.

Comments: 11 pages, the manuscript has undergone major revisions

Glueballs on the three-sphere

Authors: Bas van den Heuvel

Abstract: We study the non-perturbative effects of the global features of the configuration space for SU(2) gauge theory on the three-sphere. The strategy is to reduce the full problem to an effective theory for the dynamics of the low-energy modes. By explicitly integrating out the high-energy modes, the one-loop correction to the effective hamiltonian is obtained. Imposing the $θ$ dependence through bou… ▽ More We study the non-perturbative effects of the global features of the configuration space for SU(2) gauge theory on the three-sphere. The strategy is to reduce the full problem to an effective theory for the dynamics of the low-energy modes. By explicitly integrating out the high-energy modes, the one-loop correction to the effective hamiltonian is obtained. Imposing the $θ$ dependence through boundary conditions in configuration space incorporates the non-perturbative effects of the non-contractable loops in the full configuration space. After this we obtain the glueball spectrum of the effective theory with a variational method. △ Less

Submitted 19 August, 1996; originally announced August 1996.

Comments: 48 p LaTeX, 13 Postscript figures appended

Report number: INLO-PUB-16/96

Journal ref: Nucl.Phys. B488 (1997) 282-334

Glueballs on S^3

Authors: Bas van den Heuvel

Abstract: For SU(2) gauge theory on the three-sphere we study the dynamics of the low-energy modes. By explicitely integrating out the high-energy modes, the one-loop correction to the hamiltonian for this problem is obtained. After imposing the $θ$-dependence through boundary conditions in configuration space, we obtain the glueball spectrum of the effective theory with a variational method. For SU(2) gauge theory on the three-sphere we study the dynamics of the low-energy modes. By explicitely integrating out the high-energy modes, the one-loop correction to the hamiltonian for this problem is obtained. After imposing the $θ$-dependence through boundary conditions in configuration space, we obtain the glueball spectrum of the effective theory with a variational method. △ Less

Submitted 5 August, 1996; originally announced August 1996.

Comments: 3p Latex. Talk presented at LATTICE96(theoretical developments)

Report number: INLO-PUB-13/96

Journal ref: Nucl.Phys.Proc.Suppl. 53 (1997) 808-810

One-loop effective action for SU(2) gauge theory on S^3

Authors: Bas van den Heuvel

Abstract: We consider the effective theory for the low-energy modes of SU(2) gauge theory on the three-sphere. By explicitely integrating out the high-energy modes, the one-loop correction to the hamiltonian for this problem is obtained. We calculate the influence of this correction on the glueball spectrum. We consider the effective theory for the low-energy modes of SU(2) gauge theory on the three-sphere. By explicitely integrating out the high-energy modes, the one-loop correction to the hamiltonian for this problem is obtained. We calculate the influence of this correction on the glueball spectrum. △ Less

Submitted 18 April, 1996; originally announced April 1996.

Comments: 12p. latex, 3 PostScript figures included (epsf)

Report number: INLO-PUB-3/96

Journal ref: Phys.Lett. B386 (1996) 233-240

Glueball Spectroscopy on S^3

Authors: Bas van den Heuvel

Abstract: For SU(2) gauge theory on the three-sphere we implement the influence of the boundary of the fundamental domain, and in particular the $θ$-dependence, on a subspace of low-energy modes of the gauge field. We construct a basis of functions that respect these boundary conditions and use these in a variational approximation of the spectrum of the lowest order effective hamiltonian. For SU(2) gauge theory on the three-sphere we implement the influence of the boundary of the fundamental domain, and in particular the $θ$-dependence, on a subspace of low-energy modes of the gauge field. We construct a basis of functions that respect these boundary conditions and use these in a variational approximation of the spectrum of the lowest order effective hamiltonian. △ Less

Submitted 11 September, 1995; originally announced September 1995.

Comments: 8p. latex, 3 uuencoded PostScript figures appended

Report number: INLO-PUB-10/95

Journal ref: Phys.Lett. B368 (1996) 124-130

Dynamics on the SU(2) fundamental domain

Authors: Bas van den Heuvel, Pierre van Baal

Abstract: For SU(2) gauge theory on the three-sphere we focus on a subspace of modes of the gauge field that contains the tunnelling paths and the sphalerons and on which the energy functional is degenerate to second order in the fields. The ultimate goal is to study the $θ$-dependence of the low-lying states for this model by imposing boundary conditions on the fundamental domain. For SU(2) gauge theory on the three-sphere we focus on a subspace of modes of the gauge field that contains the tunnelling paths and the sphalerons and on which the energy functional is degenerate to second order in the fields. The ultimate goal is to study the $θ$-dependence of the low-lying states for this model by imposing boundary conditions on the fundamental domain. △ Less

Submitted 24 November, 1994; originally announced November 1994.

Comments: Contribution to Lattice '94, 3 pages PostScript

Report number: INLO-PUB-17/94

Journal ref: Nucl.Phys.Proc.Suppl. 42 (1995) 823-825

Zooming-in on the SU(2) fundamental domain

Authors: Pierre van Baal, Bas van den Heuvel

Abstract: For SU(2) gauge theories on the three-sphere we analyse the Gribov horizon and the boundary of the fundamental domain in the 18 dimensional subspace that contains the tunnelling path and the sphaleron and on which the energy functional is degenerate to second order in the fields. We prove that parts of this boundary coincide with the Gribov horizon with the help of bounds on the fundamental modu… ▽ More For SU(2) gauge theories on the three-sphere we analyse the Gribov horizon and the boundary of the fundamental domain in the 18 dimensional subspace that contains the tunnelling path and the sphaleron and on which the energy functional is degenerate to second order in the fields. We prove that parts of this boundary coincide with the Gribov horizon with the help of bounds on the fundamental modular domain. △ Less

Submitted 8 October, 1993; v1 submitted 5 October, 1993; originally announced October 1993.

Comments: 19p., 6 figs. appended in PostScript (uuencoded), preprint INLO-PUB-12/93. Revision: ONLY change is a much more economic PostScript code for figures 1-4 (with apologies)

Journal ref: Nucl.Phys. B417 (1994) 215-237