Lambda calculus is one of the fundamental mathematical models of computation, where we utilize variables, function abstractions, and function applications. Further, it can be extended with types, giving rise to the typed lambda calculus, which forms the core of functional programming languages. Types in a language provide safety by preventing, for example, the addition of a number and a string. In this work, we present one of the problems that arises when using a functional language in production, where certain processes need to wait for a specified amount of time to pass. We would like the type system to address this problem. A simple type system, as found in OCaml, does not facilitate this requirement, so the type system can be extended with a modal type, which ensures that a resource is not used unless enough time has passed. For proper handling of this type, unboxing and boxing operations are introduced. In this work, we provide stateful operational semantics for this kind of language, where we use state to handle temporal resources correctly. We prove a safety theorem, ensuring that every program written in this language preserves its type and either steps or halt at every moment. We also define an equational theory for this stateful view of resource useage and prove that evaluation in operational semantics respects the equational theory. All results, apart from some cases of the soundness theorem, have also been formalized using the proof assistant Agda.
|
