Skip to content
<awesome-gh-repos>
vic

TiarkRompf/collapsing-towers

Collapsing Towers of Interpreters
Source code at GitHub null
TiarkRompf/collapsing-towers.json
{
  "createdAt": "2016-03-09T02:03:42Z",
  "defaultBranch": "master",
  "description": "Collapsing Towers of Interpreters",
  "fullName": "TiarkRompf/collapsing-towers",
  "homepage": null,
  "language": "Rocq Prover",
  "name": "collapsing-towers",
  "pushedAt": "2025-06-21T19:37:31Z",
  "stargazersCount": 92,
  "topics": [],
  "updatedAt": "2025-11-17T17:57:51Z",
  "url": "https://github.com/TiarkRompf/collapsing-towers"
}

Collapsing Towers of Interpreters

Section titled “Collapsing Towers of Interpreters”

We are concerned with the following challenge: given a sequence of programming languages L_0,...,L_n and interpreters for L_i+1 written in L_i, derive a compiler from L_n to L_0. This compiler should be one-pass, and it should be optimal in the sense that the translation removes all interpretive overhead of the intermediate languages.

See [popl18]!(popl18) directory for the authorative artifact accompanying the POPL 2018 paper Collapsing Towers of Interpreters (PDF).