{"id":"W2963472284","doi":"10.48550/arxiv.1507.08053","title":"A Case Study on Logical Relations using Contextual Types","year":2015,"lang":"en","type":"article","venue":"arXiv (Cornell University)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; ENCODE; Equivalence (formal languages); Computer science; Logical consequence; Operational semantics; Abstract syntax; Normalization (sociology); Theoretical computer science; Mathematics; Algebra over a field; Programming language; Semantics (computer science); Discrete mathematics; Artificial intelligence; Pure 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.02149908,0.0008613622,0.001225171,0.002821633,0.006499079,0.009546474,0.003642493,0.004569663,0.006319663],"category_scores_gemma":[0.04065463,0.001426838,0.002652767,0.003590362,0.0226516,0.02674562,0.01092078,0.008015603,0.001209042],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00496746,"about_ca_system_score_gemma":0.003520253,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.008513207,"about_ca_topic_score_gemma":0.006408185,"domain_scores_codex":[0.9725429,0.01800257,0.0009165297,0.002235686,0.004444156,0.0018581],"domain_scores_gemma":[0.9597037,0.03010099,0.0009387411,0.005960611,0.002489895,0.0008060739],"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.0000128113,0.00001114212,0.0001202955,0.00004166742,0.000004520638,0.0002128823,0.0006383052,0.0006897069,0.0001916257,0.9937537,0.0004552624,0.003868029],"study_design_scores_gemma":[0.00004173894,0.00004487986,0.0002570281,0.0001729717,0.00003136826,0.0008714421,0.001159204,0.008369012,0.003016633,0.9169675,0.06901692,0.00005125631],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02992693,0.00462581,0.8765494,0.01220877,0.000319331,0.0002013944,0.0001251544,0.001219361,0.07482383],"genre_scores_gemma":[0.5620241,0.003286399,0.4168352,0.001691493,0.000433054,0.0002775472,0.0001326979,0.0006912575,0.01462811],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.02149908,"threshold_uncertainty_score":0.1136994,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.2485314839957215,"score_gpt":0.2386818154406781,"score_spread":0.00984966855504335,"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."}}