Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings
Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings
复制标题
编程语言和系统 - 第 32 届欧洲编程研讨会，ESOP 2023，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2023，法国巴黎，2023 年 4 月 22-27 日，会议记录
DOI：
10.1007/978-3-031-30044-8_5
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Allais G
中科院分区：
文献类型：
--
作者：
Allais G
对于依赖类型的语言，最先进的优化过程可以帮助擦除典型的不变的数据结构和程序的冗余信息。使用IDRIS 2中实现的量化类型理论，我们演示了如何定义一个富含不变量的类型检查时间数据结构，该结构将高效的运行时表示与运行时无关的不变量打包在一起。然后，编译器可以在编译期间积极地擦除所有这些不变量。
State of the art optimisation passes for dependently typed languages can help erase the redundant information typical of invariantrich data structures and programs. These automated processes do not dramatically change the structure of the data, even though more efficient representations could be available.Using Quantitative Type Theory as implemented in Idris 2, we demonstrate how to define an invariant-rich, typechecking-time data structure packing an efficient runtime representation together with runtime irrelevant invariants. The compiler can then aggressively erase all such invariants during compilation.