Inductive families
From MaRDI portal
Recommendations
Cites work
- A framework for defining logics
- A natural extension of natural deduction
- An abstract framework for environment machines
- Comparing integrated and external logics of functional programs
- Do-it-yourself type theory
- Foundation of logic programming based on inductive definition
- scientific article; zbMATH DE number 3910392 (Why is no real title available?)
- scientific article; zbMATH DE number 3692654 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 65535 (Why is no real title available?)
- scientific article; zbMATH DE number 3521950 (Why is no real title available?)
- scientific article; zbMATH DE number 512790 (Why is no real title available?)
- scientific article; zbMATH DE number 3365218 (Why is no real title available?)
- scientific article; zbMATH DE number 3375475 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Normalising the associative law: An experiment with Martin-Löf's type theory
- Propositional functions and families of types
- Telescopic mappings in typed lambda calculus
- Terminating general recursion
- The calculus of constructions
- The foundation of a generic theorem prover
Cited in
(79)- A compact kernel for the calculus of inductive constructions
- A two-storied universe of transfinite mechanisms
- Order-sorted inductive types
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Induction-recursion and initial algebras.
- Inductively generated formal topologies.
- Game semantics for dependent types
- Homotopy type theory in Lean
- Constructive hybrid games
- \( \pi\) with leftovers: a mechanisation in Agda
- Finitary higher inductive types in the groupoid model
- The construction of set-truncated higher inductive types
- The justification of identity elimination in Martin-Löf's type theory
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
- Pretopologies and a uniform presentation of sup-lattices, quantales and frames
- Indexed induction-recursion
- scientific article; zbMATH DE number 1670736 (Why is no real title available?)
- Canonicity of weak -groupoid laws using parametricity theory
- Proofs for free. Parametricity for dependent types
- Constructive membership predicates as index types
- scientific article; zbMATH DE number 4134038 (Why is no real title available?)
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Dialogues, reasons and endorsement
- scientific article; zbMATH DE number 4202427 (Why is no real title available?)
- The Lean theorem prover (system description)
- Algebra of Programming Using Dependent Types
- A pattern for almost compositional functions
- Hoare type theory, polymorphism and separation
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- Initial Algebra Semantics for Cyclic Sharing Structures
- Lexicographic Path Induction
- Algebra of programming in Agda: Dependent types for relational program derivation
- scientific article; zbMATH DE number 3985206 (Why is no real title available?)
- scientific article; zbMATH DE number 4096760 (Why is no real title available?)
- scientific article; zbMATH DE number 65535 (Why is no real title available?)
- Embeddability of ptykes
- scientific article; zbMATH DE number 1086681 (Why is no real title available?)
- Well-founded Relations in Type Theory
- scientific article; zbMATH DE number 2006633 (Why is no real title available?)
- scientific article; zbMATH DE number 2077110 (Why is no real title available?)
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
- scientific article; zbMATH DE number 883893 (Why is no real title available?)
- Constructing higher inductive types as groupoid quotients
- A syntax for higher inductive-inductive types
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- POPLMark reloaded: mechanizing proofs by logical relations
- Variations on inductive-recursive definitions
- Dependent Types at Work
- Signatures and induction principles for higher inductive-inductive types
- Eta-rules in Martin-Löf type theory
- Martin-Löf's type theory as an open-ended framework
- Calculating correct compilers
- Programming with ornaments
- Interactive programming in Agda -- objects and graphical user interfaces
- The essence of ornaments
- Idris, a general-purpose dependently typed programming language: Design and implementation
- Types for Proofs and Programs
- Containers, monads and induction recursion
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- Inductively defined types in the Calculus of Constructions
- Types for Proofs and Programs
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- Programming language semantics: It’s easy as 1,2,3
- A Comparison of Type Theory with Set Theory
- Infinite objects in type theory
- Builtin types viewed as inductive families
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- Topological quantum gates in homotopy type theory
- A syntax for mutual inductive families
- Refining constructive hybrid games
- Deep induction for inductive families
- On systems of definitions, induction and recursion
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- A two-level linear dependent type theory
- ProofViz: an interactive visual proof explorer
- A principled approach to programming with nested types in Haskell
- Propositional functions and families of types
This page was built for publication: Inductive families
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1336951)
