Ciencias de la Computación
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.