{"id":"W2216433683","doi":"10.4204/eptcs.185.3","title":"A Case Study on Logical Relations using Contextual Types","year":2015,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"McGill University","funders":"","keywords":"Mathematical proof; ENCODE; Equivalence (formal languages); Operational semantics; Computer science; Abstract syntax; Normalization (sociology); Logical consequence; Exploit; Logical equivalence; Theoretical computer science; Mathematics; Algebra over a field; Programming language; Semantics (computer science); Discrete mathematics; Pure mathematics; Artificial intelligence","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.01940678,0.0008790026,0.001220331,0.002754423,0.006411293,0.009504535,0.003573134,0.00469971,0.006416063],"category_scores_gemma":[0.03809096,0.00135836,0.002552812,0.003442161,0.02205464,0.02601925,0.01055217,0.007569364,0.001235718],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.004805443,"about_ca_system_score_gemma":0.003506856,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.008340584,"about_ca_topic_score_gemma":0.006142626,"domain_scores_codex":[0.9744613,0.01651506,0.0008291379,0.002074148,0.004280606,0.00183977],"domain_scores_gemma":[0.9645644,0.02624919,0.0008546136,0.005299625,0.002276878,0.000755253],"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.000012978,0.00001046617,0.000111748,0.00003918229,0.000004168736,0.0002292069,0.0006254942,0.0006578971,0.0001883435,0.9940439,0.0004164051,0.003660272],"study_design_scores_gemma":[0.00004171313,0.00004670411,0.0002526163,0.0001760436,0.00003071202,0.0009362837,0.001226571,0.008351594,0.002997927,0.9150346,0.07085393,0.00005131674],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03212911,0.004769153,0.8605083,0.01231955,0.0003169368,0.0002063,0.0001262139,0.001212655,0.08841184],"genre_scores_gemma":[0.5842291,0.003272182,0.3931085,0.001623449,0.0004137255,0.0002802169,0.0001276324,0.0006420813,0.01630314],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01940678,"threshold_uncertainty_score":0.1026341,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0424867910284814,"score_gpt":0.296455703992082,"score_spread":0.2539689129636006,"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."}}