2018/06/12 by Stump, Aaron, Jenkins, Christopher · 1 citation
#FOS: Computer and information sciences #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.1806.04709
This document presents the syntax, classification rules, realizability semantics, and soundness theorem for Cedille, an extrinsic (i.e., Curry-style) type theory extending the Calculus of Constructions, and designed for deriving of inductive datatypes, with their induction principles.