Inductive families
type: Item
instance of: scholarly article
title: Inductive families
zbMATH Open document ID: 0808.03044
DOI: 10.1007/BF01211308
author: Peter Dybjer
published in: Formal Aspects of Computing
publication date: 1994-10-26T00:00:00Z
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 672029
zbMATH Keywords: intuitionistic type theory
zbMATH Keywords: formalisation of untyped lambda calculus
zbMATH Keywords: recursive definitions
zbMATH Keywords: Martin-Löf's type theory
zbMATH Keywords: inductive definitions
zbMATH Keywords: natural deduction
zbMATH Keywords: generalized induction
describes a project that uses: Coq
describes a project that uses: LEGO
describes a project that uses: Gallina
MaRDI profile type: Publication
cites work: Do-it-yourself type theory
cites work: Q3894958
cites work: The calculus of constructions
cites work: Q5753923
cites work: An abstract framework for environment machines
cites work: Telescopic mappings in typed lambda calculus
cites work: Comparing integrated and external logics of functional programs
cites work: Q4012883
cites work: Normalising the associative law: An experiment with Martin-Löf's type theory
cites work: A framework for defining logics
cites work: Foundation of logic programming based on inductive definition
cites work: Q5638283
cites work: Q5646883
cites work: Q4099613
cites work: Q3886868
cites work: Q3688389
cites work: Terminating general recursion
cites work: Q3999860
cites work: The foundation of a generic theorem prover
cites work: Q4281483
cites work: A natural extension of natural deduction
cites work: Propositional functions and families of types
description: scientific article; zbMATH DE number 672029