References & Citations
Computer Science > Programming Languages
Title: Syntax and Semantics of Cedille
(Submitted on 12 Jun 2018 (v1), last revised 27 Apr 2021 (this version, 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.
Submission history
From: Christopher Jenkins [view email][v1] Tue, 12 Jun 2018 18:45:55 GMT (13kb)
[v2] Tue, 20 Oct 2020 04:20:21 GMT (13kb)
[v3] Tue, 27 Apr 2021 20:56:16 GMT (23kb)
Link back to: arXiv, form interface, contact.