The following pages link to Inductive families (Q1336951):
Displaying 50 items.
- Canonicity of weak \(\omega\)-groupoid laws using parametricity theory (Q283766) (← links)
- ProofViz: an interactive visual proof explorer (Q832103) (← links)
- A principled approach to programming with nested types in Haskell (Q848745) (← links)
- A compact kernel for the calculus of inductive constructions (Q1040007) (← links)
- A two-storied universe of transfinite mechanisms (Q1121881) (← links)
- Order-sorted inductive types (Q1286367) (← links)
- Representing inductively defined sets by wellorderings in Martin-Löf's type theory (Q1392287) (← links)
- Induction-recursion and initial algebras. (Q1412830) (← links)
- Inductively generated formal topologies. (Q1412832) (← links)
- Game semantics for dependent types (Q1641014) (← links)
- Homotopy type theory in Lean (Q1687770) (← links)
- Constructive hybrid games (Q2096468) (← links)
- \( \pi\) with leftovers: a mechanisation in Agda (Q2117018) (← links)
- Finitary higher inductive types in the groupoid model (Q2130587) (← links)
- The construction of set-truncated higher inductive types (Q2133178) (← links)
- The justification of identity elimination in Martin-Löf's type theory (Q2288279) (← links)
- Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory (Q2503336) (← links)
- Pretopologies and a uniform presentation of sup-lattices, quantales and frames (Q2575764) (← links)
- Indexed induction-recursion (Q2577476) (← links)
- Proofs for free (Q2844694) (← links)
- A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520) (← links)
- Dialogues, Reasons and Endorsement (Q3305643) (← links)
- The Lean Theorem Prover (System Description) (Q3454108) (← links)
- Algebra of Programming Using Dependent Types (Q3521992) (← links)
- A pattern for almost compositional functions (Q3546044) (← links)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- Initial Algebra Semantics for Cyclic Sharing Structures (Q3637190) (← links)
- Algebra of programming in Agda: Dependent types for relational program derivation (Q3644935) (← links)
- Embeddability of ptykes (Q4032649) (← links)
- A general formulation of simultaneous inductive-recursive definitions in type theory (Q4508246) (← links)
- (Q4989403) (← links)
- A Syntax for Higher Inductive-Inductive Types (Q4993350) (← links)
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs (Q5019018) (← links)
- POPLMark reloaded: Mechanizing proofs by logical relations (Q5110924) (← links)
- Variations on inductive-recursive definitions (Q5111280) (← links)
- Dependent Types at Work (Q5191088) (← links)
- (Q5216301) (← links)
- ETA-RULES IN MARTIN-LÖF TYPE THEORY (Q5240810) (← links)
- MARTIN-LÖF'S TYPE THEORY AS AN OPEN-ENDED FRAMEWORK (Q5249247) (← links)
- Calculating correct compilers (Q5371953) (← links)
- Programming with ornaments (Q5372000) (← links)
- Interactive programming in Agda – Objects and graphical user interfaces (Q5372002) (← links)
- The essence of ornaments (Q5372005) (← links)
- Idris, a general-purpose dependently typed programming language: Design and implementation (Q5398331) (← links)
- Containers, monads and induction recursion (Q5741557) (← links)
- (Q5875411) (← links)
- Typing with Leftovers - A mechanization of Intuitionistic Multiplicative-Additive Linear Logic (Q6060672) (← links)
- Programming language semantics: It’s easy as 1,2,3 (Q6065508) (← links)
- Builtin types viewed as inductive families (Q6535230) (← links)
- A comparison of HOL and ALF formalizations of a categorical coherence theorem (Q6567701) (← links)
