About: Dependent type

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia-live.demo.openlinksw.com

Data type whose definition depends on a value

Property	Value
dbo:description	тип даних, який залежить від деякого значення (uk) olyan adattípus amelynek a definíciója egy értéktől függ (hu) data type whose definition depends on a value (en) datatype, hvis definition afhænger af en værdi (da) datový typ, jehož definice závisí na hodnotě (cs) type dont la définition dépend d'une valeur (fr)
dbo:wikiPageExternalLink	http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf http://sage.soe.ucsc.edu/ https://hbr.github.io/Lambda-Calculus/cc-tex https://web.archive.org/web/20120831123017/http:/sneezy.cs.nott.ac.uk/darcs/DTP08/ https://web.archive.org/web/20120901113229/http:/sneezy.cs.nott.ac.uk/darcs/dtp10/ https://www.cs.cmu.edu/afs/cs/Web/People/crary/819-f09/Martin-Lof80.pdf http://www.ada-auth.org/standards/ada12.html http://www.haskell.org/haskellwiki/Dependent_type http://www.cse.chalmers.se/research/group/logic/book/ http://www.cse.chalmers.se/~ulfn/papers/thesis.pdf https://www.cs.ru.nl/dtp11/ https://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf http://strictlypositive.org/view.ps.gz http://code.google.com/p/guru-lang/ https://strathprints.strath.ac.uk/76626/1/McBride_etal_amctmtxii2021_type_systems_for_programs_respecting_dimensions.pdf
dbo:wikiPageWikiLink	dbc:Dependently_typed_programming dbr:Predicate_(mathematical_logic) dbr:Proof-carrying_code dbr:System_F dbr:Program_extraction dbr:Proof_irrelevance dbr:Proof_term dbr:Logic_programming dbr:Oxford_University_Press dbr:Henk_Barendregt dbr:Polymorphism_(computer_science) dbr:Universe_(mathematics) dbr:F*_(programming_language) dbr:F_Sharp_(programming_language) dbr:Intuitionistic_type_theory dbr:Generalized_quantifier dbr:Universal_quantification dbr:Proof_assistant dbr:Codomain dbr:Propositional_calculus dbr:Type_system dbr:Type_theory dbr:If_and_only_if dbr:Dual_(category_theory) dbr:Typed_lambda_calculus dbr:Function_type dbr:Prototype_Verification_System dbr:Epigram_(programming_language) dbr:Matita dbr:Logic dbr:OCaml dbr:Combinatory_logic dbr:Nicolaas_Govert_de_Bruijn dbr:Dependent_ML dbr:ATS_(programming_language) dbr:Product_type dbr:Coq dbr:Cartesian_product dbr:Intuitionistic_logic dbr:C_(programming_language) dbr:Computer_science dbr:Haskell_Curry dbc:Type_theory dbr:Generic_programming dbr:Scheme_(programming_language) dbr:Ada_(programming_language) dbr:Model_theory dbr:Constructive_proof dbr:Pure_type_system dbr:Undecidable_problem dbr:Journal_of_Functional_Programming dbr:Twelf dbc:Foundations_of_mathematics dbr:William_Alvin_Howard dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Natural_number dbc:Type_systems dbr:Curry–Howard_correspondence dbr:Lambda_cube dbr:Kind_(type_theory) dbr:LF_(logical_framework) dbr:Lean_(proof_assistant) dbr:Purely_functional_programming dbr:Haskell_(programming_language) dbr:Calculus_of_inductive_constructions dbr:Subroutine dbr:Idris_(programming_language) dbr:Cayenne_(programming_language) dbr:Predicate_logic dbr:Program_verification dbr:NuPRL dbr:Agda_(theorem_prover) dbr:Termination_checking dbr:Tactic_(computer_science) dbr:Functional_programming_languages dbr:Real_numbers dbr:Type_checking
dbp:date	2020-11-09 (xsd:date)
dbp:id	dependent+product (en) dependent+product+type (en) dependent+sum (en) dependent+sum+type (en) dependent+type (en) dependent+type+theory (en)
dbp:title	dependent product (en) dependent product type (en) dependent sum (en) dependent sum type (en) dependent type (en) dependent type theory (en)
dbp:url	https://web.archive.org/web/20201109032232/http:/sage.soe.ucsc.edu/
dbp:wikiPageUsesTemplate	dbt:Some dbt:Foundations-footer dbt:Nlab dbt:Cite_book dbt:Reflist dbt:Notelist dbt:Math dbt:Anchor dbt:Cite_journal dbt:See_also dbt:No dbt:Dunno dbt:Refend dbt:Yes dbt:Any dbt:Refbegin dbt:Type_systems dbt:Mvar dbt:Cite_thesis dbt:Webarchive dbt:Efn dbt:Short_description
dct:subject	dbc:Dependently_typed_programming dbc:Type_theory dbc:Foundations_of_mathematics dbc:Type_systems
gold:hypernym	dbr:Type
rdf:type	owl:Thing owl:Thing
rdfs:label	Dependent type (en) Εξαρτώμενος τύπος (el) Závislostní typ (cs) Type dépendant (fr) 依存型 (ja) Зависимый тип (ru) Залежний тип (uk) 依赖类型 (zh)
rdfs:seeAlso	dbr:Proof_assistant
owl:sameAs	freebase:Dependent type wikidata:Dependent type dbpedia-fr:Dependent type dbpedia-zh:Dependent type dbpedia-ja:Dependent type dbpedia-ru:Dependent type dbpedia-el:Dependent type dbpedia-cs:Dependent type dbpedia-uk:Dependent type dbpedia-global:Dependent type dbr:Dependent type
prov:wasDerivedFrom	wikipedia-en:Dependent_type?oldid=1282903987&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Dependent_type
is dbo:wikiPageRedirects of	dbr:Dependently_typed_programming dbr:Dependent_types dbr:Dependent_types dbr:Dependent_typing dbr:Dependent_typing dbr:Sigma_type dbr:Dependent_type_theory dbr:Dependently-typed dbr:Dependently-typed_language dbr:Dependently-typed_programming_language dbr:Dependently_typed dbr:Dependently_typed_language dbr:Dependently_typed_programming_language dbr:Comparision_of_programming_languages_with_dependent_types dbr:Comparison_of_dependently_typed_programming_languages dbr:List_of_dependently-typed_programming_languages dbr:ΛΠ-calculus dbr:Type-level_programming
is dbo:wikiPageWikiLink of	dbr:Type_safety dbr:Inductive_type dbr:Index_of_philosophy_articles_(D–H) dbr:Functional_programming dbr:Clojure dbr:Universe_(mathematics) dbr:Cartesian_closed_category dbr:Per_Martin-Löf dbr:Haskell dbr:Proof_assistant dbr:Type_system dbr:Type_theory dbr:Function_type dbr:Fiber_bundle dbr:Epigram_(programming_language) dbr:Matita dbr:Turing_completeness dbr:Guru_(disambiguation) dbr:Groupoid dbr:Heyting_arithmetic dbr:Product_type dbr:Coq dbr:Dependently_typed_programming dbr:Metaprogramming dbr:Higher-order_logic dbr:Twelf dbr:Fibred_category dbr:Variable-length_array dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:Agda_(programming_language) dbr:Dimensional_analysis dbr:Dependency dbr:Curry–Howard_correspondence dbr:Aldor dbr:Lambda_cube dbr:Homotopy_type_theory dbr:Lean_(proof_assistant) dbr:Constructive_set_theory dbr:Container_(type_theory) dbr:Stephanie_Weirich dbr:Dependent_types dbr:Dependent_typing dbr:Idris_(programming_language) dbr:Intersection_type dbr:FriCAS dbr:Sigma_type dbr:Dependent_type_theory dbr:Dependently-typed dbr:Dependently-typed_language dbr:Dependently-typed_programming_language dbr:Dependently_typed dbr:Dependently_typed_language dbr:Dependently_typed_programming_language dbr:Comparision_of_programming_languages_with_dependent_types dbr:Comparison_of_dependently_typed_programming_languages dbr:List_of_dependently-typed_programming_languages dbr:ΛΠ-calculus dbr:Type-level_programming
is dbp:typing of	dbr:F*_(programming_language) dbr:Epigram_(programming_language) dbr:ATS_(programming_language) dbr:Agda_(programming_language) dbr:Futhark_(programming_language)
is rdfs:seeAlso of	dbr:Proof_assistant
is foaf:primaryTopic of	wikipedia-en:Dependent_type