Inductive families
From MaRDI portal
Publication:1336951
DOI10.1007/BF01211308zbMath0808.03044MaRDI QIDQ1336951
Publication date: 26 October 1994
Published in: Formal Aspects of Computing (Search for Journal in Brave)
natural deductionMartin-Löf's type theoryrecursive definitionsintuitionistic type theoryinductive definitionsgeneralized inductionformalisation of untyped lambda calculus
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
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