About: Simply typed lambda calculus

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

Formal system in mathematical logic

Property	Value
dbo:description	formal system in mathematical logic (en) sistema formal en lógica matemática (es) variante du lambda-calcul avec des types (fr)
dbo:wikiPageExternalLink	http://www.lfcs.inf.ed.ac.uk/reports/98/ECS-LFCS-98-381/ ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps
dbo:wikiPageWikiLink	dbr:Type_safety dbr:Currying dbr:System_F dbr:Normalisation_by_evaluation dbr:Evaluation_strategy dbr:Coproduct dbr:Natural_deduction dbr:Morphism dbr:Parametric_polymorphism dbc:Lambda_calculus dbr:Lambda_calculus dbr:Recursion dbr:Untyped_lambda_calculus dbr:Joachim_Lambek dbr:Minimal_logic dbr:Set_theory dbr:Set_(mathematics) dbr:Fixed-point_combinator dbr:Type_constructor dbr:Type_erasure dbr:Type_inhabitation dbr:Typing_environment dbr:Typing_rule dbr:Decidability_(logic) dbr:Type_system dbr:Topos dbr:Type_theory dbr:Church_encoding dbr:Typed_lambda_calculus dbr:Function_type dbr:Dialectica_interpretation dbr:Function_space dbr:Category_of_sets dbr:Backus–Naur_form dbr:Tautology_(logic) dbr:Combinatory_logic dbr:Equivalence_class dbr:Completeness_(logic) dbr:Principal_type dbr:Cartesian_product dbr:Intuitionistic_logic dbr:Dependent_type dbr:Closed_monoidal_category dbr:Alonzo_Church dbc:Type_theory dbr:Polynomial dbr:Functor dbr:Operational_semantics dbr:Apply dbc:Theory_of_computation dbr:Product_(category_theory) dbr:Simply_typed_lambda_calculus dbr:Natural_number dbr:Type_inference dbr:Grzegorczyk_hierarchy dbr:LF_(logical_framework) dbr:Beta_reduction dbr:Hindley–Milner_type_inference dbr:Equational_theory dbr:Call_by_value dbr:Linear_type_system dbr:Elementary_recursive dbr:Strong_normalization dbr:Turing_complete dbr:Final_object dbr:Call_by_name dbr:Church_numeral dbr:Curry–Howard_isomorphism dbr:Internal_language dbr:Recursive_type dbr:Unification_(computing) dbr:Cartesian_closed_categories dbr:Eta_reduction dbr:Normalization_property_(lambda-calculus) dbr:Object_(category_theory) dbr:Programming_language_for_Computable_Functions
dbp:bot	medic (en)
dbp:date	May 2025 (en)
dbp:wikiPageUsesTemplate	dbt:Cite_web dbt:Reflist dbt:Notelist dbt:Cite_journal dbt:Dead_link dbt:Alonzo_Church dbt:R dbt:ISBN dbt:Cbignore dbt:Mono dbt:SEP dbt:Efn dbt:Tmath dbt:Short_description
dct:subject	dbc:Lambda_calculus dbc:Type_theory dbc:Theory_of_computation
rdfs:label	Simply typed lambda calculus (en) Λ-λογισμός με απλούς τύπους (el) Cálculo lambda simplemente tipado (es) Cálculo lambda simplesmente tipado (pt) Просто типизированное лямбда-исчисление (ru) 简单类型λ演算 (zh)
owl:sameAs	freebase:Simply typed lambda calculus wikidata:Simply typed lambda calculus dbpedia-zh:Simply typed lambda calculus dbpedia-pt:Simply typed lambda calculus dbpedia-es:Simply typed lambda calculus dbpedia-ru:Simply typed lambda calculus dbpedia-el:Simply typed lambda calculus dbpedia-global:Simply typed lambda calculus
prov:wasDerivedFrom	wikipedia-en:Simply_typed_lambda_calculus?oldid=1292509057&ns=0
foaf:isPrimaryTopicOf	wikipedia-en:Simply_typed_lambda_calculus
is dbo:knownFor of	dbr:Alonzo_Church
is dbo:wikiPageDisambiguates of	dbr:STLC
is dbo:wikiPageRedirects of	dbr:Simply-typed_lambda_calculus dbr:Bidirectional_type_checking dbr:Λ→ dbr:Simply_typed_lambda dbr:Simply_typed_lambda-calculus dbr:Simply_typed_λ-calculus dbr:Simply_typed_λ_calculus
is dbo:wikiPageWikiLink of	dbr:Currying dbr:System_F dbr:Nominal_terms_(computer_science) dbr:Normalisation_by_evaluation dbr:Church–Rosser_theorem dbr:First-class_function dbr:Categorial_grammar dbr:Subtyping dbr:Lambda_calculus dbr:Joachim_Lambek dbr:Cartesian_closed_category dbr:Markov's_principle dbr:Minimal_logic dbr:Fixed-point_combinator dbr:STLC dbr:Type_constructor dbr:Type_inhabitation dbr:Typing_rule dbr:Hindley–Milner_type_system dbr:Type_theory dbr:Typed_lambda_calculus dbr:Function_type dbr:Curry's_paradox dbr:Normal_form_(abstract_rewriting) dbr:Turing_completeness dbr:Gérard_Huet dbr:Categorical_logic dbr:Greek_letters_used_in_mathematics,_science,_and_engineering dbr:Primitive_recursive_functional dbr:Dependent_type dbr:Alonzo_Church dbr:History_of_type_theory dbr:Pure_type_system dbr:Q0_(mathematical_logic) dbr:Judgment_(mathematical_logic) dbr:Apply dbr:List_of_mathematical_logic_topics dbr:Substructural_type_system dbr:POPLmark_challenge dbr:Tuple dbr:William_Alvin_Howard dbr:Simply_typed_lambda_calculus dbr:Type_inference dbr:Eval dbr:Curry–Howard_correspondence dbr:Lambda_cube dbr:Hom_functor dbr:Meta-circular_evaluator dbr:Richard_Statman dbr:Generalized_algebraic_data_type dbr:Kind_(type_theory) dbr:Robert_Feys dbr:Intersection_type_discipline dbr:Simply-typed_lambda_calculus dbr:Bidirectional_type_checking dbr:Λ→ dbr:Simply_typed_lambda dbr:Simply_typed_lambda-calculus dbr:Simply_typed_λ-calculus dbr:Simply_typed_λ_calculus
is dbp:knownFor of	dbr:Alonzo_Church
is foaf:primaryTopic of	wikipedia-en:Simply_typed_lambda_calculus