2 papers
cs.LO2024
(Co)condition hits the Path
Tesla Zhang, Valery Isaev
We propose an enhancement to inductive types and records in a dependent type theory, namely (co)conditions. With a primitive interval type, conditions generalize the cubical syntax…
cs.PL2021
Elegant elaboration with function invocation
Tesla Zhang
We present an elegant design of the core language in a dependently-typed lambda calculus with -reduction and an elaboration algorithm.