Inductive families

From MaRDI portal
Publication:1336951

DOI10.1007/BF01211308zbMath0808.03044MaRDI QIDQ1336951

Peter Dybjer

Publication date: 26 October 1994

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




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