Tag: dependent-type
Found 74 results for 'dependent-type'.
1) type-theory - What is the role of the Bicolored Calculus of Constructions?
2) type-theory - Explicit set of types and terms in MLTT
3) reference-request - Type theory and fixed points of datatypes
4) type-theory - Church-Rosser property for dependently typed lambda calculus?
5) type-theory - Why it's impossible to declare an induction principle for Church numerals
6) pl.programming-languages - Lack of atomic propositions in the Calculus of Constructions from ATTAPL textbook
7) type-theory - Strong Normalization of Extended Calculus of Constructions (CC with cumulative universes)
8) lo.logic - Rules about Prop and Set in UTT
9) type-theory - Dependent types over Church-encoded type in PTS/CoC
10) pl.programming-languages - What are the pros and cons for type cases in dependent type theories?
11) lo.logic - Example of where violation of strict positivity condition in inductive types leads to inconsistency
12) lo.logic - What's the difference between ADTs, GADTs, and inductive types?
13) lo.logic - Well-formedness condition for inductive types
14) lo.logic - What does consistency mean for "computational theories" corresponding to inductive types?
15) type-theory - Rendering of type-level computation
16) lo.logic - Good description of Calculus of Inductive Construction
17) reference-request - PHOAS with extrinsic typing?
18) type-theory - Formalizing the theory of finite sets in type theory
19) type-theory - Is there a way to define dependent types without explicit substitutions internally within agda?
20) lo.logic - Dependent C-style types with subtyping rule
21) type-systems - Is compiler for dependent type much harder than an intepreter?
22) reference-request - Modeling objects (OOP) in dependent type theory
23) type-theory - Relating univalence for a theory of cateogries to the skeleton concept
24) type-theory - $\mathbb{N}$ in intensional MLTT with judgmentally commutative $+$ and $\times$
25) pl.programming-languages - Constraint types (IBM/X10) compared to dependent types
26) type-theory - Is it possible to verify a typechecker for a total dependently-typed language in that language's logic?
27) reference-request - Proof techniques for showing that dependent type checking is decidable
28) type-theory - Fixed points in dependent type theories
29) type-theory - How do we use directed univalence in directed type theory?
30) reference-request - Intuition Behind Strict Positivity?
31) dependent-type - References on implementing universe levels over MLTT?
32) dependent-type - NBE for MiniTT: Why is labelled sum eliminator both a normal form and a neutral value?
33) lo.logic - Implications of the rule of cumulativity in the Calculus of Constructions
34) dependent-type - Motivation for Dependent Type
35) coq - Why an infinite type hierarchy?
36) reference-request - Reference for the fact that (0=1) implies false requires a universe in MLTT
37) dependent-type - Dependent Types and Compile Time Types
38) type-theory - Effect of HoTT/Univalence Axiom on equality between terms of inductive types?
39) type-theory - Defining finite sets inductively in a proof assistant?
40) type-theory - What's the categorical semantics of definitional equality?
41) pl.programming-languages - Relationship between contracts and dependent typing
42) type-theory - In the Hott book, are the most of the type formers redundant? And if so, why?
43) dependent-type - Impredicativity + large eliminations (with no excluded middle) in Coq
44) dependent-type - Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?
45) type-theory - Is there a theory of overloading types?
46) lo.logic - How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?
47) type-theory - Dependent Sums and Products
48) type-theory - Defining binary natural numbers without quotient types
49) type-theory - Examples of Universe inconsistency in normal use of dependent types
50) reference-request - Intuition behind nested positivity and counterexamples