Print Email Facebook Twitter Intrinsically-Typed Definitional Interpreters for Imperative Languages Title Intrinsically-Typed Definitional Interpreters for Imperative Languages Author Poulsen, C.B. (TU Delft Programming Languages) Rouvoet, A.J. (TU Delft Programming Languages) Tolmach, Andrew (Portland State University) Krebbers, R.J. (TU Delft Programming Languages) Visser, Eelco (TU Delft Programming Languages) Date 2018-01-10 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). Subject definitional interpretersdependent typesscope graphsmechanized semanticsAgdatype safetyJavascopes and frames To reference this document use: http://resolver.tudelft.nl/uuid:4dc286fd-af6c-4d6b-a59b-bdf446550aa3 DOI https://doi.org/10.1145/3158104 ISSN 2475-1421 Source Proceedings of the ACM on Programming Languages, 2 (POPL), 1-34 Part of collection Institutional Repository Document type journal article Rights © 2018 C.B. Poulsen, A.J. Rouvoet, Andrew Tolmach, R.J. Krebbers, Eelco Visser Files PDF 34370649.pdf 592.15 KB Close viewer /islandora/object/uuid%3A4dc286fd-af6c-4d6b-a59b-bdf446550aa3/datastream/OBJ/view