# A Type System for First-Class Layers with Inheritance, Subtyping, and Swapping

## TL;DR

This paper introduces a formal type system for a context-oriented programming language with first-class layers, inheritance, subtyping, and swapping, ensuring type safety in dynamic context-dependent software modifications.

## Contribution

It formalizes a small COP language with a sound type system that models key features of JCop, including dynamic layer activation and inheritance.

## Key findings

- Proves type soundness of the language
- Models dynamic layer activation and inheritance
- Ensures type safety in context-dependent modifications

## Abstract

Context-Oriented Programming (COP) is a programming paradigm to encourage modularization of context-dependent software. Key features of COP are layers---modules to describe context-dependent behavioral variations of a software system---and their dynamic activation, which can modify the behavior of multiple objects that have already been instantiated. Typechecking programs written in a COP language is difficult because the activation of a layer can even change objects' interfaces. Inoue et al. have informally discussed how to make JCop, an extension of Java for COP by Appeltauer et al., type-safe. In this article, we formalize a small COP language called ContextFJ$_{<:}$ with its operational semantics and type system and show its type soundness. The language models main features of the type-safe version of JCop, including dynamically activated first-class layers, inheritance of layer definitions, layer subtyping, and layer swapping.