{"id":"W2102473097","doi":"10.1145/2503887.2503889","title":"First-class substitutions in contextual type theory","year":2013,"lang":"en","type":"article","venue":"","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":15,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"Javna Agencija za Raziskovalno Dejavnost RS","keywords":"Substitution (logic); Type theory; Class (philosophy); Typed lambda calculus; Normalization (sociology); Computer science; Dependent type; Elegance; Type (biology); Simply typed lambda calculus; Lambda calculus; Focus (optics); Algebra over a field; Mathematics; Programming language; Artificial intelligence; Pure mathematics; Epistemology; Sociology; Philosophy","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":["insufficient_payload"],"consensus_categories":[],"category_scores_codex":[0.0002192986,0.0000740952,0.00009501789,0.00005892673,0.00007072457,0.0001330655,0.0004219862,0.00005069666,0.0002384269],"category_scores_gemma":[0.00004942319,0.00005359093,0.00002761843,0.0002712852,0.0000527977,0.0003303897,0.00009007609,0.00007270832,0.002165443],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000295985,"about_ca_system_score_gemma":0.00004534896,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0009441383,"about_ca_topic_score_gemma":0.0006264431,"domain_scores_codex":[0.9993054,0.00005269878,0.0001423143,0.0001907126,0.000100435,0.0002084115],"domain_scores_gemma":[0.9994538,0.00008691665,0.00002763081,0.0003060497,0.0000678295,0.00005777933],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[7.249882e-7,0.0000295459,0.001467732,0.000003190728,0.000003633783,0.000003816576,0.0003090299,0.00001261859,0.00002065663,0.9922147,0.001647088,0.004287302],"study_design_scores_gemma":[0.001153985,0.0002899376,0.0406562,0.00001157376,0.000006096635,0.00004379773,0.0006959206,0.03458019,0.0003428304,0.6243299,0.2972173,0.0006723063],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.013465,0.0002567499,0.7953459,0.001109723,0.001096545,0.0004596121,1.341453e-7,0.0003352507,0.1879311],"genre_scores_gemma":[0.9931175,0.000004754521,0.001255476,0.0002556577,0.00003953028,0.00002811955,6.475232e-7,0.000002946425,0.005295359],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9796525,"threshold_uncertainty_score":0.9986115,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02510614264486484,"score_gpt":0.2396202704392124,"score_spread":0.2145141277943475,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}