scientific article; zbMATH DE number 2061701
From MaRDI portal
Publication:4457447
Recommendations
- scientific article; zbMATH DE number 2182487
- Inductively defined types in the Calculus of Constructions
- Constructing inductive-inductive types in cubical type theory
- Types for Proofs and Programs
- Inductive types in homotopy type theory
- Equational theories for inductive types
- Mathematical induction in ramified type theory
- Computer Science Logic
- Types and invariants in the refinement calculus
- Inductive types and exact completion
Cited in
(20)- The extended calculus of constructions (ECC) with inductive types
- A construction method for induced types and its application to G₂
- Total objects in inductively defined types
- Corrigendum to: ``Inductive-data-type systems
- scientific article; zbMATH DE number 1696611 (Why is no real title available?)
- First steps towards cumulative inductive types in CIC
- Type theory in type theory using quotient inductive types
- Reduction and conversion strategies for the calculus of (co)inductive constructions. I
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
- scientific article; zbMATH DE number 5994829 (Why is no real title available?)
- Inductive Type Schemas as Functors
- Dual Calculus with Inductive and Coinductive Types
- A New Elimination Rule for the Calculus of Inductive Constructions
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- On lists and other abstract data types in the calculus of constructions
- scientific article; zbMATH DE number 1512607 (Why is no real title available?)
- scientific article; zbMATH DE number 2182487 (Why is no real title available?)
- Cumulative inductive types in Coq
- Type theories from Barendregt's cube for theorem provers
- Inductively defined types in the Calculus of Constructions
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4457447)
