Standard

Intrinsically-Typed Definitional Interpreters for Imperative Languages. / Poulsen, Casper; Rouvoet, Arjen; Tolmach, Andrew; Krebbers, Robbert; Visser, Eelco.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL. Association for Computing Machinery (ACM), 2017.

Research output: Scientific - peer-reviewConference contribution

Harvard

Poulsen, C, Rouvoet, A, Tolmach, A, Krebbers, R & Visser, E 2017, Intrinsically-Typed Definitional Interpreters for Imperative Languages. in Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL. Association for Computing Machinery (ACM).

APA

Poulsen, C., Rouvoet, A., Tolmach, A., Krebbers, R., & Visser, E. (2017). Intrinsically-Typed Definitional Interpreters for Imperative Languages. In Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL. Association for Computing Machinery (ACM).

Vancouver

Poulsen C, Rouvoet A, Tolmach A, Krebbers R, Visser E. Intrinsically-Typed Definitional Interpreters for Imperative Languages. In Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL. Association for Computing Machinery (ACM). 2017.

Author

Poulsen, Casper; Rouvoet, Arjen; Tolmach, Andrew; Krebbers, Robbert; Visser, Eelco / Intrinsically-Typed Definitional Interpreters for Imperative Languages.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL. Association for Computing Machinery (ACM), 2017.

Research output: Scientific - peer-reviewConference contribution

BibTeX

@inbook{4dc286fdaf6c4d6ba59bbdf446550aa3,
title = "Intrinsically-Typed Definitional Interpreters for Imperative Languages",
keywords = "definitional interpreters, dependent types, scope graphs, mechanized semantics, Agda, type safety, Java",
author = "Casper Poulsen and Arjen Rouvoet and Andrew Tolmach and Robbert Krebbers and Eelco Visser",
year = "2017",
month = "11",
booktitle = "Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL",
publisher = "Association for Computing Machinery (ACM)",
address = "United States",

}

RIS

TY - CHAP

T1 - Intrinsically-Typed Definitional Interpreters for Imperative Languages

AU - Poulsen,Casper

AU - Rouvoet,Arjen

AU - Tolmach,Andrew

AU - Krebbers,Robbert

AU - Visser,Eelco

PY - 2017/11/10

Y1 - 2017/11/10

N2 - 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).

AB - 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).

KW - definitional interpreters

KW - dependent types

KW - scope graphs

KW - mechanized semantics

KW - Agda

KW - type safety

KW - Java

UR - https://github.com/metaborg/mj.agda

M3 - Conference contribution

BT - Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL

PB - Association for Computing Machinery (ACM)

ER -

ID: 31446165