{"id":"W3181123080","doi":"10.1007/978-3-030-79876-5_38","title":"Harpoon: Mechanizing Metatheory Interactively","year":2021,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"Fonds de recherche du Québec – Nature et technologies; Natural Sciences and Engineering Research Council of Canada","keywords":"Mathematical proof; Assertion; Computer science; Normalization (sociology); Programming language; Metatheory; Representation (politics); Set (abstract data type); Proof of concept; Theoretical computer science; Mathematics","routes":{"ca_aff":true,"ca_fund":true,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003392802,0.0007245282,0.0005577634,0.001530451,0.0009213832,0.002702471,0.002367796,0.0007269044,0.01583023],"category_scores_gemma":[0.008827861,0.0009567054,0.001255975,0.0005934688,0.003342462,0.004846428,0.005067186,0.003003135,0.00288629],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001565195,"about_ca_system_score_gemma":0.002052724,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003072675,"about_ca_topic_score_gemma":0.005294906,"domain_scores_codex":[0.996662,0.001368403,0.0001153824,0.0003644268,0.001208475,0.0002814303],"domain_scores_gemma":[0.9951381,0.003349541,0.0001324314,0.000821802,0.0004319043,0.000126293],"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.0001620592,0.0001225683,0.0005507644,0.0005128819,0.00005891598,0.0003713824,0.001134493,0.01314279,0.01339401,0.8104705,0.03320999,0.1268696],"study_design_scores_gemma":[0.0001826871,0.0001116373,0.0005007118,0.0003900191,0.0001036341,0.000693861,0.0002930872,0.1715256,0.0607163,0.5053737,0.2599712,0.0001376482],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01379523,0.0003771676,0.9275494,0.001017997,0.0002671682,0.000148352,0.0002051671,0.01731002,0.0393296],"genre_scores_gemma":[0.3768823,0.0006811764,0.58688,0.001385494,0.0001820405,0.0002723838,0.0005884927,0.00453649,0.02859162],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01583023,"threshold_uncertainty_score":0.05295736,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0282621557546542,"score_gpt":0.2531520141780269,"score_spread":0.2248898584233727,"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."}}