{"id":"W4412989207","doi":"10.1145/3747511","title":"McTT: A Verified Kernel for a Proof Assistant","year":2025,"lang":"en","type":"article","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":1,"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":"Computer science; Kernel (algebra); Proof of concept; Burden of proof; Mathematics; Discrete mathematics; Operating system; Political science; Law","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0006972619,0.0002166952,0.0002997109,0.0001346893,0.00021942,0.0003101307,0.003381673,0.0001101597,0.000001177198],"category_scores_gemma":[0.001494875,0.0001404806,0.0002184211,0.0006624549,0.00009679072,0.0002030442,0.0008705829,0.0001622537,0.000002812594],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00005703403,"about_ca_system_score_gemma":0.00006983965,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003804775,"about_ca_topic_score_gemma":0.000005555338,"domain_scores_codex":[0.9984002,0.00001217223,0.0003481725,0.000482571,0.0003290444,0.0004278019],"domain_scores_gemma":[0.9984655,0.0001275695,0.0003133682,0.0007470052,0.0002928007,0.00005374647],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00006994128,0.0002809736,0.003441405,0.0007757818,0.000116603,0.000001452155,0.001928903,0.000001203543,0.005442155,0.7660164,0.003717904,0.2182073],"study_design_scores_gemma":[0.003731934,0.001709074,0.006598086,0.0006602278,0.0002305011,0.0000373912,0.003600255,0.00154265,0.4196543,0.262953,0.2980367,0.001245925],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.4902396,0.01190128,0.2855963,0.05842258,0.009204789,0.03149072,0.0000362603,0.006169325,0.1069392],"genre_scores_gemma":[0.9587749,0.000003182083,0.03784388,0.0002378068,0.00007710609,0.0004262811,0.000001081216,0.0000161771,0.002619567],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.5030634,"threshold_uncertainty_score":0.6284046,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01880341651926334,"score_gpt":0.2795932222139133,"score_spread":0.2607898056946499,"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."}}