2018/11/04 by Aaron Stump, Stump, Aaron
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming Languages (cs.PL) #Software Engineering Research #cs.LO #cs.PL
paper · pdf · doi:10.48550/arxiv.1811.01318
arxiv created 2018/11/04 · openalex publication_date 2018/11/04 · arxiv updated 2018/11/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.