{"id":"W2297381814","doi":"","title":"Proof-term reconstruction from TSTP to Agda","year":2015,"lang":"en","type":"article","venue":"El Repositorio Institucional de la Universidad EAFIT (Universidad EAFIT)","topic":"Monetary Policy and Economic Impact","field":"Economics, Econometrics and Finance","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"","keywords":"Term (time); Computer science; Programming language; Calculus (dental)","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004532836,0.001065369,0.0009102009,0.001950224,0.0009481785,0.005834548,0.002457076,0.001478912,0.0476111],"category_scores_gemma":[0.02258147,0.001130082,0.00278231,0.001465856,0.001669914,0.005378986,0.005749098,0.00458384,0.01951637],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002093755,"about_ca_system_score_gemma":0.004488301,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002430933,"about_ca_topic_score_gemma":0.001761997,"domain_scores_codex":[0.9923967,0.002072797,0.0006924857,0.001370648,0.002659376,0.000808141],"domain_scores_gemma":[0.9870152,0.004469544,0.0003377699,0.004713627,0.003241772,0.0002219778],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"not_applicable","study_design_scores_codex":[0.0006932004,0.0001445647,0.0008915652,0.001149789,0.0001742873,0.0006441813,0.0006888111,0.02115968,0.008267559,0.6382409,0.04517342,0.282772],"study_design_scores_gemma":[0.0001679623,0.0001189722,0.0002595888,0.0003764311,0.0001962752,0.0006010048,0.000262383,0.09655708,0.03737459,0.646445,0.217566,0.00007469621],"study_design_candidate":"not_applicable","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.005526544,0.0004308619,0.9433926,0.001317039,0.0005822729,0.0002903786,0.003001143,0.02174284,0.02371634],"genre_scores_gemma":[0.2653218,0.0007567886,0.6859683,0.001135377,0.0004023738,0.0004836397,0.008419696,0.007836984,0.02967504],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.0476111,"threshold_uncertainty_score":0.1592749,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03474949518031224,"score_gpt":0.2299830591049088,"score_spread":0.1952335639245966,"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."}}