Showing 1–4 of 4 results for author: Bennetzen, B

Encoding call-by-push-value in the pi-calculus

Authors: Benjamin Bennetzen, Nikolaj Rossander Kristensen, Peter Buus Steffensen

Abstract: In this report we define an encoding of Levys call-by-push-value lambda-calculus (CBPV) in the pi-calculus, and prove that our encoding is both sound and complete. We present informal (by-hand) proofs of soundness, completeness, and all required lemmas. The encoding is specialized to the internal pi-calculus (pi-i-calculus) to circumvent certain challenges associated with using de Bruijn index in… ▽ More In this report we define an encoding of Levys call-by-push-value lambda-calculus (CBPV) in the pi-calculus, and prove that our encoding is both sound and complete. We present informal (by-hand) proofs of soundness, completeness, and all required lemmas. The encoding is specialized to the internal pi-calculus (pi-i-calculus) to circumvent certain challenges associated with using de Bruijn index in a formalization, and it also helps with bisimulation as early-, late- and open-bisimulation coincide in this setting, furthermore bisimulation is a congruence. Additionally, we argue that our encoding also satisfies the five criteria for good encodings proposed by Gorla, as well as show similarities between Milners and our encoding. This paper includes encodings from CBPV in the pi-i-calculus, asynchronous polyadic pi-calculus and the local pi-calculus. We begin a formalization of the proof in Coq for the soundness and completeness of the encoding in the pi-i-calculus. Not all lemmas used in the formalization are themselves formally proven. However, we argue that the non-proven lemmas are reasonable, as they are proven by hand, or amount to Coq formalities that are straightforward given informal arguments. △ Less

Submitted 12 June, 2025; originally announced June 2025.

Comments: 56 pages

A generalised editor calculus (Short Paper)

Authors: Benjamin Bennetzen, Peter Buus Steffensen, Hans Hüttel, Nikolaj Rossander Kristensen, Andreas Tor Mortensen

Abstract: In this paper, we present a generalization of a syntax-directed editor calculus, which can be used to instantiate a specialized syntax-directed editor for any language, given by some abstract syntax. The editor calculus guarantees the absence of syntactical errors while allowing incomplete programs. The generalized editor calculus is then encoded into a simply typed lambda calculus, extended with… ▽ More In this paper, we present a generalization of a syntax-directed editor calculus, which can be used to instantiate a specialized syntax-directed editor for any language, given by some abstract syntax. The editor calculus guarantees the absence of syntactical errors while allowing incomplete programs. The generalized editor calculus is then encoded into a simply typed lambda calculus, extended with pairs, booleans, pattern matching and fixed points △ Less

Submitted 24 May, 2025; originally announced May 2025.

Comments: 7 pages, 21 figures

ACM Class: F.2.2, I.2.7

Cost Analysis for Import and Export Using an Abstract Machine

Authors: Benjamin Bennetzen, Daniel Vang Kleist, Emilie Sonne Steinmann, Loke Walsted, Nikolaj Rossander Kristensen, Peter Buus Steffensen

Abstract: This paper presents the syntax and reduction rules for an abstract machine based on the JavaScript XML language. We incorporate the notion of cost into our reduction rules, and create a type system that over-approximate this cost. This over-approximation results in an equation that may contain unknowns originating from while loops. We conclude with a formal proof of soundness of the type system fo… ▽ More This paper presents the syntax and reduction rules for an abstract machine based on the JavaScript XML language. We incorporate the notion of cost into our reduction rules, and create a type system that over-approximate this cost. This over-approximation results in an equation that may contain unknowns originating from while loops. We conclude with a formal proof of soundness of the type system for our abstract machine, demonstrating that it over-approximates the cost of any terminating program. An implementation of the type system, constraint gathering, and the abstract machine is also presented △ Less

Submitted 23 October, 2024; originally announced October 2024.

Comments: Benjamin Bennetzen: 0009-0007-1751-6862 Daniel Vang Kleist: 0009-0005-1785-2124 Emilie Sonne Steinmann: 0009-0000-4733-5842 Loke Walsted: 0009-0002-1758-4594 Nikolaj Rossander Kristensen: 0009-0005-2339-8247 Peter Buus Steffensen: 0009-0005-6410-5869

Report number: oai:pure.atira.dk:studentproject/3eadb997-8ce2-4f63-81cb-ac29b050f21b

A Type System to Ensure Non-Interference in ReScript

Authors: Benjamin Bennetzen, Daniel Vang Kleist, Emilie Sonne Steinmann, Loke Walsted, Nikolaj Rossander Kristensen, Peter Buus Steffensen

Abstract: Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type sy… ▽ More Protecting confidential data from leaking is a critical challenge in computer systems, particularly given the growing number of observers on the internet. Therefore, limiting information flow using robust security policies becomes increasingly vital. We focus on the non-interference policy, where the goal is to ensure that confidential data can not impact public data. This paper presents a type system, for a subset of the ReScript syntax, designed to enforce non-interference. We conclude with a proof of soundness for the type system, demonstrating that if an expression is type-able, it is inherently non-interferent. In addition, we provide a brief overview of a type checker that implements the previously mentioned type system. △ Less

Submitted 23 October, 2024; originally announced October 2024.

Comments: Benjamin Bennetzen: 0009-0007-1751-6862 Daniel Vang Kleist: 0009-0005-1785-2124 Emilie Sonne Steinmann: 0009-0000-4733-5842 Loke Walsted: 0009-0002-1758-4594 Nikolaj Rossander Kristensen: 0009-0005-2339-8247 Peter Buus Steffensen: 0009-0005-6410-5869

Report number: oai:pure.atira.dk:studentproject/a972b553-b16e-4e5a-ada3-0143f9e1c457