About: Intuitionistic type theory

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

Alternative foundation of mathematics

Property	Value
dbo:description	alternative foundation of mathematics (en) теорія типів, яку розробив Пер Мартін-Леф (uk)
dbo:wikiPageExternalLink	http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ http://intuitionistic.files.wordpress.com/2010/07/martin-lof-tt.pdf%7Ctitle= http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html http://www.cs.chalmers.se/Cs/Research/Logic/book/ https://www.springer.com/philosophy/book/978-94-007-1735-0 http://math.ucr.edu/home/baez/ncat.def.html http://www.cse.chalmers.se/~peterd/papers/MartinL%C3%B6f1984.pdf
dbo:wikiPageWikiLink	dbc:Dependently_typed_programming dbr:Unit_type dbr:Category_theory dbr:Philosopher dbr:Per_Martin-Löf dbr:Integer dbr:Real_number dbr:First-order_logic dbr:Universal_quantification dbr:Principia_Mathematica dbr:Proof_assistant dbr:Proof_theory dbr:Type_theory dbr:Path_(topology) dbr:Typed_lambda_calculus dbc:Intuitionism dbc:Logic_in_computer_science dbr:Homotopy dbr:Epigram_(programming_language) dbr:Sweden dbr:Intensional_logic dbr:ATS_(programming_language) dbr:Reflexive_relation dbr:Disjoint_union dbr:Value_(computer_science) dbr:Impredicativity dbr:Ross_Street dbr:Coq dbr:Cartesian_product dbc:Constructivism_(mathematics) dbr:Intuitionistic_logic dbr:Extensionality dbr:Rational_number dbr:Jean-Yves_Girard dbr:Structural_induction dbc:Type_theory dbr:Negation dbr:Locally_cartesian_closed_category dbr:Boolean_Algebra dbr:Point_(geometry) dbr:Law_of_excluded_middle dbr:Undecidable_problem dbr:Successor_function dbc:Foundations_of_mathematics dbr:Mathematician dbr:Tuple dbr:Calculus_of_constructions dbr:Foundations_of_mathematics dbr:Homotopy_type_theory dbr:Record_(computer_science) dbr:Decision_problem dbr:Dependent_types dbr:Extensional_definition dbr:Setoid dbr:John_Baez dbr:Idris_(programming_language) dbr:Empty_type dbr:Cayenne_(programming_language) dbr:Predicate_logic dbr:Intensional_definition dbr:Programming_languages dbr:BHK_interpretation dbr:Girard's_paradox dbr:Mathematical_constructivism dbr:NuPRL dbr:Category_of_families dbr:Computational_type_theory dbr:R._A._G._Seely dbr:Agda_(theorem_prover) dbr:Existential_quantifier dbr:Fixpoint_combinator dbr:Predicativity dbr:Well-founded dbr:Curry–Howard_isomorphism dbr:Higher_inductive_type dbr:Impredicative dbr:Type_checking
dbp:wikiPageUsesTemplate	dbt:Foundations-footer dbt:Cite_book dbt:Main dbt:Reflist dbt:Further dbt:Non-classical_logic dbt:Tmath dbt:Short_description
dct:subject	dbc:Dependently_typed_programming dbc:Intuitionism dbc:Logic_in_computer_science dbc:Constructivism_(mathematics) dbc:Type_theory dbc:Foundations_of_mathematics
gold:hypernym	dbr:Theory
rdfs:label	Intuitionistic type theory (en) Teoria de tipus intuicionista (ca) Teoria dei tipi intuizionista (it) 直観主義型理論 (ja) Teoria dos tipos intuicionista (pt) Інтуїціоністська теорія типів (uk) Интуиционистская теория типов (ru) 直觉类型论 (zh)
owl:sameAs	freebase:Intuitionistic type theory wikidata:Intuitionistic type theory dbpedia-it:Intuitionistic type theory dbpedia-zh:Intuitionistic type theory dbpedia-ja:Intuitionistic type theory dbpedia-pt:Intuitionistic type theory dbpedia-ru:Intuitionistic type theory dbpedia-ca:Intuitionistic type theory dbpedia-uk:Intuitionistic type theory dbpedia-global:Intuitionistic type theory dbr:Intuitionistic type theory
prov:wasDerivedFrom	wikipedia-en:Intuitionistic_type_theory?oldid=1294075196&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Intuitionistic_type_theory
is dbo:knownFor of	dbr:Per_Martin-Löf
is dbo:wikiPageDisambiguates of	dbr:Type dbr:ITT
is dbo:wikiPageRedirects of	dbr:Extensional_type_theory dbr:Intensional_type_theory dbr:Martin-Löf_type_theory dbr:Martin-Löf_type_theory dbr:Martin-Loef's_type_theory dbr:Martin-Loef_Type_Theory dbr:Martin-Loef_type_theory dbr:Martin-Lof's_type_theory dbr:Martin-Lof_Type_Theory dbr:Martin-Lof_type_theory dbr:Martin-Löf's_type_theory dbr:Martin-Löf_Type_Theory dbr:Martin–Löf_type_theory dbr:Constructive_Type_Theory dbr:Constructive_type_theory dbr:Constructivist_type_theory dbr:Intuitionistic_Theory_of_Types dbr:Intuitionistic_Type_Theory dbr:Intuitionistic_theory_of_types dbr:Inductive_family
is dbo:wikiPageWikiLink of	dbr:Institute_for_Advanced_Study dbr:List_of_functional_programming_topics dbr:Induction-recursion dbr:Inductive_type dbr:Functional_programming dbr:Parametric_polymorphism dbr:Per_Martin-Löf dbr:Proof_theory dbr:Topos dbr:Type_theory dbr:Typed_lambda_calculus dbr:Escuela_Superior_Latinoamericana_de_Informática dbr:Epigram_(programming_language) dbr:Matita dbr:Impredicativity dbr:Proof-theoretic_semantics dbr:Type dbr:Coq dbr:Intuitionistic_logic dbr:Dependent_type dbr:ITT dbr:Truth_value dbr:Glossary_of_areas_of_mathematics dbr:Constructive_proof dbr:History_of_topos_theory dbr:History_of_type_theory dbr:Zipper_(data_structure) dbr:List_of_incomplete_proofs dbr:Mathematical_structure dbr:Higher-order_logic dbr:Anders_Martin-Löf dbr:List_of_mathematical_logic_topics dbr:Ordinal_collapsing_function dbr:Calculus_of_constructions dbr:Agda_(programming_language) dbr:Curry–Howard_correspondence dbr:Homotopy_type_theory dbr:Nuprl dbr:System_U dbr:Constructive_set_theory dbr:Polynomial_functor_(type_theory) dbr:Extensional_type_theory dbr:Intensional_type_theory dbr:Setoid dbr:Induction-induction dbr:Intuitionism dbr:Game_semantics dbr:Martin-Löf_type_theory dbr:Martin-Loef's_type_theory dbr:Martin-Loef_Type_Theory dbr:Martin-Loef_type_theory dbr:Martin-Lof's_type_theory dbr:Martin-Lof_Type_Theory dbr:Martin-Lof_type_theory dbr:Martin-Löf's_type_theory dbr:Martin-Löf_Type_Theory dbr:Martin–Löf_type_theory dbr:Constructive_Type_Theory dbr:Constructive_type_theory dbr:Constructivist_type_theory dbr:Intuitionistic_Theory_of_Types dbr:Intuitionistic_Type_Theory dbr:Intuitionistic_theory_of_types dbr:Inductive_family
is rdfs:seeAlso of	dbr:Per_Martin-Löf
is foaf:primaryTopic of	wikipedia-en:Intuitionistic_type_theory