Syntax and Typing for Cedille Core

Aaron Stump

doi:10.48550/arxiv.1811.01318

Back

Preprint

Open access

Syntax and Typing for Cedille Core

Aaron Stump

ArXiv.org

11/03/2018

DOI: 10.48550/arxiv.1811.01318

Files and links (1)

url

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

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 specifies a core version of the type theory implemented in the Cedille tool. Cedille is a language for dependently typed programming and computer-checked proof. Cedille can elaborate source programs down to Cedille Core, which can be checked in a straightforward way by a small checker (a reference implementation included with Cedille is under 1000 lines of Haskell). Other tools could also target Cedille Core as an expressive backend type theory. The document describes syntax and typing rules for Cedille Core.

Details

Title: Subtitle: Syntax and Typing for Cedille Core
Creators: Aaron Stump
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.1811.01318
ISSN: 2331-8422
Language: English
Date posted: 11/03/2018
Academic Unit: Computer Science
Record Identifier: 9984411080402771

Metrics

1 Record Views