Syntax and Semantics of Cedille

Aaron Stump; Christopher Jenkins

doi:10.48550/arxiv.1806.04709

Back

Preprint

Open access

Syntax and Semantics of Cedille

Aaron Stump and Christopher Jenkins

ArXiv.org

06/12/2018

DOI: 10.48550/arxiv.1806.04709

Files and links (1)

url

https://doi.org/10.48550/arXiv.1806.04709View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

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.

Computer Science - Programming Languages

Details

Title: Subtitle: Syntax and Semantics of Cedille
Creators: Aaron Stump
Christopher Jenkins
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.1806.04709
ISSN: 2331-8422
Language: English
Date posted: 06/12/2018
Academic Unit: Computer Science
Record Identifier: 9984411065702771

Metrics

2 Record Views