11 citations · 22 across the 4 of their papers we have counts for
4 papers
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…
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…
Is Sized Typing for Coq Practical?
Jonathan Chan, Yufeng Li, William J. Bowman
Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theo…
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…