cispa_all_3462.pdf (1.28 MB)

On the Semantic Expressiveness of Recursive Types

Download (1.28 MB)
conference contribution
posted on 2023-11-29, 18:17 authored by Marco Patrignani, Eric Mark Martin, Dominique Devriese
Recursive types extend the simply-typed lambda calculus (STLC) with the additional expressive power to enable diverging computation and to encode recursive data-types (e.g., lists). Two formulations of recursive types exist: iso-recursive and equi-recursive. The relative advantages of iso- and equi-recursion are well- studied when it comes to their impact on type-inference. However, the relative semantic expressiveness of the two formulations remains unclear so far. This paper studies the semantic expressiveness of STLC with iso- and equi-recursive types, proving that these formulations are equally expressive. In fact, we prove that they are both as expressive as STLC with only term-level recursion. We phrase these equi-expressiveness results in terms of full abstraction of three canonical compilers between these three languages (STLC with iso-, with equi-recursive types and with term-level recursion). Our choice of languages allows us to study expressiveness when interacting over both a simply-typed and a recursively-typed interface. The three proofs all rely on a typed version of a proof technique called approximate backtranslation. Together, our results show that there is no difference in semantic expressiveness between STLCs with iso- and equi-recursive types. In this paper, we focus on a simply-typed setting but we believe our results scale to more powerful type systems like System F.


Preferred Citation

Marco Patrignani, Eric Martin and Dominique Devriese. On the Semantic Expressiveness of Recursive Types. In: Symposium on Principles of Programming Languages (POPL). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Symposium on Principles of Programming Languages (POPL)

Legacy Posted Date


Open Access Type

  • Gold


@inproceedings{cispa_all_3462, title = "On the Semantic Expressiveness of Recursive Types", author = "Patrignani, Marco and Martin, Eric Mark and Devriese, Dominique", booktitle="{Symposium on Principles of Programming Languages (POPL)}", year="2021", }

Usage metrics


    No categories selected


    Ref. manager