Syntax and Semantics of Cedille
Programming Languages
2021-04-29 v3
Abstract
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.
Keywords
Cite
@article{arxiv.1806.04709,
title = {Syntax and Semantics of Cedille},
author = {Aaron Stump and Christopher Jenkins},
journal= {arXiv preprint arXiv:1806.04709},
year = {2021}
}