{"id":"W4379536897","doi":"10.1145/3591286","title":"Extensible Metatheory Mechanization via Family Polymorphism","year":2023,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Metatheory; Programming language; Mathematical proof; Computer science; Extensibility; Proof assistant; Software engineering; Theoretical computer science; Mathematics","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":[],"consensus_categories":[],"category_scores_codex":[0.001005125,0.0002188973,0.0002643624,0.0002435796,0.000222961,0.0002298214,0.002921565,0.0001034521,0.000003313603],"category_scores_gemma":[0.0008349644,0.0001472357,0.0001581592,0.001658279,0.00007864784,0.0003465013,0.001160157,0.000169111,0.00008598305],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0000312651,"about_ca_system_score_gemma":0.00002661061,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006846055,"about_ca_topic_score_gemma":0.000001625873,"domain_scores_codex":[0.9981866,0.00002440123,0.0003133699,0.0004648371,0.0005536149,0.0004572103],"domain_scores_gemma":[0.9984832,0.00009279674,0.0003262104,0.0007562063,0.0002656527,0.00007591542],"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":[0.00001460692,0.0001229818,0.001308462,0.0001828334,0.00008527425,0.000008998447,0.003075272,0.000006983065,0.05940446,0.6627127,0.002243907,0.2708335],"study_design_scores_gemma":[0.00145492,0.00107203,0.00839379,0.0001858662,0.0001680703,0.0001315375,0.006013541,0.003749072,0.357953,0.5908676,0.0286076,0.001402957],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.8387047,0.004664959,0.1005377,0.01319865,0.005578169,0.005913936,0.000007043716,0.01083652,0.02055831],"genre_scores_gemma":[0.9857851,0.00001740862,0.01241848,0.0002331608,0.0001211653,0.00007553163,0.000002547851,0.00003146922,0.001315125],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.2985485,"threshold_uncertainty_score":0.6004099,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02153602823069928,"score_gpt":0.2567209835178066,"score_spread":0.2351849552871074,"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."}}