8 citations · 8 across the 1 of their papers we have counts for
2 papers
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…