Modal logic, originated in Mathematics and Philosophy, plays nowadays an important role in Computer Science. For instance in the theory of programming languages, where modal formulas of the form $\Box A$, can be considered as types designating enhanced or encapsulated values, in contrast to ordinary values of type $A$. The encapsulation feature can be interpreted in several ways, for instance as run-time generated code that computes values of type~$A$, useful in staged computation; or as the type of mobile code of type~$A$ in distributed computing.
In this talk I present a programming language prototype for encapsulated computation where the typing is controlled by a sequent-calculus whose cut elimination process generates an operational semantics related to the so-called A-normal form, an essential transformation in the compilation of functional languages. This research is being supported by UNAM-DGAPA-PAPIIT IN119920.