Abstract:
An intrinsically-typed interpreter is an implementation of the semantics of a programming language. A key feature of intrinsically-typed interpreters is that the type of the interpreter represents the type safety theorem of the object language. We are developing intrinsically-typed interpreters for languages with effects and coeffects. Our aim is to find general abstractions for hiding proof terms and thus enable concise implementation of effectful and coeffectful languages. At the workshop, we intend to discuss with the participants what kind of abstractions would be useful, as well as how to implement those abstractions.
Reference:
Intrinsically-Typed Interpreters for Effectful Languages (Syouki Tsuyama, Youyou Cong and Hidehiko Masuhara), The 1st Workshop on the Implementation of Type Systems (WITS 2022), 2022.
Bibtex Entry:
@misc{tsuyama2022wits,
author = {Syouki Tsuyama and Youyou Cong and Hidehiko Masuhara},
title = {Intrinsically-Typed Interpreters for Effectful Languages},
howpublished = {The 1st Workshop on the Implementation of Type Systems (WITS 2022)},
month = jan,
year = 2022,
url = {https://popl22.sigplan.org/details/wits-2022-papers/11/Intrinsically-Typed-Interpreters-for-Effectful-Languages-discussion-},
abstract = {An intrinsically-typed interpreter is an implementation of the semantics of a programming language. A key feature of intrinsically-typed interpreters is that the type of the interpreter represents the type safety theorem of the object language. We are developing intrinsically-typed interpreters for languages with effects and coeffects. Our aim is to find general abstractions for hiding proof terms and thus enable concise implementation of effectful and coeffectful languages. At the workshop, we intend to discuss with the participants what kind of abstractions would be useful, as well as how to implement those abstractions.},
date = {2022-01-22}
}