Destructive Environment Operations in the Lambda Calculus with Procedural Features

DOI

10.2991/978-94-6239-638-8_6How to use a DOI?

Keywords

lambda calculus; first-class environments; destructive operation; memory management; operational semantics; type preservation

Abstract

We have studied the lambda calculus with first-class environments in our previous work. The lambda calculus with first-class environments was an extension of the lambda calculus, but it had no destructive operation on the environment. For example, when we receive an actual parameter as a formal parameter, we only add the binding between them to the environment. In this paper, we try to introduce a mechanism that can destructively manipulate the bindings in the environment.

Also, for the purpose of formalizing the resistance to DoS attacks, we have proposed the Spice-calculus. This calculus modifies the mechanism of argument passing in the pi-calculus and the secure pi-calculus, and it makes it possible to handle memory cost explicitly. In the Spice-calculus, we can explicitly add a binding to the environment and also explicitly remove it. The explicit removal of a binding is a destructive operation on the environment. This study is conducted to further extend and deepen these previous works.

In this paper, we extend the lambda calculus by adding limited procedural programming features, such as explicit memory allocation and deallocation. We design a type system so that the amount of memory required by a subterm can be decided from the type information of its environment. By working in a purely functional framework, we can focus on the mechanism of environment operations without the extra complexity of concurrency. We define the syntax of our calculus and present a big-step operational semantics. Moreover, we propose a simple type system and show that the type preservation theorem holds for the big-step semantics in this system.

Copyright

© 2026 The Author(s)

Open Access

Open Access This chapter is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International License (http://creativecommons.org/licenses/by-nc/4.0/), which permits any noncommercial use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

Download article (PDF)

TY  - CONF
AU  - Kosuke Kaneshita
AU  - Shin-ya Nishizaki
PY  - 2026
DA  - 2026/04/30
TI  - Destructive Environment Operations in the Lambda Calculus with Procedural Features
BT  - Proceedings of the  Workshop on Computation: Theory and Practice (WCTP 2025)
PB  - Atlantis Press
SP  - 61
EP  - 73
SN  - 2589-4900
UR  - https://doi.org/10.2991/978-94-6239-638-8_6
DO  - 10.2991/978-94-6239-638-8_6
ID  - Kaneshita2026
ER  -