HackerPapers

arXiv:2304.04574cs.PL

Defunctionalization with Dependent Types

Yulong Huang, Jeremy Yallop

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

Abstract

The defunctionalization translation that eliminates higher-order functions from programs forms a key part of many compilers. However, defunctionalization for dependently-typed languages has not been formally studied. We present the first formally-specified defunctionalization translation for a dependently-typed language and establish key metatheoretical properties such as soundness and type preservation. The translation is suitable for incorporation into type-preserving compilers for dependently-typed languages

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Apr 2023 to Apr 2023. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.