Lambda Calculus with Regular Types

In this paper we introduce λ_R: A foundational calculus for sequence processing with regular expression types. Its term language is the lambda calculus extended with sequences of terms and its types are regular expressions over simple types. We provide a flexible notion of subtyping based on the semantic notion of nominal interpretation of a type. Then we prove that types are preserved by reduction (subject reduction), and that there exist no infinite reduction sequences starting at typed terms (strong normalization).