{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003731664,0.0008604688,0.0008015828,0.001232632,0.0007654444,0.003257231,0.003782939,0.001686011,0.01464811],"category_scores_gemma":[0.01895695,0.001434228,0.002568784,0.0006465215,0.002341482,0.00504596,0.004940073,0.003670862,0.0076224],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001646383,"about_ca_system_score_gemma":0.00415404,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002205333,"about_ca_topic_score_gemma":0.001387671,"domain_scores_codex":[0.9944958,0.0009908447,0.0006549727,0.0009675776,0.002466026,0.0004247784],"domain_scores_gemma":[0.9913346,0.003362586,0.0005773035,0.002954954,0.00149007,0.0002805326],"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.0008738101,0.0003614643,0.003618813,0.002017153,0.0003077113,0.001420179,0.00137356,0.03895302,0.05525771,0.5295151,0.04570326,0.3205982],"study_design_scores_gemma":[0.0005545289,0.000405508,0.0008165008,0.0005897182,0.0002981765,0.001839091,0.0001338325,0.3661094,0.11142,0.2140651,0.3035025,0.0002656971],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.001988845,0.00009203632,0.9702442,0.0001586923,0.00008554594,0.0001228488,0.0002627844,0.02537794,0.001667166],"genre_scores_gemma":[0.1163361,0.0002528303,0.8654783,0.0004679887,0.0001402737,0.0005071016,0.001396695,0.008677332,0.006743414],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01464811,"threshold_uncertainty_score":0,"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."}}