ABSTRACT
In a programming language with procedures and assignments, it is often important to isolate uses of state to particular program fragments. The frameworks of type, region, and effect inference, and monadic state are technologies that have been used to state and enforce the property that an expression has no visible side-effects. This property has been exploited to justify the deallocation of memory regions despite the presence of dangling pointers.Starting from an idea developed in the context of monadic state in Haskell, we develop an ML-like language with full assignments and an operator that enforces the encapsulation of effects. Using this language, we formalize and prove the folklore connection between effect masking and monadic encapsulation. Then, by employing a novel set of reductions to deal with dangling pointers, we establish the soundness of the type-based encapsulation with a proof based on a standard subject reduction argument.
Index Terms
- Objects, classes and modules in Objective Caml (invited lecture, abstract only)
Recommendations
Objects, classes and modules in Objective Caml (invited lecture, abstract only)
In a programming language with procedures and assignments, it is often important to isolate uses of state to particular program fragments. The frameworks of type, region, and effect inference, and monadic state are technologies that have been used to ...
Combinators and type-driven transformers in Objective Caml
We describe an implementation of LDTA 2011 Tool Challenge tasks in Objective Caml language. Instead of using some dedicated domain-specific tools we utilize typical functional programming machinery such as polymorphic functions, monads and combinators; ...
Aspectual Caml: an aspect-oriented functional language
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingWe propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. This paper describes the design and implementation ...
Comments