Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
Abstract elided by the publisher.
Related papers
- Functors are Type Refinement Systems POPL 2015
- Generating Well-Typed Terms That Are Not "Useless" POPL 2024
- Normalization by evaluation for sized dependent types ICFP 2017
- Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types POPL 2019
- Intrinsically-typed definitional interpreters for imperative languages POPL 2018
- Type-safe higher-order channels with channel locality JFP 2009
- Typing Algorithm in Type Theory with Inheritance POPL 1997
- On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem ESOP 2020