{"id":"W2296691843","doi":"10.1145/3290322","title":"Sound and complete bidirectional typechecking for higher-rank polymorphism with existentials and indexed types","year":2019,"lang":"en","type":"preprint","venue":"Proceedings of the ACM on Programming Languages","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"Queen's University","funders":"Engineering and Physical Sciences Research Council","keywords":"Computer science; Programming language; Type inference; Type theory; Dependent type; Haskell; Soundness; Mathematical proof; Subtyping; Combinatory logic; Scala; Type (biology); Theoretical computer science; Lambda calculus; Inference; Functional programming; Mathematics; Artificial intelligence; Java","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":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0005767386,0.0003291981,0.0004939725,0.000141946,0.0001979158,0.000572339,0.001477632,0.0002193906,0.000001909969],"category_scores_gemma":[0.0002426425,0.0002143398,0.0001166809,0.0001847385,0.0001816408,0.0001528682,0.001866981,0.0003152702,0.000001637888],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003642892,"about_ca_system_score_gemma":0.00004452922,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0001240964,"about_ca_topic_score_gemma":0.0000097032,"domain_scores_codex":[0.9982468,0.00001783476,0.0003117517,0.0006967649,0.000385643,0.0003411655],"domain_scores_gemma":[0.9983396,0.000160104,0.0006104457,0.0005569861,0.0002643231,0.00006853035],"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.0006088605,0.0005480666,0.08102234,0.01084639,0.00194436,0.00001037,0.01235995,0.00004775076,0.01020298,0.6136733,0.001115381,0.2676202],"study_design_scores_gemma":[0.01184772,0.006578311,0.07678893,0.004953888,0.002060454,0.00081113,0.004788143,0.003613892,0.04162595,0.7358399,0.1036774,0.007414307],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"empirical","genre_gemma":"empirical","genre_scores_codex":[0.9387527,0.01889759,0.01697209,0.005966581,0.003889086,0.009006255,0.00004890263,0.001304155,0.005162676],"genre_scores_gemma":[0.9680349,0.00002526437,0.03079643,0.00008056414,0.000210515,0.0001173812,0.000004530547,0.00003546683,0.0006949269],"genre_candidate":"empirical","genre_consensus":"empirical","teacher_disagreement_score":0.2602059,"threshold_uncertainty_score":0.8740525,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04079259752242029,"score_gpt":0.2765958302982153,"score_spread":0.235803232775795,"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."}}