Inductive families
From MaRDI portal
Recommendations
Cites work
- 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?)
- 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
- 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
(71)- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- Dialogues, reasons and endorsement
- Initial Algebra Semantics for Cyclic Sharing Structures
- On systems of definitions, induction and recursion
- Type-theoretic interpretation of iterated, strictly positive inductive definitions
- ProofViz: an interactive visual proof explorer
- scientific article; zbMATH DE number 3985206 (Why is no real title available?)
- Dependent Types at Work
- Types for Proofs and Programs
- Finitary higher inductive types in the groupoid model
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- scientific article; zbMATH DE number 4134038 (Why is no real title available?)
- Lexicographic Path Induction
- scientific article; zbMATH DE number 4096760 (Why is no real title available?)
- scientific article; zbMATH DE number 65535 (Why is no real title available?)
- \( \pi\) with leftovers: a mechanisation in Agda
- Canonicity of weak -groupoid laws using parametricity theory
- Induction-recursion and initial algebras.
- Embeddability of ptykes
- Topological quantum gates in homotopy type theory
- scientific article; zbMATH DE number 7649955 (Why is no real title available?)
- A two-storied universe of transfinite mechanisms
- scientific article; zbMATH DE number 2077110 (Why is no real title available?)
- scientific article; zbMATH DE number 7168146 (Why is no real title available?)
- Game semantics for dependent types
- A UNIVERSE OF STRICTLY POSITIVE FAMILIES
- Indexed induction-recursion
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A Comparison of Type Theory with Set Theory
- The justification of identity elimination in Martin-Löf's type theory
- Constructing higher inductive types as groupoid quotients
- Algebra of Programming Using Dependent Types
- Programming language semantics: It’s easy as 1,2,3
- The construction of set-truncated higher inductive types
- The essence of ornaments
- Eta-rules in Martin-Löf type theory
- Order-sorted inductive types
- Inductively generated formal topologies.
- A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
- Inductively defined types in the Calculus of Constructions
- A pattern for almost compositional functions
- Idris, a general-purpose dependently typed programming language: Design and implementation
- A Brief Overview of Agda – A Functional Language with Dependent Types
- scientific article; zbMATH DE number 1670736 (Why is no real title available?)
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory
- A principled approach to programming with nested types in Haskell
- Programming with ornaments
- A compact kernel for the calculus of inductive constructions
- Interactive programming in Agda -- objects and graphical user interfaces
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Propositional functions and families of types
- Pretopologies and a uniform presentation of sup-lattices, quantales and frames
- Homotopy type theory in Lean
- POPLMark reloaded: mechanizing proofs by logical relations
- Proofs for free. Parametricity for dependent types
- Variations on inductive-recursive definitions
- A syntax for higher inductive-inductive types
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory
- Infinite objects in type theory
- Types for Proofs and Programs
- Containers, monads and induction recursion
- Constructive membership predicates as index types
- Builtin types viewed as inductive families
- Calculating correct compilers
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic
- The Lean theorem prover (system description)
- Algebra of programming in Agda: Dependent types for relational program derivation
- Martin-Löf's type theory as an open-ended framework
- scientific article; zbMATH DE number 2006633 (Why is no real title available?)
- Constructive hybrid games
- Hoare type theory, polymorphism and separation
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)
