Recursive families of inductive types

DOI10.1007/3-540-44659-1_5MaRDI QIDQ2754033zbMATH OpenFDO

Authors Venanzio Capretta

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44659-1_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Inductive families
• Inductively defined types in the Calculus of Constructions
• scientific article; zbMATH DE number 883893
• Positive inductive-recursive definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory

Cited in

(9)

• Inductive families
• Constructive membership predicates as index types
• Refining inductive types
• Global semantic typing for inductive and coinductive computing
• A Type of Partial Recursive Functions
• A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
• A UNIVERSE OF STRICTLY POSITIVE FAMILIES
• scientific article; zbMATH DE number 883893 (Why is no real title available?)
• Builtin types viewed as inductive families

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Recursive families of inductive types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2754033)