Builtin types viewed as inductive families

DOI10.1007/978-3-031-30044-8_5MaRDI QIDQ6535230zbMATH OpenFDO

Authors Guillaume Allais

Publication date 24 November 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30044-8_5

zbMATH Keywords

Idris 2indexed familiesquantitative type theoryruntime representation

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Data structures (68P05)

Recommendations

• scientific article; zbMATH DE number 4189687
• scientific article; zbMATH DE number 1670736
• Refining inductive types
• On the internal structures of inductive types
• scientific article; zbMATH DE number 3930968
• Inductive, coinductive, and pointed types
• Inductively defined types in the Calculus of Constructions
• scientific article; zbMATH DE number 1629944
• Interpretations of recursively defined types

Cites work

• A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday
• Automating inversion of inductive predicates in Coq
• Equations: a dependent pattern-matching compiler
• Everybody's got to be somewhere
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Inductive families
• Syntax and semantics of quantitative type theory
• The view from the left
• Types for Proofs and Programs

This page was built for publication: Builtin types viewed as inductive families

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