Print Email Facebook Twitter Intrinsically-typed definitional interpreters à la carte Title Intrinsically-typed definitional interpreters à la carte Author van der Rest, C.R. (TU Delft Programming Languages) Poulsen, C.B. (TU Delft Programming Languages) Rouvoet, A.J. (TU Delft Programming Languages) Visser, Eelco (TU Delft Programming Languages) Mosses, P.D. (TU Delft Programming Languages) Date 2022 Abstract Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety. To reference this document use: http://resolver.tudelft.nl/uuid:bfb4aaec-3a78-4a58-a788-cfd7e23991ba DOI https://doi.org/10.1145/3563355 ISSN 2475-1421 Source Proceedings of the ACM on Programming Languages, 6 (OOPSLA2), 1903–1932 Part of collection Institutional Repository Document type journal article Rights © 2022 C.R. van der Rest, C.B. Poulsen, A.J. Rouvoet, Eelco Visser, P.D. Mosses Files PDF 3563355.pdf 462.61 KB Close viewer /islandora/object/uuid:bfb4aaec-3a78-4a58-a788-cfd7e23991ba/datastream/OBJ/view