About: Type theory

Property	Value
dbo:description	théorie mathématique (fr) formale Systeme als Alternativen zur axiomatischen Mengenlehre (de) concept in mathematical logic and computer science (en) teorie na pomezí matematiky, počítačové vědy a filosofie (cs) mõiste matemaatilises loogikas ja informaatikas (et) 수학자 버트런드 러셀이 제안한 유형 개념에서 파생한 이론 (ko)
dbo:wikiPageExternalLink	http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ http://www.cs.chalmers.se/Cs/Research/Logic/Types/tutorials.html https://hbr.github.io/Lambda-Calculus/cc-tex https://homotopytypetheory.org/book/ https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html http://lists.seas.upenn.edu/mailman/listinfo/types-list https://home.ttic.edu/~dreyer/course/papers/barendregt.pdf https://hott.github.io/HoTT-2019/images/mltt-rules.pdf https://www.cse.chalmers.se/research/group/logic/book/book.pdf https://plato.stanford.edu/entries/type-theory-intuitionistic/ https://ncatlab.org/nlab/show/type+theory http://www.cs.chalmers.se/Cs/Research/Logic/TypesSS05/program.html https://pure.tue.nl/ws/files/1383309/498552.pdf http://www.iwu.edu/~htiede/papers/pdf/jolli-review.pdf http://math.andrej.com/category/type-theory/ https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf https://www.cs.uoregon.edu/research/summerschool/archives.html https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html http://www.nuprl.org/book/Introduction_Type_Theory.html http://www.nuprl.org/documents/Constable/naive.pdf ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz https://www.youtube.com/watch%3Fv=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN https://ghostarchive.org/archive/20221009/http:/www.nuprl.org/documents/Constable/naive.pdf https://ghostarchive.org/archive/20221009/https:/pure.tue.nl/ws/files/1383309/498552.pdf https://www.researchgate.net/publication/277287583 http://citeseer.ist.psu.edu/cardelli97type.html http://plato.stanford.edu/entries/type-theory/
dbo:wikiPageWikiLink	dbr:Predicate_(mathematical_logic) dbr:System_F dbr:Induction-recursion dbr:Unit_type dbr:Parametricity dbr:Classical_logic dbr:Richard_Montague dbr:Isabelle_(proof_assistant) dbr:Category_theory dbr:Jon_Barwise dbr:Natural_deduction dbr:Uncountable_set dbr:Categorial_grammar dbr:Subtyping dbr:Lambda_calculus dbr:Compiler dbr:Dana_Scott dbr:Peano_axioms dbr:Universe_(mathematics) dbr:Rule_of_inference dbr:Cartesian_closed_category dbr:Intuitionistic_type_theory dbr:Per_Martin-Löf dbr:Generalized_quantifier dbr:Function_(mathematics) dbr:Real_number dbr:Set_theory dbr:Axiom_of_reducibility dbr:Bertrand_Russell dbr:First-order_logic dbr:Natural_language dbr:Russell's_paradox dbr:Universal_quantification dbr:Principia_Mathematica dbr:Program_synthesis dbr:Coinduction dbr:ST_type_theory dbr:Turnstile_(symbol) dbr:Type_constructor dbr:Type_inhabitation dbr:Recursive_language dbr:Automated_theorem_proving dbr:Proof_assistant dbr:Type_system dbr:Church_encoding dbr:Typed_lambda_calculus dbr:Formal_system dbr:Well-formed_formula dbr:Homotopy dbr:Naive_set_theory dbr:Normal_form_(abstract_rewriting) dbr:Set-builder_notation dbr:Prototype_Verification_System dbr:Matita dbr:Logic dbr:Mathematics dbr:Logical_conjunction dbr:Ordered_pair dbr:Set-theoretic_definition_of_natural_numbers dbr:Zermelo–Fraenkel_set_theory dbr:Algebraic_topology dbr:Static_program_analysis dbr:Combinatory_logic dbr:Computable_number dbr:Term_(logic) dbr:Brouwer–Heyting–Kolmogorov_interpretation dbr:Categorical_logic dbr:Product_type dbc:Hierarchy dbr:Formal_logic dbr:Coq dbr:Intuitionistic_logic dbr:Dependent_type dbr:Automath dbr:Montague_grammar dbr:Axiom dbr:Computer_science dbr:Alonzo_Church dbc:Type_theory dbr:Double_bind dbc:Systems_of_formal_logic dbr:Double_negation dbr:Thierry_Coquand dbr:Locally_cartesian_closed_category dbr:Or_(logic) dbr:Boolean_Logic dbr:Law_of_excluded_middle dbr:Mathematical_logic dbr:Julia_(programming_language) dbr:Substitution_(algebra) dbr:John_Lane_Bell dbr:Pure_type_system dbr:Naive_Set_Theory_(book) dbr:Material_conditional dbr:Transitive_property dbr:Judgment_(mathematical_logic) dbr:Mizar_system dbr:Higher-order_logic dbr:Rewriting dbr:Logic_for_Computable_Functions dbr:Logical_framework dbr:Twelf dbr:Boolean_logic dbr:Alfred_North_Whitehead dbr:Union_(set_theory) dbr:Existential_quantification dbr:Intersection dbr:Kleene–Rosser_paradox dbr:Calculus_of_constructions dbr:ML_(programming_language) dbr:Simply_typed_lambda_calculus dbr:Agda_(programming_language) dbr:Natural_number dbr:Axiom_of_choice dbr:Gregory_Bateson dbr:Indicator_function dbr:Paul_Halmos dbr:Curry–Howard_correspondence dbr:Foundations_of_mathematics dbr:Stanford_Encyclopedia_of_Philosophy dbr:Lambda_cube dbr:Homotopy_type_theory dbr:Pregroup_grammar dbr:LEGO_(proof_assistant) dbr:Structural_rule dbr:System_U dbr:Decision_problem dbr:Lean_(proof_assistant) dbr:Reflection_principle dbr:Mogensen–Scott_encoding dbr:Constructive_mathematics dbr:Structural_recursion dbr:Semantic_analysis_(compilers) dbr:Induction-induction dbr:Dependent_typing dbr:Automated_proof_checking dbr:Axiom_of_Choice dbr:Metavariable dbr:Empty_type dbr:HOL_(proof_assistant) dbr:Identity_type dbr:Peano_arithmetic dbr:Formal_semantics_(linguistics) dbr:Strongly_normalizing dbr:BHK_interpretation dbr:Sum_type dbr:Martin-Löf_type_theory dbr:Girard's_paradox dbr:Not_(logic) dbr:NuPRL dbr:Cubical_type_theory dbr:Constructivism_(mathematics) dbr:And_(logic) dbr:Martin-Löf dbr:Call/cc dbr:Church-Rosser_theorem dbr:Curry–Howard_isomorphism dbr:Reflexivity_property dbr:Categorical_semantics dbr:Countably_infinite dbr:Lambek dbr:Logical_or dbr:Symmetric_property dbr:C-monoid dbr:Canonicity_(type_theory) dbr:Logical_levels dbr:Nlab:cubical+type+theory dbr:Truth-value dbr:Propositions
dbp:bot	medic (en)
dbp:curator	Robert L. Constable (en)
dbp:date	May 2025 (en)
dbp:title	Computational type theory (en)
dbp:urlname	Computational_type_theory (en)
dbp:wikiPageUsesTemplate	dbt:Cite_book dbt:Cite_web dbt:Main dbt:Reflist dbt:Notelist dbt:Redirect dbt:Anchor dbt:Expand_section dbt:Dead_link dbt:Refend dbt:Computer_science dbt:Cbignore dbt:Refbegin dbt:Cite_encyclopedia dbt:Formal_semantics dbt:Cite_thesis dbt:Scholarpedia dbt:Section_link dbt:Mathematical_logic dbt:Cn dbt:Rp dbt:Webarchive dbt:Efn dbt:Short_description
dct:subject	dbc:Hierarchy dbc:Type_theory dbc:Systems_of_formal_logic
rdfs:label	Type theory (en) نظرية النمط (ar) Logika vyššího řádu (cs) Teorie typů (cs) Θεωρία τύπων (el) Λογική ανώτερου βαθμού (el) Teorio de tipoj (eo) Logiko de supera ordo (eo) Teoría de tipos (es) Logik höherer Stufe (de) Typentheorie (de) Logique d'ordre supérieur (fr) Théorie des types (fr) Teoria dei tipi (it) 型理論 (ja) 高階述語論理 (ja) 고차 논리 (ko) 유형 이론 (ko) Typetheorie (nl) Teoria typów (pl) Teoria dos tipos (pt) Lógica de ordem superior (pt) Логика высшего порядка (ru) Теория типов (ru) Теорія типів (uk) 高阶逻辑 (zh) 类型论 (zh)
owl:sameAs	dbpedia-fr:Type theory freebase:Type theory yago-res:Type theory wikidata:Type theory wikidata:Type theory dbpedia-it:Type theory dbpedia-nl:Type theory dbpedia-de:Type theory dbpedia-de:Type theory dbpedia-fr:Type theory dbpedia-zh:Type theory dbpedia-zh:Type theory dbpedia-ja:Type theory dbpedia-ja:Type theory dbpedia-pt:Type theory dbpedia-pt:Type theory dbpedia-he:Type theory dbpedia-es:Type theory dbpedia-fa:Type theory dbpedia-ru:Type theory dbpedia-ru:Type theory dbpedia-vi:Type theory dbpedia-pl:Type theory dbpedia-ko:Type theory dbpedia-ko:Type theory dbpedia-el:Type theory dbpedia-el:Type theory dbpedia-ar:Type theory dbpedia-az:Type theory dbpedia-cs:Type theory dbpedia-cs:Type theory dbpedia-eo:Type theory dbpedia-eo:Type theory dbpedia-kk:Type theory dbpedia-no:Type theory dbpedia-uk:Type theory dbpedia-global:Type theory dbr:Type theory
prov:wasDerivedFrom	wikipedia-en:Type_theory?oldid=1292581294&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Type_theory
is dbo:academicDiscipline of	dbr:Thierry_Coquand dbr:J._Roger_Hindley dbr:Conor_McBride dbr:Thorsten_Altenkirch
is dbo:knownFor of	dbr:Steve_Awodey dbr:Robert_Harper_(computer_scientist)
is dbo:notableIdea of	dbr:Bertrand_Russell
is dbo:wikiPageDisambiguates of	dbr:Type
is dbo:wikiPageRedirects of	dbr:Type_(type_theory) dbr:Equality_type dbr:Elementary_Theory_of_the_Category_of_Sets dbr:Theory_of_Logical_Types dbr:Theory_of_Types dbr:Theory_of_types dbr:Natural_language_semantics_and_type_theory dbr:Applications_of_type_theory dbr:List_of_type_theories dbr:Logical_type dbr:System_of_types dbr:Type-theoretic dbr:Type_(mathematics) dbr:Type_Theory dbr:Typed_logic dbr:Propositional_equality dbr:Universe_type dbr:Universe_types
is dbo:wikiPageWikiLink of	dbr:Type_variable dbr:Type_safety dbr:Currying dbr:Inductive_type dbr:Unit_type dbr:Mariangiola_Dezani-Ciancaglini dbr:Finite_set dbr:Isabelle_(proof_assistant) dbr:Category_theory dbr:Fixed_point_(mathematics) dbr:First-class_function dbr:Enumerated_type dbr:Monad_(category_theory) dbr:Natural_deduction dbr:Henk_Barendregt dbr:Outline_of_philosophy dbr:Parametric_polymorphism dbr:Polymorphism_(computer_science) dbr:Subtyping dbr:Peano_axioms dbr:Nyaya dbr:Universe_(mathematics) dbr:New_Foundations dbr:Cantor's_diagonal_argument dbr:Up_tack dbr:Focus_(linguistics) dbr:Formal_methods dbr:Intuitionistic_type_theory dbr:Generalized_quantifier dbr:Mu_(letter) dbr:Axiom_of_reducibility dbr:Bertrand_Russell dbr:First-order_logic dbr:Russell's_paradox dbr:Array_(data_type) dbr:Cardinal_number dbr:Steve_Awodey dbr:ST_type_theory dbr:Paris_Kanellakis dbr:Type_constructor dbr:Type_inhabitation dbr:Typing_environment dbr:Typing_rule dbr:Leon_Henkin dbr:Decidability_(logic) dbr:Hindley–Milner_type_system dbr:Proof_theory dbr:Type_system dbr:Axiom_schema_of_replacement dbr:Type_(type_theory) dbr:Heyting_algebra dbr:Michael_Makkai dbr:Bar_recursion dbr:Partial_equivalence_relation dbr:Link_grammar dbr:Timeline_of_category_theory_and_related_mathematics dbr:Personality_psychology dbr:Colon_(punctuation) dbr:Willard_Van_Orman_Quine dbr:Product_(mathematics) dbr:OpenCog dbr:Refinement_(computing) dbr:Mathematics dbr:Logical_positivism dbr:Ordered_pair dbr:Ordinal_number dbr:Set-theoretic_definition_of_natural_numbers dbr:Parameter_(computer_programming) dbr:Domain_theory dbr:Index_of_philosophy_articles_(R–Z) dbr:Information_flow_(information_theory) dbr:Abstract_data_type dbr:Algebraic_data_type dbr:Liskov_substitution_principle dbr:Gordon_Plotkin dbr:Gérard_Huet dbr:Denotational_semantics dbr:Class_logic dbr:Top_type dbr:Categorical_logic dbr:Categorical_quantum_mechanics dbr:Categories_(Peirce) dbr:Index_of_logic_articles dbr:Outline_of_software_engineering dbr:Primitive_recursive_functional dbr:Principal_type dbr:Product_type dbr:Euclidean_geometry dbr:Programming_language dbr:Truth dbr:Type dbr:Coq dbr:Data_type dbr:Type–token_distinction dbr:Structure_(mathematical_logic) dbr:Extensionality dbr:Dependent_type dbr:Theoretical_computer_science dbr:Recursive_data_type dbr:European_Summer_School_in_Logic,_Language_and_Information dbr:HOL_Light dbr:Coherent_space dbr:De_Bruijn_notation dbr:Laboratory_for_Foundations_of_Computer_Science dbr:Computer_science dbr:List_of_mathematical_theories dbr:Theory dbr:Vertical_bar dbr:List_of_pioneers_in_computer_science dbr:Semantics_(computer_science) dbr:Contradiction dbr:Partition_of_a_set dbr:Intersection_(set_theory) dbr:Truth_value dbr:Alfred_Tarski dbr:Outline_of_mathematics dbr:Equality_type dbr:Mathematical_logic dbr:P-complete dbr:Glossary_of_areas_of_mathematics dbr:Harry_Mairson dbr:History_of_topos_theory dbr:History_of_type_theory dbr:John_Lane_Bell dbr:Stream_(abstract_data_type) dbr:Pure_type_system dbr:NLab dbr:Axiom_of_regularity dbr:Outline_of_academic_disciplines dbr:Judgment_(mathematical_logic) dbr:Container_(abstract_data_type) dbr:Higher-order_logic dbr:Urelement dbr:Scott–Potter_set_theory dbr:Bounded_quantification dbr:Bounded_quantifier dbr:List_of_mathematical_logic_topics dbr:Logical_framework dbr:Robert_Harper_(computer_scientist) dbr:Subject_reduction dbr:Tagged_union dbr:Tee_(symbol) dbr:Tuple dbr:Union_type dbr:Set_(abstract_data_type) dbr:Constructivism_(philosophy_of_mathematics) dbr:Glossary_of_computer_science dbr:British_Colloquium_for_Theoretical_Computer_Science dbr:Cardinal_assignment dbr:Fibred_category dbr:J._Roger_Hindley dbr:Generalizations_of_the_derivative dbr:Head-driven_phrase_structure_grammar dbr:Calculus_of_constructions dbr:Simply_typed_lambda_calculus dbr:List_of_atheists_in_science_and_technology dbr:Second-order_propositional_logic dbr:Type_shifter dbr:List_(abstract_data_type) dbr:Axiom_of_choice dbr:Predicate_transformer_semantics dbr:Frank_Ramsey_(mathematician) dbr:Gregory_Bateson dbr:Option_type dbr:Axiom_schema_of_specification dbr:Curry–Howard_correspondence dbr:Second-order_logic dbr:Lambda_cube dbr:Bunched_logic dbr:List_of_programming_language_researchers dbr:Ludics dbr:Richard_Statman dbr:Situation_theory dbr:Bottom_type dbr:Existence_theorem dbr:Programming_language_theory dbr:Philip_Wadler dbr:Garbage_(computer_science) dbr:Kind_(type_theory) dbr:Natural_numbers_object dbr:List_of_types_of_functions dbr:System_U dbr:Ramification dbr:Intersective_modifier dbr:Record_(computer_science) dbr:Lean_(proof_assistant) dbr:Association_for_Logic,_Language_and_Information dbr:Computational_logic dbr:Conor_McBride dbr:Constructive_set_theory dbr:Container_(type_theory) dbr:Luca_Cardelli dbr:Polynomial_functor_(type_theory) dbr:Ambient_calculus dbr:Baby_Modula-3 dbr:Refinement_type dbr:Stephanie_Weirich dbr:Hereditarily_finite_set dbr:Learning_cycle dbr:Quine's_paradox dbr:Frank_Pfenning dbr:List_of_academic_fields dbr:Elementary_Theory_of_the_Category_of_Sets dbr:Outline_of_computer_science dbr:Outline_of_logic dbr:Universal_type dbr:Row_polymorphism dbr:Type_theory_with_records dbr:FO(.) dbr:Equivalent_definitions_of_mathematical_structures dbr:Valeria_de_Paiva dbr:Alternative_set_theory dbr:David_Spivak dbr:Tree_(data_structure) dbr:Glossary_of_Principia_Mathematica dbr:Collection_(abstract_data_type) dbr:Metavariable dbr:Thorsten_Altenkirch dbr:Empty_type dbr:Barbara_Liskov dbr:Intersection_type dbr:Intersection_type_discipline dbr:List_object dbr:Alternative_semantics dbr:Responsive_predicate dbr:Session_type dbr:Hyperarithmetical_theory dbr:Quotient_type dbr:Extensions_of_First_Order_Logic dbr:Identity_type dbr:Outline_of_formal_science dbr:Theory_of_Logical_Types dbr:Theory_of_Types dbr:Theory_of_types dbr:Natural_language_semantics_and_type_theory dbr:Applications_of_type_theory dbr:List_of_type_theories dbr:Logical_type dbr:System_of_types dbr:Type-theoretic dbr:Type_(mathematics) dbr:Type_Theory dbr:Typed_logic dbr:Propositional_equality dbr:Universe_type dbr:Universe_types
is dbp:field of	dbr:J._Roger_Hindley
is dbp:fields of	dbr:Conor_McBride dbr:Thorsten_Altenkirch
is dbp:notableIdeas of	dbr:Bertrand_Russell
is dbp:subDiscipline of	dbr:Peter_B._Andrews dbr:Gary_T._Leavens
is foaf:primaryTopic of	wikipedia-en:Type_theory