8 citations · 8 across the 2 of their papers we have counts for
Showing cs.PLShow all
3 papers · 1 filter
cs.PL2025
Macro-embedding Compiler Intermediate Languages in Racket
William J. Bowman
We present the design and implementation of a macro-embedding of a family of compiler intermediate languages, from a Scheme-like language to x86-64, into Racket. This embedding is…
cs.PL2021★ 8 cited
Dependent Type Systems as Macros
Stephen Chang, Michael Ballantyne, Milo Turner +1
We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new depe…
cs.PL2018
Typed Closure Conversion for the Calculus of Constructions
William J. Bowman, Amal Ahmed
Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these…