HackerPapers

arXiv:1806.04709cs.PL

Syntax and Semantics of Cedille

Aaron Stump, Christopher Jenkins

Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.

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.

arXiv comments
Journal reference
DOI
Subjects
cs.PLProgramming Languages

On Hacker News

Linked by 1 identifiable commenter in 1 comment across 1 thread, from Apr 2025 to Apr 2025.

Comments linking this paper, per year.

Discussed in comments1 thread

  1. Dijkstra On the foolishness of "natural language programming" 1 comment

    • Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation…

      codebjeView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.