Intrinsically-Typed Definitional Interpreters for Imperative Languages

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser

Research output: Contribution to journalArticleScientificpeer-review

315 Downloads (Pure)

Abstract

A definitional interpreter defines the semantics of an object language in terms of the (well-known) semantics of a host language, enabling understanding and validation of the semantics through execution. Combining a definitional interpreter with a separate type system requires a separate type safety proof. An alternative approach, at least for pure object languages, is to use a dependently-typed language to encode the object language type system in the definition of the abstract syntax. Using such intrinsically-typed abstract syntax definitions allows the host language type checker to verify automatically that the interpreter satisfies type safety. Does this approach scale to larger and more realistic object languages, and in particular to languages with mutable state and objects?
In this paper, we describe and demonstrate techniques and libraries in Agda that successfully scale up intrinsically-typed definitional interpreters to handle rich object languages with non-trivial binding structures and mutable state. While the resulting interpreters are certainly more complex than the simply-typed lambda-calculus interpreter we start with, we claim that they still meet the goals of being concise, comprehensible, and executable, while guaranteeing type safety for more elaborate object languages. We make the following contributions: (1) A _dependent-passing style_ technique for hiding the weakening of indexed values as they propagate through monadic code. (2) An Agda library for programming with scope graphs and frames, which provides a uniform approach to dealing with name binding in intrinsically-typed interpreters. (3) Case studies of intrinsically-typed definitional interpreters for the simply-typed lambda-calculus with references (STLC+Ref) and for a large subset of Middleweight Java (MJ).
Original languageEnglish
Article number16
Pages (from-to)1-34
Number of pages34
JournalProceedings of the ACM on Programming Languages
Volume2
Issue numberPOPL
DOIs
Publication statusPublished - 10 Jan 2018

Keywords

  • definitional interpreters
  • dependent types
  • scope graphs
  • mechanized semantics
  • Agda
  • type safety
  • Java
  • scopes and frames

Fingerprint

Dive into the research topics of 'Intrinsically-Typed Definitional Interpreters for Imperative Languages'. Together they form a unique fingerprint.

Cite this