{"id":"W2951994069","doi":"10.48550/arxiv.1812.03624","title":"Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic","year":2018,"lang":"en","type":"preprint","venue":"arXiv (Cornell University)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Ottawa","funders":"","keywords":"Soundness; Programming language; Metatheory; Dependent type; Computer science; Linear logic; Syntax; Lambda calculus; Type theory; Combinatory logic; Theoretical computer science; Typed lambda calculus; Logic programming; Type (biology); 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.002916503,0.000510781,0.0008313471,0.002161228,0.001463972,0.00448704,0.002240015,0.001287328,0.005965017],"category_scores_gemma":[0.002244378,0.0007860482,0.001728432,0.00148806,0.005730597,0.004533105,0.002955233,0.003767375,0.001234407],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003138947,"about_ca_system_score_gemma":0.003072288,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003773651,"about_ca_topic_score_gemma":0.003207388,"domain_scores_codex":[0.9983661,0.0004555508,0.0001389065,0.0002746898,0.0005178044,0.0002469559],"domain_scores_gemma":[0.9986588,0.000539207,0.0001507525,0.0002068805,0.0003149555,0.0001293744],"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.000006993315,0.00001302167,0.00008551356,0.00002556614,0.000005755172,0.00007357963,0.0002399186,0.0009721027,0.0008007021,0.9956645,0.0003571417,0.00175517],"study_design_scores_gemma":[0.00003858166,0.00004101657,0.0001895553,0.00005919525,0.00003330066,0.0001905051,0.0001563074,0.03566267,0.002742219,0.944634,0.01621027,0.00004238732],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02781318,0.0004103831,0.9476451,0.001604111,0.000139842,0.0001181973,0.0002741129,0.001189329,0.02080588],"genre_scores_gemma":[0.5933924,0.0005328642,0.3895273,0.001250613,0.0003278931,0.0004339635,0.0003285266,0.0004841709,0.01372227],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005965017,"threshold_uncertainty_score":0.02277476,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.05692605589484442,"score_gpt":0.2130312227347483,"score_spread":0.1561051668399039,"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."}}