Inductive families

DOI10.1007/BF01211308zbMath0808.03044MaRDI QIDQ1336951

Peter Dybjer

Publication date: 26 October 1994

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

natural deductionMartin-Löf's type theoryrecursive definitionsintuitionistic type theoryinductive definitionsgeneralized inductionformalisation of untyped lambda calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35)

Related Items

Canonicity of weak \(\omega\)-groupoid laws using parametricity theory, Finitary higher inductive types in the groupoid model, ProofViz: an interactive visual proof explorer, The construction of set-truncated higher inductive types, The Lean Theorem Prover (System Description), Game semantics for dependent types, A principled approach to programming with nested types in Haskell, A Brief Overview of Agda – A Functional Language with Dependent Types, Unnamed Item, Unnamed Item, Representing inductively defined sets by wellorderings in Martin-Löf's type theory, Homotopy type theory in Lean, Programming language semantics: It’s easy as 1,2,3, A Comparison of Type Theory with Set Theory, Infinite objects in type theory, POPLMark reloaded: Mechanizing proofs by logical relations, Unnamed Item, Induction-recursion and initial algebras., Inductively generated formal topologies., Algebra of Programming Using Dependent Types, Calculating correct compilers, Programming with ornaments, Interactive programming in Agda – Objects and graphical user interfaces, The essence of ornaments, A Syntax for Higher Inductive-Inductive Types, A pattern for almost compositional functions, Hoare type theory, polymorphism and separation, Idris, a general-purpose dependently typed programming language: Design and implementation, Dialogues, Reasons and Endorsement, Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic, Containers, monads and induction recursion, Dependent Types at Work, Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory, The justification of identity elimination in Martin-Löf's type theory, Initial Algebra Semantics for Cyclic Sharing Structures, Algebra of programming in Agda: Dependent types for relational program derivation, Order-sorted inductive types, ETA-RULES IN MARTIN-LÖF TYPE THEORY, A compact kernel for the calculus of inductive constructions, Variations on inductive-recursive definitions, Proofs for free, MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, Constructive hybrid games, Indexed induction-recursion, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, A general formulation of simultaneous inductive-recursive definitions in type theory, \( \pi\) with leftovers: a mechanisation in Agda

Uses Software

• Coq
• LEGO
• Gallina

Cites Work

• Telescopic mappings in typed lambda calculus
• An abstract framework for environment machines
• Normalising the associative law: An experiment with Martin-Löf's type theory
• Propositional functions and families of types
• Do-it-yourself type theory
• Comparing integrated and external logics of functional programs
• Foundation of logic programming based on inductive definition
• The calculus of constructions
• Terminating general recursion
• The foundation of a generic theorem prover
• A natural extension of natural deduction
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item