Tue 18 Jan 2022 08:45 - 09:15 at PEPM - Contributed Talks 3 Chair(s): Youyou Cong

Tagless final embedding provides a solution to the expression problem that also allows efficient code generation, thanks to multi-staged evaluation. It can, however, be a challenge to compose effectful language fragments in this embedding. In this paper, we propose a dependent tagless final embedding, that uses of dependent types to ease the composition of effects. We show that this extension preserves the multi-staging capabilities of tagless final and how it can help scope effects in domain-specific languages.

Tue 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

08:15 - 09:15
Contributed Talks 3PEPM at PEPM
Chair(s): Youyou Cong Tokyo Institute of Technology
08:15
30m
Talk
Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent TypesRemote
PEPM
Christopher Brown University of St. Andrews, UK, Adam D. Barwell Imperial College London, UK, Yoann Marquer INRIA, Rennes, France, Olivier Zendra INRIA, Rennes, France, Tania Richmond INRIA, Rennes, France then DGA - Maîtrise de l’Information, Chen Gu Hefei University of Technology, China
Link to publication
08:45
30m
Talk
Dependent tagless finalRemote
PEPM
Nicolas Biri Luxembourg Institute of Science and Technology
Link to publication