Inductive Definitions in the system Coq - Rules and Properties

Lecture Notes in Computer Science · 1989 · Lecture notes in computer science · DOI 10.1007/bfb0040259

1 Pith paper cite this work, alongside 99 external citations. Polarity classification is still indexing.

1 Pith paper citing it

99 external citations · OpenAlex

open at publisher browse 1 citing papers

representative citing papers

cs.LO · 2025-05-15 · conditional · novelty 6.0

Impredicative encodings of W-types and M-types are proven to satisfy the eta rules and induction and coinduction, extending AFS18.

Showing 1 of 1 citing paper.

Master Thesis Impredicative Encodings of Inductive and Coinductive Types cs.LO · 2025-05-15 · conditional · none · ref 442
Impredicative encodings of W-types and M-types are proven to satisfy the eta rules and induction and coinduction, extending AFS18.