4 ms·
Yes! There is some work being done in this space already; by the incredible people at North-Eastern. One of the more interesting parts of this problem is what y
by ywei3410 6y ago
Yes! There is some work being done in this space already; by the incredible people at North-Eastern. One of the more interesting parts of this problem is what you do at the /boundaries/ of the different languages with differing semantics such that you don't accidentally introduce bad lemmas.
There are a few published papers which study the boundary between dynamic and static type-systems, but the hope was to extend it into gradual-typing between different type-systems .
- nextos 6y agoI think I know some of these papers, but could you please point me to some of the references you have mentioned?
- ywei3410 6y agoOf course — this paper talks about the mechanism which Racket explores to keep the boundary safe [1]. This paper [2] elaborates on some of the performance challenges. 'Shallow typing' by Ben Greenman et al. is available only by video [3] and slideshow form [4]. Finally, there's a really interesting paper which came out this year which uses a verifier to remove the some of the runtime cost [5] of sound gradual typing. [1] https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf https://www.cs.utah.edu/plt/publications/oopsla12-stff.pdf [2] https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf https://www2.ccs.neu.edu/racket/pubs/popl16-tfgnvf.pdf [3] https://www.youtube.com/watch?v=A4AA8nweYAg https://www.youtube.com/watch?v=A4AA8nweYAg [4] https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.pdf https://www.ccs.neu.edu/~types/resources/talks/g-rcon-2020.p... [5] https://arxiv.org/abs/2007.12630 https://arxiv.org/abs/2007.12630
- nextos 6y agoThank you so much!