{ "name": "type-system-implementation", "publications": [ { "type": "inproceedings", "conference": "popl", "conferenceYear": "", "booktitle": "POPL", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "", "editors": [], "firstpage": 229, "lastpage": 235, "id": "02845337-ce99-4408-b336-fd41d7f2d8a0", "key": "SneltingH86", "title": "Unification in Many-Sorted Algebras as a Device for Incremental Semantic Analysis", "month": "", "year": "1986", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/SneltingH86", "authors": [ { "alias": { "url": "https://researchr.org/alias/gregor-snelting", "id": "4b63d575-234e-43f6-afde-3a0386383aad", "key": "gregor-snelting", "name": "Gregor Snelting" } }, { "alias": { "url": "https://researchr.org/alias/wolfgang-henhapl", "id": "bbe582cd-eb2e-43ae-bd3e-14a19f43a321", "key": "wolfgang-henhapl", "name": "Wolfgang Henhapl" } } ] }, { "id": "05e6d000-7dec-4185-a6ce-8c4028394e6d", "key": "Har85-0", "title": "Aspects of the Implementation of Type Theory", "month": "", "year": "1985", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Har85-0", "authors": [ { "alias": { "url": "https://researchr.org/alias/robert-w.-harper", "id": "8cb51ee7-41f7-4383-844d-8cffabb2fb38", "key": "robert-w.-harper", "name": "Robert W. Harper" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings", "volume": "2741", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/franz-baader", "id": "02e35dae-b679-402a-8c6d-5a678a80925f", "key": "franz-baader", "name": "Franz Baader" } } ], "firstpage": 473, "lastpage": 487, "id": "08a95d4e-1096-4d45-a776-f11aaf5a6e2b", "key": "PientkaP03", "title": "Optimizing Higher-Order Pattern Unification", "month": "", "year": "2003", "doi": "http://springerlink.metapress.com/openurl.asp?genre\u003darticle\u0026amp;issn\u003d0302-9743\u0026amp;volume\u003d2741\u0026amp;spage\u003d473", "note": "", "abstract": "", "url": "https://researchr.org/publication/PientkaP03", "authors": [ { "alias": { "url": "https://researchr.org/alias/brigitte-pientka", "id": "ffa902a1-f230-4f09-b858-3bfb3d5d5878", "key": "brigitte-pientka", "name": "Brigitte Pientka" } }, { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } } ] }, { "type": "article", "journal": "PACMPL", "volumenumber": "3", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "08ad9eb2-c96e-4350-91ee-ad779beb0b2d", "key": "WeirichCVE19", "title": "A role for dependent types in Haskell", "month": "", "year": "2019", "doi": "https://doi.org/10.1145/3341705", "note": "", "abstract": "", "url": "https://researchr.org/publication/WeirichCVE19", "authors": [ { "alias": { "url": "https://researchr.org/alias/stephanie-weirich", "id": "6e5f4081-0f75-4178-a2ec-9822fdb2e8eb", "key": "stephanie-weirich", "name": "Stephanie Weirich" } }, { "alias": { "url": "https://researchr.org/alias/pritam-choudhury", "id": "3124e670-854b-42ee-9cf4-4096e6aef2e6", "key": "pritam-choudhury", "name": "Pritam Choudhury" } }, { "alias": { "url": "https://researchr.org/alias/antoine-voizard", "id": "f957c6ca-6980-48eb-9ab2-516677104d44", "key": "antoine-voizard", "name": "Antoine Voizard" } }, { "alias": { "url": "https://researchr.org/alias/richard-a.-eisenberg", "id": "351698b7-ddbf-44ca-969a-00ba578a305f", "key": "richard-a.-eisenberg", "name": "Richard A. Eisenberg" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "22nd International Conference on Types for Proofs and Programs, TYPES 2016, May 23-26, 2016, Novi Sad, Serbia", "volume": "97", "number": "", "series": "LIPIcs", "address": "", "organization": "", "publisher": "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik", "editors": [ { "alias": { "url": "https://researchr.org/alias/silvia-ghilezan", "id": "1160513e-b4f4-4310-83d9-310536626c6d", "key": "silvia-ghilezan", "name": "Silvia Ghilezan" } }, { "alias": { "url": "https://researchr.org/alias/herman-geuvers", "id": "07114cd3-b278-4a45-a617-a45046bcacb6", "key": "herman-geuvers", "name": "Herman Geuvers" } }, { "alias": { "url": "https://researchr.org/alias/jelena-ivetic", "id": "a078c03b-e3a6-46e7-b654-9e9755f02307", "key": "jelena-ivetic", "name": "Jelena Ivetic" } } ], "firstpage": 0, "lastpage": 0, "id": "0e7b80b5-5327-44f1-9389-787209ba9237", "key": "BauerGHPS16", "title": "Design and Implementation of the Andromeda Proof Assistant", "month": "", "year": "2016", "doi": "https://doi.org/10.4230/LIPIcs.TYPES.2016.5", "note": "", "abstract": "", "url": "https://researchr.org/publication/BauerGHPS16", "authors": [ { "alias": { "url": "https://researchr.org/alias/andrej-bauer", "id": "9def6603-9dd2-4843-b5d3-9911d86954e4", "key": "andrej-bauer", "name": "Andrej Bauer" } }, { "alias": { "url": "https://researchr.org/alias/ga%C3%ABtan-gilbert", "id": "bf0f23c3-a921-473b-bdf7-cebec80f96c2", "key": "gaëtan-gilbert", "name": "Gaëtan Gilbert" } }, { "alias": { "url": "https://researchr.org/alias/philipp-g.-haselwarter", "id": "6e1c6b15-9b7d-4ad5-8bde-3554a1257e6a", "key": "philipp-g.-haselwarter", "name": "Philipp G. Haselwarter" } }, { "alias": { "url": "https://researchr.org/alias/matija-pretnar", "id": "9eb7f5d5-0293-42fb-80b0-50155ecda391", "key": "matija-pretnar", "name": "Matija Pretnar" } }, { "alias": { "url": "https://researchr.org/alias/christopher-a.-stone", "id": "d5fd211f-7a8b-4191-97d3-82e0e5e83d24", "key": "christopher-a.-stone", "name": "Christopher A. Stone" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "17", "issuenumber": "2", "firstpage": 215, "lastpage": 286, "id": "11f8309f-3ed5-4039-b1ed-e131cdbca411", "key": "Xi07:0", "title": "Dependent ML An approach to practical programming with dependent types", "month": "", "year": "2007", "doi": "http://dx.doi.org/10.1017/S0956796806006216", "note": "", "abstract": "", "url": "https://researchr.org/publication/Xi07%3A0", "authors": [ { "alias": { "url": "https://researchr.org/alias/hongwei-xi", "id": "f55c9a21-0d0d-4e10-895d-b458e704dd72", "key": "hongwei-xi", "name": "Hongwei Xi" } } ] }, { "type": "inproceedings", "conference": "icfp", "conferenceYear": "", "booktitle": "Proceedings of the seventh ACM SIGPLAN international conference on Functional Programming (ICFP 2002)", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "", "editors": [], "firstpage": 235, "lastpage": 246, "id": "1f07196c-be8f-4f81-acd6-66222134a5ec", "key": "GregoireL02", "title": "A compiled implementation of strong reduction", "month": "", "year": "2002", "doi": "http://doi.acm.org/10.1145/581478.581501", "note": "", "abstract": "", "url": "https://researchr.org/publication/GregoireL02", "authors": [ { "alias": { "url": "https://researchr.org/alias/benjamin-gr%C3%A9goire", "id": "bd7fa072-c16b-449d-a8d6-1ffc885d4438", "key": "benjamin-grégoire", "name": "Benjamin Grégoire" } }, { "alias": { "url": "https://researchr.org/alias/xavier-leroy", "id": "b5e441a0-7288-4c05-ac0b-ca8acf3af398", "key": "xavier-leroy", "name": "Xavier Leroy" }, "person": { "url": "https://researchr.org/profile/xavierleroy", "id": "eaeb9530-a4d0-40e2-846a-aff61555c158", "key": "xavierleroy", "fullname": "Xavier Leroy" } } ] }, { "type": "inproceedings", "conference": "lics", "conferenceYear": "", "booktitle": "Proceedings, Fourth Annual Symposium on Logic in Computer Science, 5-8 June, 1989, Asilomar Conference Center, Pacific Grove, California, USA", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "IEEE Computer Society", "editors": [], "firstpage": 313, "lastpage": 322, "id": "212de2a6-1700-42d3-a472-24d1c9e357f7", "key": "Pfenning89", "title": "Elf: A Language for Logic Definition and Verified Metaprogramming", "month": "", "year": "1989", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Pfenning89", "authors": [ { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } } ] }, { "type": "inproceedings", "conference": "fscd", "conferenceYear": "", "booktitle": "5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference)", "volume": "167", "number": "", "series": "LIPIcs", "address": "", "organization": "", "publisher": "Schloss Dagstuhl - Leibniz-Zentrum für Informatik", "editors": [ { "alias": { "url": "https://researchr.org/alias/zena-m.-ariola", "id": "6eb79994-428b-40e6-b76b-18913f75dafe", "key": "zena-m.-ariola", "name": "Zena M. Ariola" } } ], "firstpage": 0, "lastpage": 0, "id": "21d6f47c-4781-4d3d-b806-7e8518f09fc9", "key": "HondetB20", "title": "The New Rewriting Engine of Dedukti (System Description)", "month": "", "year": "2020", "doi": "https://doi.org/10.4230/LIPIcs.FSCD.2020.35", "note": "", "abstract": "", "url": "https://researchr.org/publication/HondetB20", "authors": [ { "alias": { "url": "https://researchr.org/alias/gabriel-hondet", "id": "17418a11-6864-4dc6-bed1-987296ba327c", "key": "gabriel-hondet", "name": "Gabriel Hondet" } }, { "alias": { "url": "https://researchr.org/alias/fr%C3%A9d%C3%A9ric-blanqui", "id": "10facc20-e42c-4445-9011-c9564e03a9df", "key": "frédéric-blanqui", "name": "Frédéric Blanqui" } } ] }, { "type": "article", "journal": "Proc. ACM Program. Lang.", "volumenumber": "8", "issuenumber": "PLDI", "firstpage": 1115, "lastpage": 1139, "id": "2377997b-e347-4168-9048-e4acd723a923", "key": "GaherSJKD24", "title": "RefinedRust: A Type System for High-Assurance Verification of Rust Programs", "month": "", "year": "2024", "doi": "https://doi.org/10.1145/3656422", "note": "", "abstract": "", "url": "https://researchr.org/publication/GaherSJKD24", "authors": [ { "alias": { "url": "https://researchr.org/alias/lennard-g%C3%A4her", "id": "177eaa74-324c-41ab-a5cb-48c4a4f9d83d", "key": "lennard-gäher", "name": "Lennard Gäher" } }, { "alias": { "url": "https://researchr.org/alias/michael-sammler", "id": "9228d961-c332-41e4-9d28-d84dacca7752", "key": "michael-sammler", "name": "Michael Sammler" } }, { "alias": { "url": "https://researchr.org/alias/ralf-jung-0002", "id": "2e7179dc-3061-4a6e-9012-21b791030c3b", "key": "ralf-jung-0002", "name": "Ralf Jung 0002" } }, { "alias": { "url": "https://researchr.org/alias/robbert-krebbers", "id": "4af5e5e8-154a-4c27-bd7e-8698e988adfd", "key": "robbert-krebbers", "name": "Robbert Krebbers" } }, { "alias": { "url": "https://researchr.org/alias/derek-dreyer", "id": "f0b63475-1479-452c-b944-30b8b783767c", "key": "derek-dreyer", "name": "Derek Dreyer" } } ] }, { "id": "256d0293-f600-40fb-9cfd-110797ead3bc", "key": "frber2021small", "title": "Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo Rewriting", "month": "", "year": "2021", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/frber2021small", "authors": [ { "alias": { "url": "https://researchr.org/alias/michael-f%C3%A4rber", "id": "26725875-a2f5-4eb9-afd4-4943e19698ff", "key": "michael-färber", "name": "Michael Färber" } } ] }, { "type": "article", "journal": "Proc. ACM Program. Lang.", "volumenumber": "4", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "2690f3d0-fc76-435b-82c5-db023ab72ae8", "key": "Tejiscak20", "title": "A dependently typed calculus with pattern matching and erasure inference", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3408973", "note": "", "abstract": "", "url": "https://researchr.org/publication/Tejiscak20", "authors": [ { "alias": { "url": "https://researchr.org/alias/matus-tejiscak", "id": "4e21c565-db83-4ab2-99b1-b4cb5474d25f", "key": "matus-tejiscak", "name": "Matus Tejiscak" } } ] }, { "id": "2ac8292a-2e60-45e7-92ac-d6021f587b09", "key": "hondet:hal-02317471", "title": "Efficient rewriting using decision trees", "month": "Aug", "year": "2019", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/hondet%3Ahal-02317471", "authors": [ { "alias": { "url": "https://researchr.org/alias/hondet%2C-gabriel", "id": "9377b4a3-970c-4265-b86f-51ba93b34b1b", "key": "hondet,-gabriel", "name": "Hondet, Gabriel" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway", "volume": "175", "number": "", "series": "LIPIcs", "address": "", "organization": "", "publisher": "Schloss Dagstuhl - Leibniz-Zentrum für Informatik", "editors": [ { "alias": { "url": "https://researchr.org/alias/marc-bezem", "id": "5481f276-2477-421b-8d2d-82eb75326713", "key": "marc-bezem", "name": "Marc Bezem" } }, { "alias": { "url": "https://researchr.org/alias/assia-mahboubi", "id": "ef2599ee-5dfe-4331-9e65-f4f588174e93", "key": "assia-mahboubi", "name": "Assia Mahboubi" } } ], "firstpage": 0, "lastpage": 0, "id": "2c436032-d9b3-4875-893d-6629cbd0500d", "key": "Cockx19", "title": "Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules", "month": "", "year": "2019", "doi": "https://doi.org/10.4230/LIPIcs.TYPES.2019.2", "note": "", "abstract": "", "url": "https://researchr.org/publication/Cockx19", "authors": [ { "alias": { "url": "https://researchr.org/alias/jesper-cockx", "id": "379545f4-fdfd-42b3-8892-9a73768dbaba", "key": "jesper-cockx", "name": "Jesper Cockx" }, "person": { "url": "https://researchr.org/profile/jespercockx", "id": "46dd4d29-926d-4723-bd06-81f3726e7558", "key": "jespercockx", "fullname": "Jesper Cockx" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings", "volume": "9706", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/nicola-olivetti", "id": "043adaa7-2ce3-4080-a2af-15b3a28d3157", "key": "nicola-olivetti", "name": "Nicola Olivetti" } }, { "alias": { "url": "https://researchr.org/alias/ashish-tiwari", "id": "6e259cf1-8d65-4f99-a820-16cbe07817b5", "key": "ashish-tiwari", "name": "Ashish Tiwari" } } ], "firstpage": 99, "lastpage": 115, "id": "2ea5e10a-a4b1-43f9-8f1a-5bbd1ea333e2", "key": "SelsamM16", "title": "Congruence Closure in Intensional Type Theory", "month": "", "year": "2016", "doi": "http://dx.doi.org/10.1007/978-3-319-40229-1_8", "note": "", "abstract": "", "url": "https://researchr.org/publication/SelsamM16", "authors": [ { "alias": { "url": "https://researchr.org/alias/daniel-selsam", "id": "3cb8c492-9382-4399-9cf4-ff32bdbb37b5", "key": "daniel-selsam", "name": "Daniel Selsam" } }, { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } } ] }, { "type": "inproceedings", "conference": "tphol", "conferenceYear": "", "booktitle": "Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003, Rom, Italy, September 8-12, 2003, Proceedings", "volume": "2758", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/david-a.-basin", "id": "50b64455-99c1-4eb9-94fc-07aeccd34166", "key": "david-a.-basin", "name": "David A. Basin" } }, { "alias": { "url": "https://researchr.org/alias/burkhart-wolff", "id": "f15d1a5f-412a-430b-86cf-3c2a3710d4c2", "key": "burkhart-wolff", "name": "Burkhart Wolff" } } ], "firstpage": 120, "lastpage": 135, "id": "31484253-21b3-4928-91b1-738aaa278bcb", "key": "SchurmannP03", "title": "A Coverage Checking Algorithm for LF", "month": "", "year": "2003", "doi": "http://springerlink.metapress.com/openurl.asp?genre\u003darticle\u0026amp;issn\u003d0302-9743\u0026amp;volume\u003d2758\u0026amp;spage\u003d120", "note": "", "abstract": "", "url": "https://researchr.org/publication/SchurmannP03", "authors": [ { "alias": { "url": "https://researchr.org/alias/carsten-sch%C3%BCrmann", "id": "ea16dc4f-0420-4ee0-8fe8-949e23113ec5", "key": "carsten-schürmann", "name": "Carsten Schürmann" } }, { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } } ] }, { "type": "article", "journal": "PACMPL", "volumenumber": "3", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "378d574d-20c3-4a5d-9dbc-22b0fa1e45ae", "key": "SozeauM19", "title": "Equations reloaded: high-level dependently-typed functional programming and proving in Coq", "month": "", "year": "2019", "doi": "https://doi.org/10.1145/3341690", "note": "", "abstract": "", "url": "https://researchr.org/publication/SozeauM19", "authors": [ { "alias": { "url": "https://researchr.org/alias/matthieu-sozeau", "id": "915a6b4d-ac46-409a-b405-1e31079029ee", "key": "matthieu-sozeau", "name": "Matthieu Sozeau" } }, { "alias": { "url": "https://researchr.org/alias/cyprien-mangin", "id": "b58dcede-e874-4a52-985b-3b13e929ce45", "key": "cyprien-mangin", "name": "Cyprien Mangin" } } ] }, { "type": "inproceedings", "conference": "icfp", "conferenceYear": "", "booktitle": "Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/jacques-garrigue", "id": "7be8552d-e6cd-4e13-9b81-1b6e804a2afa", "key": "jacques-garrigue", "name": "Jacques Garrigue" } }, { "alias": { "url": "https://researchr.org/alias/gabriele-keller", "id": "826976c6-ba5c-48b1-8a13-bae63dfed0b5", "key": "gabriele-keller", "name": "Gabriele Keller" } }, { "alias": { "url": "https://researchr.org/alias/eijiro-sumii", "id": "03de522e-d659-4954-8135-7ab3b5b76a8f", "key": "eijiro-sumii", "name": "Eijiro Sumii" } } ], "firstpage": 284, "lastpage": 297, "id": "3d51c5d6-83b8-40f8-a5a0-e9de89b4d55c", "key": "ChristiansenB16", "title": "Elaborator reflection: extending Idris in Idris", "month": "", "year": "2016", "doi": "http://doi.acm.org/10.1145/2951913.2951932", "note": "", "abstract": "", "url": "https://researchr.org/publication/ChristiansenB16", "authors": [ { "alias": { "url": "https://researchr.org/alias/david-christiansen", "id": "cc421cac-a1c5-42ee-a53b-11ceabd66a4e", "key": "david-christiansen", "name": "David Christiansen" } }, { "alias": { "url": "https://researchr.org/alias/edwin-brady", "id": "071438f4-d83e-481f-973b-9fb75a2a6605", "key": "edwin-brady", "name": "Edwin Brady" }, "person": { "url": "https://researchr.org/profile/edwinbrady", "id": "deefc76b-14bb-4e95-b2b3-cbb4874ea695", "key": "edwinbrady", "fullname": "Edwin Brady" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings", "volume": "9195", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/amy-p.-felty", "id": "2b469895-8ccc-405a-bdae-5aa61a9964ce", "key": "amy-p.-felty", "name": "Amy P. Felty" } }, { "alias": { "url": "https://researchr.org/alias/aart-middeldorp", "id": "3520681b-1d93-464f-805b-477331cd2c40", "key": "aart-middeldorp", "name": "Aart Middeldorp" } } ], "firstpage": 378, "lastpage": 388, "id": "4209d28c-8c0f-4fe1-b382-e8044edb1103", "key": "MouraKADR15", "title": "The Lean Theorem Prover (System Description)", "month": "", "year": "2015", "doi": "http://dx.doi.org/10.1007/978-3-319-21401-6_26", "note": "", "abstract": "", "url": "https://researchr.org/publication/MouraKADR15", "authors": [ { "alias": { "url": "https://researchr.org/alias/leonardo-mendon%C3%A7a-de-moura", "id": "a0d65825-971d-4f8b-8abc-96e1f2b1ad47", "key": "leonardo-mendonça-de-moura", "name": "Leonardo Mendonça de Moura" } }, { "alias": { "url": "https://researchr.org/alias/soonho-kong", "id": "67e5fe7a-3aa2-4634-9360-77fbb4b1e301", "key": "soonho-kong", "name": "Soonho Kong" } }, { "alias": { "url": "https://researchr.org/alias/jeremy-avigad", "id": "8b346f05-14af-47dd-a45a-f21dfacc60ad", "key": "jeremy-avigad", "name": "Jeremy Avigad" } }, { "alias": { "url": "https://researchr.org/alias/floris-van-doorn", "id": "0cc4db85-2e16-4c1c-8311-3604d34bd04e", "key": "floris-van-doorn", "name": "Floris van Doorn" } }, { "alias": { "url": "https://researchr.org/alias/jakob-von-raumer", "id": "8f13bf9e-7e60-4a6f-9177-422a687a7ba5", "key": "jakob-von-raumer", "name": "Jakob von Raumer" } } ] }, { "type": "inproceedings", "conference": "ifl", "conferenceYear": "", "booktitle": "Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL \u002714, Boston, MA, USA, October 1-3, 2014", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/sam-tobin-hochstadt", "id": "62bdfa5e-bb01-4006-ac9f-cd3e6076ed84", "key": "sam-tobin-hochstadt", "name": "Sam Tobin-Hochstadt" } } ], "firstpage": 1, "lastpage": 0, "id": "43dea761-32e8-41de-ae46-49e874014454", "key": "Christiansen14-1", "title": "Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection", "month": "", "year": "2014", "doi": "http://doi.acm.org/10.1145/2746325.2746326", "note": "", "abstract": "", "url": "https://researchr.org/publication/Christiansen14-1", "authors": [ { "alias": { "url": "https://researchr.org/alias/david-raymond-christiansen", "id": "399fb675-0e23-4cca-9167-9587a23c05ff", "key": "david-raymond-christiansen", "name": "David Raymond Christiansen" } } ] }, { "id": "44f854ff-6b11-4bc2-9c68-c9e87c89f67b", "key": "Norell2007towardsapractical", "title": "Towards a practical programming language based on dependent type theory", "month": "September", "year": "2007", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Norell2007towardsapractical", "authors": [ { "alias": { "url": "https://researchr.org/alias/ulf-norell", "id": "7e7a07cd-30ac-41ed-8837-f9d0db689d0e", "key": "ulf-norell", "name": "Ulf Norell" } } ] }, { "type": "inproceedings", "conference": "popl", "conferenceYear": "", "booktitle": "POPL", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "", "editors": [], "firstpage": 214, "lastpage": 227, "id": "4a61730b-8347-4645-a190-47580e081fe1", "key": "XiP99", "title": "Dependent Types in Practical Programming", "month": "", "year": "1999", "doi": "http://doi.acm.org/10.1145/292540.292560", "note": "", "abstract": "", "url": "https://researchr.org/publication/XiP99", "authors": [ { "alias": { "url": "https://researchr.org/alias/hongwei-xi", "id": "f55c9a21-0d0d-4e10-895d-b458e704dd72", "key": "hongwei-xi", "name": "Hongwei Xi" }, "person": { "url": "https://researchr.org/profile/hongweixi", "id": "e563f529-dd99-49a6-b469-d06c46240182", "key": "hongweixi", "fullname": "Hongwei Xi" } }, { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } } ] }, { "type": "inproceedings", "conference": "lpar", "conferenceYear": "", "booktitle": "Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings", "volume": "9450", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/martin-davis", "id": "f4e088d0-00c7-4cd5-b0ff-8077086955fa", "key": "martin-davis", "name": "Martin Davis" } }, { "alias": { "url": "https://researchr.org/alias/ansgar-fehnker", "id": "49a76c74-240d-46f6-a949-926ae600d8ff", "key": "ansgar-fehnker", "name": "Ansgar Fehnker" } }, { "alias": { "url": "https://researchr.org/alias/annabelle-mciver", "id": "3b8981c2-1c73-459f-9129-87d87e4054f8", "key": "annabelle-mciver", "name": "Annabelle McIver" } }, { "alias": { "url": "https://researchr.org/alias/andrei-voronkov", "id": "948b5857-11db-4275-83ba-b1aee6b13d2b", "key": "andrei-voronkov", "name": "Andrei Voronkov" } } ], "firstpage": 460, "lastpage": 468, "id": "4b3045e5-774f-47b9-804c-57ce69954729", "key": "DunchevGCT15", "title": "ELPI: Fast, Embeddable, \\lambda Prolog Interpreter", "month": "", "year": "2015", "doi": "http://dx.doi.org/10.1007/978-3-662-48899-7_32", "note": "", "abstract": "", "url": "https://researchr.org/publication/DunchevGCT15", "authors": [ { "alias": { "url": "https://researchr.org/alias/cvetan-dunchev", "id": "8e82d4f8-a159-4f7f-8cec-46a0b8c63fac", "key": "cvetan-dunchev", "name": "Cvetan Dunchev" } }, { "alias": { "url": "https://researchr.org/alias/ferruccio-guidi", "id": "8351f06f-e5af-47da-bdf5-227350282505", "key": "ferruccio-guidi", "name": "Ferruccio Guidi" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } } ] }, { "id": "51ab7765-5b81-49f9-b2a3-5396db7cc117", "key": "dagand2012elaborating", "title": "Elaborating Inductive Definitions", "month": "", "year": "2012", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/dagand2012elaborating", "authors": [ { "alias": { "url": "https://researchr.org/alias/pierre-evariste-dagand", "id": "0efd12d8-75fd-41fd-a184-ba7d0ca6e435", "key": "pierre-evariste-dagand", "name": "Pierre-Evariste Dagand" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II", "volume": "12167", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/nicolas-peltier", "id": "a046ec28-9ef4-4360-af32-b88962a259fd", "key": "nicolas-peltier", "name": "Nicolas Peltier" } }, { "alias": { "url": "https://researchr.org/alias/viorica-sofronie-stokkermans", "id": "765189f7-3807-4806-83fd-67bd6cc029db", "key": "viorica-sofronie-stokkermans", "name": "Viorica Sofronie-Stokkermans" } } ], "firstpage": 167, "lastpage": 182, "id": "575ba4db-47a6-4c7f-a2d0-3eeaea114560", "key": "0002M20-2", "title": "Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages", "month": "", "year": "2020", "doi": "https://doi.org/10.1007/978-3-030-51054-1_10", "note": "", "abstract": "", "url": "https://researchr.org/publication/0002M20-2", "authors": [ { "alias": { "url": "https://researchr.org/alias/sebastian-ullrich", "id": "7807da24-f80f-4274-95bd-018d26525119", "key": "sebastian-ullrich", "name": "Sebastian Ullrich" }, "person": { "url": "https://researchr.org/profile/sebastianullrich", "id": "af6a9ce4-253d-4cd1-868e-b26560d5e223", "key": "sebastianullrich", "fullname": "Sebastian Ullrich" } }, { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } } ] }, { "id": "57a286d3-3c94-4b91-88c2-c679705330bc", "key": "friedman2018little", "title": "The Little Typer", "month": "", "year": "2018", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/friedman2018little", "authors": [ { "alias": { "url": "https://researchr.org/alias/friedman%2C-daniel-p", "id": "cdf68fad-13cd-467c-982b-984686f9623c", "key": "friedman,-daniel-p", "name": "Friedman, Daniel P" } }, { "alias": { "url": "https://researchr.org/alias/christiansen%2C-david-thrane", "id": "f18eac82-bfc3-43ca-9ad9-701028d0dc06", "key": "christiansen,-david-thrane", "name": "Christiansen, David Thrane" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "Types for Proofs and Programs, International Workshop TYPES 99, Lökeberg, Sweden, June 12-16, 1999, Selected Papers", "volume": "1956", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/thierry-coquand", "id": "4c7d3354-af12-4a8a-b442-9c1af76f0e73", "key": "thierry-coquand", "name": "Thierry Coquand" } }, { "alias": { "url": "https://researchr.org/alias/peter-dybjer", "id": "10972740-60f0-4aae-a910-c71e0f6cc32a", "key": "peter-dybjer", "name": "Peter Dybjer" } }, { "alias": { "url": "https://researchr.org/alias/bengt-nordstr%C3%B6m", "id": "ab6b9fe3-0436-4b14-b609-4c1fb8da44a1", "key": "bengt-nordström", "name": "Bengt Nordström" } }, { "alias": { "url": "https://researchr.org/alias/jan-m.-smith", "id": "9ecc60b0-5d5d-471d-baed-0a2cf4e7a4f2", "key": "jan-m.-smith", "name": "Jan M. Smith" } } ], "firstpage": 94, "lastpage": 113, "id": "5954aeea-d5fb-4a2f-a6a3-b363d649a6b5", "key": "CallaghanL99", "title": "Implementation Techniques for Inductive Types in Plastic", "month": "", "year": "1999", "doi": "http://link.springer.de/link/service/series/0558/bibs/1956/19560094.htm", "note": "", "abstract": "", "url": "https://researchr.org/publication/CallaghanL99", "authors": [ { "alias": { "url": "https://researchr.org/alias/paul-callaghan", "id": "b140e034-7e65-4e8f-b202-b20a8ff92a2a", "key": "paul-callaghan", "name": "Paul Callaghan" } }, { "alias": { "url": "https://researchr.org/alias/zhaohui-luo", "id": "1c1a3885-6cce-4af3-812a-ec6eb3dd52d2", "key": "zhaohui-luo", "name": "Zhaohui Luo" } } ] }, { "type": "inproceedings", "conference": "iclp", "conferenceYear": "", "booktitle": "Logic Programming, 20th International Conference, ICLP 2004, Saint-Malo, France, September 6-10, 2004, Proceedings", "volume": "3132", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/bart-demoen", "id": "1b8e20ec-c246-4563-b817-f2b536d188b6", "key": "bart-demoen", "name": "Bart Demoen" } }, { "alias": { "url": "https://researchr.org/alias/vladimir-lifschitz", "id": "c9b78fe2-b012-449f-92c9-cd393bbf41f3", "key": "vladimir-lifschitz", "name": "Vladimir Lifschitz" } } ], "firstpage": 269, "lastpage": 283, "id": "5afe6b24-fcbd-48ce-93d7-3d989ea52318", "key": "CheneyU04", "title": "alpha-Prolog: A Logic Programming Language with Names, Binding and a-Equivalence", "month": "", "year": "2004", "doi": "http://springerlink.metapress.com/openurl.asp?genre\u003darticle\u0026amp;issn\u003d0302-9743\u0026amp;volume\u003d3132\u0026amp;spage\u003d269", "note": "", "abstract": "", "url": "https://researchr.org/publication/CheneyU04", "authors": [ { "alias": { "url": "https://researchr.org/alias/james-cheney", "id": "029eed6f-842d-4461-87b6-9a188bd56a2d", "key": "james-cheney", "name": "James Cheney" } }, { "alias": { "url": "https://researchr.org/alias/christian-urban", "id": "c842235b-de23-42a4-8d5a-14a0bec36ea8", "key": "christian-urban", "name": "Christian Urban" } } ] }, { "type": "inproceedings", "conference": "sdt", "conferenceYear": "", "booktitle": "Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27-29, 1984, Proceedings", "volume": "173", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/gilles-kahn", "id": "432ce279-cdbd-48b3-9f90-b4fbda93a05d", "key": "gilles-kahn", "name": "Gilles Kahn" } }, { "alias": { "url": "https://researchr.org/alias/david-b.-macqueen", "id": "c0f99348-7a44-49fb-afa8-9e2a5b8329e5", "key": "david-b.-macqueen", "name": "David B. MacQueen" } }, { "alias": { "url": "https://researchr.org/alias/gordon-d.-plotkin", "id": "b5a334e6-e7e5-4700-8dd6-bf7664c84f5d", "key": "gordon-d.-plotkin", "name": "Gordon D. Plotkin" } } ], "firstpage": 215, "lastpage": 233, "id": "5c1d4661-ffec-44ab-968d-2431259f77b7", "key": "Despeyroux84", "title": "Executable Specification of Static Semantics", "month": "", "year": "1984", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Despeyroux84", "authors": [ { "alias": { "url": "https://researchr.org/alias/thierry-despeyroux", "id": "8c71842a-faa3-433e-beb8-75338eb62cee", "key": "thierry-despeyroux", "name": "Thierry Despeyroux" } } ] }, { "type": "inproceedings", "conference": "tlca", "conferenceYear": "", "booktitle": "Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009. Proceedings", "volume": "5608", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/pierre-louis-curien", "id": "c42f7f77-090a-4c54-8b03-090b186f3969", "key": "pierre-louis-curien", "name": "Pierre-Louis Curien" } } ], "firstpage": 5, "lastpage": 19, "id": "5fc590a4-641c-485e-86a2-95d6c2398b82", "key": "AbelCP09", "title": "A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance", "month": "", "year": "2009", "doi": "http://dx.doi.org/10.1007/978-3-642-02273-9_3", "note": "", "abstract": "", "url": "https://researchr.org/publication/AbelCP09", "authors": [ { "alias": { "url": "https://researchr.org/alias/andreas-abel", "id": "bb837782-2fca-43ee-82bd-fdf5eb32f279", "key": "andreas-abel", "name": "Andreas Abel" } }, { "alias": { "url": "https://researchr.org/alias/thierry-coquand", "id": "4c7d3354-af12-4a8a-b442-9c1af76f0e73", "key": "thierry-coquand", "name": "Thierry Coquand" } }, { "alias": { "url": "https://researchr.org/alias/miguel-pagano", "id": "553b72f2-a0fb-4133-82bd-51d7427972e7", "key": "miguel-pagano", "name": "Miguel Pagano" } } ] }, { "type": "article", "journal": "J. Autom. Reasoning", "volumenumber": "39", "issuenumber": "2", "firstpage": 109, "lastpage": 139, "id": "626b05e6-f152-438a-8580-7bdec1891e92", "key": "AspertiCTZ07", "title": "User Interaction with the Matita Proof Assistant", "month": "", "year": "2007", "doi": "http://dx.doi.org/10.1007/s10817-007-9070-5", "note": "", "abstract": "", "url": "https://researchr.org/publication/AspertiCTZ07", "authors": [ { "alias": { "url": "https://researchr.org/alias/andrea-asperti", "id": "3c4b5963-1e85-449b-ad7e-f3c33cc74f2c", "key": "andrea-asperti", "name": "Andrea Asperti" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } }, { "alias": { "url": "https://researchr.org/alias/stefano-zacchiroli", "id": "7ed9e3e7-f2d6-4975-8c38-8265bf6624f6", "key": "stefano-zacchiroli", "name": "Stefano Zacchiroli" } } ] }, { "id": "643726fa-ba85-4389-911b-b78eb8d3d1bb", "key": "ethos-4985", "title": "Practical implementation of a dependently typed functional programming language", "month": "", "year": "2005", "doi": "http://ethos.bl.uk/OrderDetails.do?uin\u003duk.bl.ethos.417649", "note": "British Library, EThOS", "abstract": "", "url": "https://researchr.org/publication/ethos-4985", "authors": [ { "alias": { "url": "https://researchr.org/alias/edwin-brady", "id": "071438f4-d83e-481f-973b-9fb75a2a6605", "key": "edwin-brady", "name": "Edwin Brady" }, "person": { "url": "https://researchr.org/profile/edwinbrady", "id": "deefc76b-14bb-4e95-b2b3-cbb4874ea695", "key": "edwinbrady", "fullname": "Edwin Brady" } } ] }, { "id": "655ab377-ecbe-4e83-ba36-6646e425848f", "key": "mazzoli2016type", "title": "Type checking through unification", "month": "", "year": "2016", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/mazzoli2016type", "authors": [ { "alias": { "url": "https://researchr.org/alias/francesco-mazzoli", "id": "a894c351-42dd-4ec1-9d9c-8069a6f60ed6", "key": "francesco-mazzoli", "name": "Francesco Mazzoli" } }, { "alias": { "url": "https://researchr.org/alias/andreas-abel", "id": "bb837782-2fca-43ee-82bd-fdf5eb32f279", "key": "andreas-abel", "name": "Andreas Abel" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings", "volume": "1632", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/harald-ganzinger", "id": "b5444565-26ce-4c95-bd4f-e7bb54aca7f2", "key": "harald-ganzinger", "name": "Harald Ganzinger" } } ], "firstpage": 202, "lastpage": 206, "id": "6be63cbc-8a47-4024-856e-313cd5ecb704", "key": "PfenningS99", "title": "System Description: Twelf - A Meta-Logical Framework for Deductive Systems", "month": "", "year": "1999", "doi": "http://link.springer.de/link/service/series/0558/bibs/1632/16320202.htm", "note": "", "abstract": "", "url": "https://researchr.org/publication/PfenningS99", "authors": [ { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } }, { "alias": { "url": "https://researchr.org/alias/carsten-sch%C3%BCrmann", "id": "ea16dc4f-0420-4ee0-8fe8-949e23113ec5", "key": "carsten-schürmann", "name": "Carsten Schürmann" } } ] }, { "type": "article", "journal": "Higher-Order Programming with Effects", "volumenumber": "65", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "6ea80317-8a02-400d-99f9-cdd162ec517e", "key": "bowman2016growing", "title": "Growing a proof assistant", "month": "", "year": "2016", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/bowman2016growing", "authors": [ { "alias": { "url": "https://researchr.org/alias/bowman%2C-william-j", "id": "ee581db5-7e4b-4666-9a31-3bfff0399c0f", "key": "bowman,-william-j", "name": "Bowman, William J" } } ] }, { "type": "article", "journal": "CoRR", "volumenumber": "abs/1505.04324", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "70dbd461-dba5-459b-a0a1-d86fe1c5adfd", "key": "DBLP:journals-corr-MouraAKR15", "title": "Elaboration in Dependent Type Theory", "month": "", "year": "2015", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/DBLP%3Ajournals-corr-MouraAKR15", "authors": [ { "alias": { "url": "https://researchr.org/alias/leonardo-mendon%7B%5Ebc%7Bc%7D%7Da-de-moura", "id": "ccebad1d-236d-4b07-97d9-d3f47b49520b", "key": "leonardo-mendon{\\c{c}}a-de-moura", "name": "Leonardo Mendon{\\c{c}}a de Moura" } }, { "alias": { "url": "https://researchr.org/alias/jeremy-avigad", "id": "8b346f05-14af-47dd-a45a-f21dfacc60ad", "key": "jeremy-avigad", "name": "Jeremy Avigad" } }, { "alias": { "url": "https://researchr.org/alias/soonho-kong", "id": "67e5fe7a-3aa2-4634-9360-77fbb4b1e301", "key": "soonho-kong", "name": "Soonho Kong" } }, { "alias": { "url": "https://researchr.org/alias/cody-roux", "id": "45718907-04b3-4722-96d0-46e3919f468c", "key": "cody-roux", "name": "Cody Roux" } } ] }, { "type": "inproceedings", "conference": "cpp", "conferenceYear": "", "booktitle": "CPP \u002722: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/andrei-popescu-0001", "id": "2600ab5c-f002-4057-8ceb-7d88f03f4f33", "key": "andrei-popescu-0001", "name": "Andrei Popescu 0001" } }, { "alias": { "url": "https://researchr.org/alias/steve-zdancewic", "id": "4b79ee25-cb27-427f-afb2-e35e1a6ca09f", "key": "steve-zdancewic", "name": "Steve Zdancewic" } } ], "firstpage": 225, "lastpage": 238, "id": "72f7e470-5141-4437-885e-f62e7c865afd", "key": "Farber22", "title": "Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting", "month": "", "year": "2022", "doi": "https://doi.org/10.1145/3497775.3503683", "note": "", "abstract": "", "url": "https://researchr.org/publication/Farber22", "authors": [ { "alias": { "url": "https://researchr.org/alias/michael-f%C3%A4rber", "id": "26725875-a2f5-4eb9-afd4-4943e19698ff", "key": "michael-färber", "name": "Michael Färber" } } ] }, { "type": "article", "journal": "ACM Trans. Program. Lang. Syst.", "volumenumber": "8", "issuenumber": "4", "firstpage": 547, "lastpage": 576, "id": "79a9a01e-b5be-42c1-8bb0-0f6ede389478", "key": "BahlkeS86:0", "title": "The PSG System: From Formal Language Definitions to Interactive Programming Environments", "month": "", "year": "1986", "doi": "http://doi.acm.org/10.1145/6465.20890", "note": "", "abstract": "", "url": "https://researchr.org/publication/BahlkeS86%3A0", "authors": [ { "alias": { "url": "https://researchr.org/alias/rolf-bahlke", "id": "0fdb6c75-6646-4847-99c0-cee5f11cf767", "key": "rolf-bahlke", "name": "Rolf Bahlke" } }, { "alias": { "url": "https://researchr.org/alias/gregor-snelting", "id": "4b63d575-234e-43f6-afde-3a0386383aad", "key": "gregor-snelting", "name": "Gregor Snelting" } } ] }, { "id": "7be2e05b-000d-4525-b9c7-6825f3b790df", "key": "ethos-1465", "title": "Type inference, Haskell and dependent types", "month": "", "year": "2013", "doi": "http://ethos.bl.uk/OrderDetails.do?uin\u003duk.bl.ethos.605927", "note": "British Library, EThOS", "abstract": "", "url": "https://researchr.org/publication/ethos-1465", "authors": [ { "alias": { "url": "https://researchr.org/alias/adam-michael-gundry", "id": "aa5bbf0b-cbe1-4ebc-aba5-79be76304679", "key": "adam-michael-gundry", "name": "Adam Michael Gundry" } } ] }, { "type": "inproceedings", "conference": "rta", "conferenceYear": "", "booktitle": "Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings", "volume": "8560", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/gilles-dowek", "id": "0c78cea6-7d33-47b0-a34e-613fb28bef2d", "key": "gilles-dowek", "name": "Gilles Dowek" } } ], "firstpage": 31, "lastpage": 45, "id": "7c0ac786-745d-4956-9e1f-26e6a38cac40", "key": "Setzer0PT14", "title": "Unnesting of Copatterns", "month": "", "year": "2014", "doi": "http://dx.doi.org/10.1007/978-3-319-08918-8_3", "note": "", "abstract": "", "url": "https://researchr.org/publication/Setzer0PT14", "authors": [ { "alias": { "url": "https://researchr.org/alias/anton-setzer", "id": "8fb60653-d5bb-4ccc-95f4-93382d47d3ef", "key": "anton-setzer", "name": "Anton Setzer" } }, { "alias": { "url": "https://researchr.org/alias/andreas-abel-0001", "id": "4f66562d-b754-48d7-8d3c-2dc719f48983", "key": "andreas-abel-0001", "name": "Andreas Abel 0001" }, "person": { "url": "https://researchr.org/profile/andreasabel", "id": "7769fdd0-5885-4718-af1d-8942aa05f1b1", "key": "andreasabel", "fullname": "Andreas Abel" } }, { "alias": { "url": "https://researchr.org/alias/brigitte-pientka", "id": "ffa902a1-f230-4f09-b858-3bfb3d5d5878", "key": "brigitte-pientka", "name": "Brigitte Pientka" } }, { "alias": { "url": "https://researchr.org/alias/david-thibodeau", "id": "da38559f-12f0-46a6-920e-1f6d62f5be3d", "key": "david-thibodeau", "name": "David Thibodeau" } } ] }, { "type": "inproceedings", "conference": "itp", "conferenceYear": "", "booktitle": "Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010, Edinburgh, UK, July 15, 2010", "volume": "5", "number": "", "series": "EPiC Series", "address": "", "organization": "", "publisher": "EasyChair", "editors": [ { "alias": { "url": "https://researchr.org/alias/ekaterina-komendantskaya", "id": "05bfb549-a57f-486e-8ecf-5490241f0320", "key": "ekaterina-komendantskaya", "name": "Ekaterina Komendantskaya" } }, { "alias": { "url": "https://researchr.org/alias/ana-bove", "id": "32c039ca-56fb-4c4b-95d5-1685a20bcb3c", "key": "ana-bove", "name": "Ana Bove" } }, { "alias": { "url": "https://researchr.org/alias/milad-niqui", "id": "3ec69389-53cb-4ba6-b1cd-faafc7497ac8", "key": "milad-niqui", "name": "Milad Niqui" } } ], "firstpage": 18, "lastpage": 32, "id": "7ce3942e-9c24-46ba-a8eb-aef94eaa1099", "key": "000110-2", "title": "MiniAgda: Integrating Sized and Dependent Types", "month": "", "year": "2010", "doi": "http://www.easychair.org/publications/?page\u003d506004245", "note": "", "abstract": "", "url": "https://researchr.org/publication/000110-2", "authors": [ { "alias": { "url": "https://researchr.org/alias/andreas-abel-0001", "id": "4f66562d-b754-48d7-8d3c-2dc719f48983", "key": "andreas-abel-0001", "name": "Andreas Abel 0001" }, "person": { "url": "https://researchr.org/profile/andreasabel", "id": "7769fdd0-5885-4718-af1d-8942aa05f1b1", "key": "andreasabel", "fullname": "Andreas Abel" } } ] }, { "type": "inproceedings", "conference": "esop", "conferenceYear": "", "booktitle": "Programming Languages and Systems - ESOP 96, 6th European Symposium on Programming, Linköping, Sweden, April 22-24, 1996, Proceedings", "volume": "1058", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/hanne-riis-nielson", "id": "0c1dfffc-4002-488f-abf3-6f404f314536", "key": "hanne-riis-nielson", "name": "Hanne Riis Nielson" } } ], "firstpage": 296, "lastpage": 310, "id": "849c1df1-89ba-4d54-a5d1-f66f33d6cf86", "key": "RohwedderP96", "title": "Mode and Termination Checking for Higher-Order Logic Programs", "month": "", "year": "1996", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/RohwedderP96", "authors": [ { "alias": { "url": "https://researchr.org/alias/ekkehard-rohwedder", "id": "c7427295-a7a4-4581-b611-ed7dd38e1758", "key": "ekkehard-rohwedder", "name": "Ekkehard Rohwedder" } }, { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } } ] }, { "type": "inproceedings", "conference": "sfp", "conferenceYear": "", "booktitle": "Revised Selected Papers from the Sixth Symposium on Trends in Functional Programming, TFP 2005, Tallinn, Estonia, 23-24 September 2005", "volume": "6", "number": "", "series": "Trends in Functional Programming", "address": "", "organization": "", "publisher": "Intellect", "editors": [ { "alias": { "url": "https://researchr.org/alias/marko-c.-j.-d.-van-eekelen", "id": "60f3419a-8c27-4f74-930f-e1a9b1f67b38", "key": "marko-c.-j.-d.-van-eekelen", "name": "Marko C. J. D. van Eekelen" } } ], "firstpage": 79, "lastpage": 94, "id": "8529ce0b-7520-44bb-8b4c-5ad0e7226af0", "key": "ChapmanAM05", "title": "Epigram reloaded: a standalone typechecker for ETT", "month": "", "year": "2005", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/ChapmanAM05", "authors": [ { "alias": { "url": "https://researchr.org/alias/james-chapman", "id": "14413f47-9d55-44a4-822b-6d46a2abf0ba", "key": "james-chapman", "name": "James Chapman" } }, { "alias": { "url": "https://researchr.org/alias/thorsten-altenkirch", "id": "c9045a58-435c-40b0-89f3-70e169445fc6", "key": "thorsten-altenkirch", "name": "Thorsten Altenkirch" }, "person": { "url": "https://researchr.org/profile/thorstenaltenkirch", "id": "f5ded86a-1232-4bee-8be2-c259258a0923", "key": "thorstenaltenkirch", "fullname": "Thorsten Altenkirch" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" }, "person": { "url": "https://researchr.org/profile/conormcbride", "id": "0cbfa47f-c2dd-4b57-a6fd-be876e63cf35", "key": "conormcbride", "fullname": "Conor McBride" } } ] }, { "id": "895c9507-5206-4cd3-8cb2-bac8c3aa1a9e", "key": "ethos-7403", "title": "The theory of LEGO", "month": "", "year": "1995", "doi": "http://ethos.bl.uk/OrderDetails.do?uin\u003duk.bl.ethos.561652", "note": "British Library, EThOS", "abstract": "", "url": "https://researchr.org/publication/ethos-7403", "authors": [ { "alias": { "url": "https://researchr.org/alias/robert-pollack", "id": "9f3b0cb2-688f-48e4-87ae-8072ce373e16", "key": "robert-pollack", "name": "Robert Pollack" } } ] }, { "type": "inproceedings", "conference": "haskell", "conferenceYear": "", "booktitle": "Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, September 22-22, 2004", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/henrik-nilsson", "id": "5fc6541a-a788-4be9-8f37-33d884867bbc", "key": "henrik-nilsson", "name": "Henrik Nilsson" } } ], "firstpage": 1, "lastpage": 9, "id": "8b20c5d3-3b85-4445-86bb-acf5cc7c0cba", "key": "McBrideM04-0", "title": "Functional pearl: I am not a number-I am a free variable", "month": "", "year": "2004", "doi": "http://doi.acm.org/10.1145/1017472.1017477", "note": "", "abstract": "", "url": "https://researchr.org/publication/McBrideM04-0", "authors": [ { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" }, "person": { "url": "https://researchr.org/profile/conormcbride", "id": "0cbfa47f-c2dd-4b57-a6fd-be876e63cf35", "key": "conormcbride", "fullname": "Conor McBride" } }, { "alias": { "url": "https://researchr.org/alias/james-mckinna", "id": "61ec6e7a-4463-43d2-a572-7c698065f43b", "key": "james-mckinna", "name": "James McKinna" } } ] }, { "type": "article", "journal": "Proc. ACM Program. Lang.", "volumenumber": "4", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "8ec68466-521c-404f-9c05-ac9e0966a092", "key": "Kovacs20", "title": "Elaboration with first-class implicit function types", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3408983", "note": "", "abstract": "", "url": "https://researchr.org/publication/Kovacs20", "authors": [ { "alias": { "url": "https://researchr.org/alias/andr%C3%A1s-kov%C3%A1cs", "id": "084a679b-99a3-44e6-97f9-4ffc0b150954", "key": "andrás-kovács", "name": "András Kovács" } } ] }, { "type": "article", "journal": "Sci. Comput. Program.", "volumenumber": "26", "issuenumber": "1-3", "firstpage": 167, "lastpage": 177, "id": "8febe0fb-9b13-4bf2-a010-182c94c830b9", "key": "Coquand96", "title": "An Algorithm for Type-Checking Dependent Types", "month": "", "year": "1996", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Coquand96", "authors": [ { "alias": { "url": "https://researchr.org/alias/thierry-coquand", "id": "4c7d3354-af12-4a8a-b442-9c1af76f0e73", "key": "thierry-coquand", "name": "Thierry Coquand" } } ] }, { "id": "90074f58-696a-41a6-9047-c2206e2a54ab", "key": "hal-8150", "title": "Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique)", "month": "", "year": "2015", "doi": "https://tel.archives-ouvertes.fr/tel-01299180", "note": "", "abstract": "", "url": "https://researchr.org/publication/hal-8150", "authors": [ { "alias": { "url": "https://researchr.org/alias/ronan-saillard", "id": "1c96c14a-58c3-4c04-96a7-a5827fe22dff", "key": "ronan-saillard", "name": "Ronan Saillard" } } ] }, { "type": "article", "journal": "Mathematical Structures in Computer Science", "volumenumber": "29", "issuenumber": "8", "firstpage": 1125, "lastpage": 1150, "id": "90ee2e90-cabf-49b5-aaf1-48f9d29b175f", "key": "GuidiCT19", "title": "Implementing type theory in higher order constraint logic programming", "month": "", "year": "2019", "doi": "https://doi.org/10.1017/S0960129518000427", "note": "", "abstract": "", "url": "https://researchr.org/publication/GuidiCT19", "authors": [ { "alias": { "url": "https://researchr.org/alias/ferruccio-guidi", "id": "8351f06f-e5af-47da-bdf5-227350282505", "key": "ferruccio-guidi", "name": "Ferruccio Guidi" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } } ] }, { "type": "article", "journal": "PACMPL", "volumenumber": "3", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "9123c622-d264-4f4a-9f15-4ac2abf0aa32", "key": "GratzerSB19", "title": "Implementing a modal dependent type theory", "month": "", "year": "2019", "doi": "https://doi.org/10.1145/3341711", "note": "", "abstract": "", "url": "https://researchr.org/publication/GratzerSB19", "authors": [ { "alias": { "url": "https://researchr.org/alias/daniel-gratzer", "id": "034f3ed3-3e16-4523-b57d-029309363d4d", "key": "daniel-gratzer", "name": "Daniel Gratzer" } }, { "alias": { "url": "https://researchr.org/alias/jonathan-sterling", "id": "ddcb80eb-626d-47b9-a59a-58bd5d6f403f", "key": "jonathan-sterling", "name": "Jonathan Sterling" } }, { "alias": { "url": "https://researchr.org/alias/lars-birkedal", "id": "c16494dc-3c68-4385-8493-8aa89be47a08", "key": "lars-birkedal", "name": "Lars Birkedal" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "21", "issuenumber": "4-5", "firstpage": 333, "lastpage": 412, "id": "92839735-9576-4301-8182-ec20ea0cc566", "key": "VytiniotisJSS11", "title": "OutsideIn(X) Modular type inference with local assumptions", "month": "", "year": "2011", "doi": "", "note": "", "abstract": "\r\nAdvanced type system features, such as GADTs, type classes and type families, have proven to be invaluable language extensions for ensuring data invariants and program correctness. Unfortunately, they pose a tough problem for type inference when they are used as local type assumptions. Local type assumptions often result in the lack of principal types and cast the generalisation of local let-bindings prohibitively difficult to implement and specify. User-declared axioms only make this situation worse. In this paper, we explain the problems and – perhaps controversially – argue for abandoning local let-binding generalisation. We give empirical results that local let generalisation is only sporadically used by Haskell programmers. Moving on, we present a novel constraint-based type inference approach for local type assumptions. Our system, called OutsideIn(X), is parameterised over the particular underlying constraint domain X, in the same way as HM(X). This stratification allows us to use a common metatheory and inference algorithm. OutsideIn(X) extends the constraints of X by introducing implication constraints on top. We describe the strategy for solving these implication constraints, which, in turn, relies on a constraint solver for X. We characterise the properties of the constraint solver for X so that the resulting algorithm only accepts programs with principal types, even when the type system specification accepts programs that do not enjoy principal types. Going beyond the general framework, we give a particular constraint solver for X \u003d type classes + GADTs + type families, a non-trivial challenge in its own right. This constraint solver has been implemented and distributed as part of GHC 7.", "url": "https://researchr.org/publication/VytiniotisJSS11", "authors": [ { "alias": { "url": "https://researchr.org/alias/dimitrios-vytiniotis", "id": "264950b5-1355-4834-bf49-b80d535bb435", "key": "dimitrios-vytiniotis", "name": "Dimitrios Vytiniotis" }, "person": { "url": "https://researchr.org/profile/dimitriosvytiniotis", "id": "54e99794-213b-4c45-99e2-88e7f9f98641", "key": "dimitriosvytiniotis", "fullname": "Dimitrios Vytiniotis" } }, { "alias": { "url": "https://researchr.org/alias/simon-l.-peyton-jones", "id": "59fbb17a-d9bb-481a-8767-ea15fd71af8f", "key": "simon-l.-peyton-jones", "name": "Simon L. Peyton Jones" }, "person": { "url": "https://researchr.org/profile/simonlpeytonjones", "id": "45da5dca-2a82-4907-ad77-1278f7b30c9f", "key": "simonlpeytonjones", "fullname": "Simon L. Peyton Jones" } }, { "alias": { "url": "https://researchr.org/alias/tom-schrijvers", "id": "f6239b3a-81b6-4253-bfc9-7c85fca3e839", "key": "tom-schrijvers", "name": "Tom Schrijvers" }, "person": { "url": "https://researchr.org/profile/tomschrijvers", "id": "bfacf374-4141-401e-95a3-c756c195ad81", "key": "tomschrijvers", "fullname": "Tom Schrijvers" } }, { "alias": { "url": "https://researchr.org/alias/martin-sulzmann", "id": "15b1240b-64a1-4d0e-9d31-2aefdcc1147e", "key": "martin-sulzmann", "name": "Martin Sulzmann" } } ] }, { "type": "article", "journal": "", "volumenumber": "", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "94f44727-7ed1-448d-8acc-a272dd9b290d", "key": "norell2007type", "title": "Type checking in the presence of meta-variables", "month": "", "year": "2007", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/norell2007type", "authors": [ { "alias": { "url": "https://researchr.org/alias/norell%2C-ulf", "id": "aea1b28d-3394-4f2e-afc1-244735bfc2d1", "key": "norell,-ulf", "name": "Norell, Ulf" } }, { "alias": { "url": "https://researchr.org/alias/coquand%2C-catarina", "id": "1194670a-9436-4049-a1b6-86f44d68b306", "key": "coquand,-catarina", "name": "Coquand, Catarina" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "Types for Proofs and Programs, International Workshop, TYPES 2006, Nottingham, UK, April 18-21, 2006, Revised Selected Papers", "volume": "4502", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/thorsten-altenkirch", "id": "c9045a58-435c-40b0-89f3-70e169445fc6", "key": "thorsten-altenkirch", "name": "Thorsten Altenkirch" }, "person": { "url": "https://researchr.org/profile/thorstenaltenkirch", "id": "f5ded86a-1232-4bee-8be2-c259258a0923", "key": "thorstenaltenkirch", "fullname": "Thorsten Altenkirch" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" } } ], "firstpage": 18, "lastpage": 32, "id": "992c93af-68e5-4c61-9fad-d88399308472", "key": "AspertiCTZ06", "title": "Crafting a Proof Assistant", "month": "", "year": "2006", "doi": "http://dx.doi.org/10.1007/978-3-540-74464-1_2", "note": "", "abstract": "", "url": "https://researchr.org/publication/AspertiCTZ06", "authors": [ { "alias": { "url": "https://researchr.org/alias/andrea-asperti", "id": "3c4b5963-1e85-449b-ad7e-f3c33cc74f2c", "key": "andrea-asperti", "name": "Andrea Asperti" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } }, { "alias": { "url": "https://researchr.org/alias/stefano-zacchiroli", "id": "7ed9e3e7-f2d6-4975-8c38-8265bf6624f6", "key": "stefano-zacchiroli", "name": "Stefano Zacchiroli" } } ] }, { "type": "article", "journal": "Electr. Notes Theor. Comput. Sci.", "volumenumber": "17", "issuenumber": "", "firstpage": 1, "lastpage": 13, "id": "9c939aea-000d-4ae4-b972-709018e231a6", "key": "PfenningS98", "title": "Algorithms for Equality and Unification in the Presence of Notational Definitions", "month": "", "year": "1998", "doi": "http://www.elsevier.com/gej-ng/31/29/23/41/23/show/Products/notes/index.htt#006", "note": "", "abstract": "", "url": "https://researchr.org/publication/PfenningS98", "authors": [ { "alias": { "url": "https://researchr.org/alias/frank-pfenning", "id": "175f6e28-36d7-4129-904d-43289f98fe7f", "key": "frank-pfenning", "name": "Frank Pfenning" }, "person": { "url": "https://researchr.org/profile/frankpfenning", "id": "7a315cd1-27d5-4981-9ff4-bf2095ea03c1", "key": "frankpfenning", "fullname": "Frank Pfenning" } }, { "alias": { "url": "https://researchr.org/alias/carsten-sch%C3%BCrmann", "id": "ea16dc4f-0420-4ee0-8fe8-949e23113ec5", "key": "carsten-schürmann", "name": "Carsten Schürmann" } } ] }, { "id": "a135c65d-b03d-4eea-8c76-2d60fb0938e5", "key": "Brady2021", "title": "Idris 2: Quantitative Type Theory in Action", "month": "", "year": "2021", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Brady2021", "authors": [ { "alias": { "url": "https://researchr.org/alias/edwin-brady", "id": "071438f4-d83e-481f-973b-9fb75a2a6605", "key": "edwin-brady", "name": "Edwin Brady" } } ] }, { "type": "article", "journal": "", "volumenumber": "", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "a1e2429f-be2b-4a49-b1bf-b3453f82be75", "key": "Asperti2009", "title": "A compact kernel for the calculus of inductive constructions", "month": "", "year": "2009", "doi": "10.1007/s12046-009-0003-3", "note": "", "abstract": "", "url": "https://researchr.org/publication/Asperti2009", "authors": [ { "alias": { "url": "https://researchr.org/alias/a.-asperti", "id": "5d441fa2-7d6e-406a-b214-67877a558f0c", "key": "a.-asperti", "name": "A. Asperti" } }, { "alias": { "url": "https://researchr.org/alias/w.-ricciotti", "id": "91c1e86f-38ee-4ad2-832f-5cf109e4bfb4", "key": "w.-ricciotti", "name": " W. Ricciotti" } }, { "alias": { "url": "https://researchr.org/alias/coen-sacerdoti", "id": "352dec8f-8a05-4702-a3d0-9e5be23fe043", "key": "coen-sacerdoti", "name": " Coen Sacerdoti" } }, { "alias": { "url": "https://researchr.org/alias/e.-tassi", "id": "8c47ff1b-a571-4ac8-a96a-c6d5bb54cde0", "key": "e.-tassi", "name": "E. Tassi" } } ] }, { "type": "inproceedings", "conference": "tphol", "conferenceYear": "", "booktitle": "Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings", "volume": "5674", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/stefan-berghofer", "id": "5f6eb63f-2a76-489a-a618-e40bc6411303", "key": "stefan-berghofer", "name": "Stefan Berghofer" } }, { "alias": { "url": "https://researchr.org/alias/tobias-nipkow", "id": "cd77d116-8911-42a5-ab5a-72d3f868215e", "key": "tobias-nipkow", "name": "Tobias Nipkow" } }, { "alias": { "url": "https://researchr.org/alias/christian-urban", "id": "c842235b-de23-42a4-8d5a-14a0bec36ea8", "key": "christian-urban", "name": "Christian Urban" } }, { "alias": { "url": "https://researchr.org/alias/makarius-wenzel", "id": "9cb20990-0d4b-46f6-a12a-b17f5cb35791", "key": "makarius-wenzel", "name": "Makarius Wenzel" } } ], "firstpage": 84, "lastpage": 98, "id": "a5bd412d-b64a-4e6a-9e2f-9dd2c5ce7767", "key": "AspertiRCT09", "title": "Hints in Unification", "month": "", "year": "2009", "doi": "http://dx.doi.org/10.1007/978-3-642-03359-9_8", "note": "", "abstract": "", "url": "https://researchr.org/publication/AspertiRCT09", "authors": [ { "alias": { "url": "https://researchr.org/alias/andrea-asperti", "id": "3c4b5963-1e85-449b-ad7e-f3c33cc74f2c", "key": "andrea-asperti", "name": "Andrea Asperti" } }, { "alias": { "url": "https://researchr.org/alias/wilmer-ricciotti", "id": "ddeb9a9f-850a-40be-956d-f3f8396e31a9", "key": "wilmer-ricciotti", "name": "Wilmer Ricciotti" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } } ] }, { "type": "article", "journal": "ACM Trans. Program. Lang. Syst.", "volumenumber": "22", "issuenumber": "1", "firstpage": 1, "lastpage": 44, "id": "abbfd40d-5207-4ac4-86b4-d71e8ba1270e", "key": "PierceT-TOPLAS-2000", "title": "Local type inference", "month": "", "year": "2000", "doi": "http://doi.acm.org/10.1145/345099.345100", "note": "", "abstract": "We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code.", "url": "https://researchr.org/publication/PierceT-TOPLAS-2000", "authors": [ { "alias": { "url": "https://researchr.org/alias/benjamin-c.-pierce", "id": "5d9887b3-bd50-4862-87ce-efd6bb07fbd8", "key": "benjamin-c.-pierce", "name": "Benjamin C. Pierce" }, "person": { "url": "https://researchr.org/profile/benjamincpierce", "id": "f83b031e-03b1-4c4f-8e76-b0f63c37357e", "key": "benjamincpierce", "fullname": "Benjamin C. Pierce" } }, { "alias": { "url": "https://researchr.org/alias/david-n.-turner", "id": "ff6a6ce8-9036-4b52-9eaa-b7ce712817ef", "key": "david-n.-turner", "name": "David N. Turner" } } ] }, { "type": "inproceedings", "conference": "cade", "conferenceYear": "", "booktitle": "Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings", "volume": "12699", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/andr%C3%A9-platzer", "id": "e4d96e4d-27ad-44c9-99e3-cbddf04ed052", "key": "andré-platzer", "name": "André Platzer" } }, { "alias": { "url": "https://researchr.org/alias/geoff-sutcliffe", "id": "4ad5af36-9830-4628-874d-6ddb4d54268a", "key": "geoff-sutcliffe", "name": "Geoff Sutcliffe" } } ], "firstpage": 625, "lastpage": 635, "id": "aea83127-043d-408a-b344-07a516f15dc8", "key": "Moura021", "title": "The Lean 4 Theorem Prover and Programming Language", "month": "", "year": "2021", "doi": "https://doi.org/10.1007/978-3-030-79876-5_37", "note": "", "abstract": "", "url": "https://researchr.org/publication/Moura021", "authors": [ { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } }, { "alias": { "url": "https://researchr.org/alias/sebastian-ullrich", "id": "7807da24-f80f-4274-95bd-018d26525119", "key": "sebastian-ullrich", "name": "Sebastian Ullrich" }, "person": { "url": "https://researchr.org/profile/sebastianullrich", "id": "af6a9ce4-253d-4cd1-868e-b26560d5e223", "key": "sebastianullrich", "fullname": "Sebastian Ullrich" } } ] }, { "type": "inproceedings", "conference": "popl", "conferenceYear": "", "booktitle": "Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/sriram-k.-rajamani", "id": "4fd0f460-318d-45b4-8929-663faf53eb8f", "key": "sriram-k.-rajamani", "name": "Sriram K. Rajamani" } }, { "alias": { "url": "https://researchr.org/alias/david-walker", "id": "d785bb26-5233-4896-a2a2-d108e45d7d7a", "key": "david-walker", "name": "David Walker" } } ], "firstpage": 369, "lastpage": 382, "id": "b0730fa7-186d-4ef8-99a3-c4fe69e440e1", "key": "SjobergW15", "title": "Programming up to Congruence", "month": "", "year": "2015", "doi": "http://doi.acm.org/10.1145/2676726.2676974", "note": "", "abstract": "", "url": "https://researchr.org/publication/SjobergW15", "authors": [ { "alias": { "url": "https://researchr.org/alias/vilhelm-sj%C3%B6berg", "id": "b3b88b84-e739-40b8-93fb-b071ee32dad7", "key": "vilhelm-sjöberg", "name": "Vilhelm Sjöberg" } }, { "alias": { "url": "https://researchr.org/alias/stephanie-weirich", "id": "6e5f4081-0f75-4178-a2ec-9822fdb2e8eb", "key": "stephanie-weirich", "name": "Stephanie Weirich" } } ] }, { "type": "inproceedings", "conference": "ppdp", "conferenceYear": "", "booktitle": "Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8-10, 2014", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/olaf-chitil", "id": "3f46156a-72c8-497f-ad2a-57ef2d70e446", "key": "olaf-chitil", "name": "Olaf Chitil" } }, { "alias": { "url": "https://researchr.org/alias/andy-king", "id": "e6fddf8e-fdae-4514-b465-82bac8c19cb1", "key": "andy-king", "name": "Andy King" } }, { "alias": { "url": "https://researchr.org/alias/olivier-danvy", "id": "3b21ff58-79e9-4f14-aedd-63ad4e065625", "key": "olivier-danvy", "name": "Olivier Danvy" }, "person": { "url": "https://researchr.org/profile/olivierdanvy", "id": "e2ae0f9d-8e1c-46c2-9d45-e79bf832af69", "key": "olivierdanvy", "fullname": "Olivier Danvy" } } ], "firstpage": 161, "lastpage": 174, "id": "b1901780-1b2f-4bd1-865f-17cc5420f663", "key": "FerreiraP14-3", "title": "Bidirectional Elaboration of Dependently Typed Programs", "month": "", "year": "2014", "doi": "http://doi.acm.org/10.1145/2643135.2643153", "note": "", "abstract": "", "url": "https://researchr.org/publication/FerreiraP14-3", "authors": [ { "alias": { "url": "https://researchr.org/alias/francisco-ferreira", "id": "50c721da-f306-4aef-9c85-20db711ccf1c", "key": "francisco-ferreira", "name": "Francisco Ferreira" } }, { "alias": { "url": "https://researchr.org/alias/brigitte-pientka", "id": "ffa902a1-f230-4f09-b858-3bfb3d5d5878", "key": "brigitte-pientka", "name": "Brigitte Pientka" } } ] }, { "type": "inproceedings", "booktitle": "A Perspective in Theoretical Computer Science - Commemorative Volume for Gift Siromoney", "volume": "16", "number": "", "series": "World Scientific Series in Computer Science", "address": "", "organization": "", "publisher": "World Scientific", "editors": [ { "alias": { "url": "https://researchr.org/alias/r.-narasimhan", "id": "9108e69d-70e8-4c60-87b4-e8de86c7bf11", "key": "r.-narasimhan", "name": "R. Narasimhan" } } ], "firstpage": 38, "lastpage": 69, "id": "b3b2fb97-f63d-4de1-ba64-0825205f2dbe", "key": "Huet89", "title": "The Constructive Engine", "month": "", "year": "1989", "doi": "http://dx.doi.org/10.1142/9789814368452_0004", "note": "", "abstract": "", "url": "https://researchr.org/publication/Huet89", "authors": [ { "alias": { "url": "https://researchr.org/alias/g%C3%A9rard-huet", "id": "143cc2d9-b7b2-45d3-9b24-a9adcc0718f6", "key": "gérard-huet", "name": "Gérard Huet" } } ] }, { "type": "article", "journal": "CoRR", "volumenumber": "abs/1908.05647", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "bc8f3155-c124-4ecd-b5e7-09ad2ed44227", "key": "DBLP:journals-corr-abs-1908-05647", "title": "Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming", "month": "", "year": "2019", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1908-05647", "authors": [ { "alias": { "url": "https://researchr.org/alias/sebastian-ullrich", "id": "7807da24-f80f-4274-95bd-018d26525119", "key": "sebastian-ullrich", "name": "Sebastian Ullrich" }, "person": { "url": "https://researchr.org/profile/sebastianullrich", "id": "af6a9ce4-253d-4cd1-868e-b26560d5e223", "key": "sebastianullrich", "fullname": "Sebastian Ullrich" } }, { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers", "volume": "3085", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/stefano-berardi", "id": "248bb994-c6dd-4eae-9449-41a92b5fc6bc", "key": "stefano-berardi", "name": "Stefano Berardi" } }, { "alias": { "url": "https://researchr.org/alias/mario-coppo", "id": "60c967a1-7178-46db-945a-72ecdbcd5b01", "key": "mario-coppo", "name": "Mario Coppo" } }, { "alias": { "url": "https://researchr.org/alias/ferruccio-damiani", "id": "913c2d6f-6832-4fed-9560-ad3f0d201188", "key": "ferruccio-damiani", "name": "Ferruccio Damiani" } } ], "firstpage": 115, "lastpage": 129, "id": "c078d5b1-92c9-4879-96c2-849271ff3313", "key": "BradyMM03", "title": "Inductive Families Need Not Store Their Indices", "month": "", "year": "2003", "doi": "http://springerlink.metapress.com/openurl.asp?genre\u003darticle\u0026amp;issn\u003d0302-9743\u0026amp;volume\u003d3085\u0026amp;spage\u003d115", "note": "", "abstract": "", "url": "https://researchr.org/publication/BradyMM03", "authors": [ { "alias": { "url": "https://researchr.org/alias/edwin-brady", "id": "071438f4-d83e-481f-973b-9fb75a2a6605", "key": "edwin-brady", "name": "Edwin Brady" }, "person": { "url": "https://researchr.org/profile/edwinbrady", "id": "deefc76b-14bb-4e95-b2b3-cbb4874ea695", "key": "edwinbrady", "fullname": "Edwin Brady" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" }, "person": { "url": "https://researchr.org/profile/conormcbride", "id": "0cbfa47f-c2dd-4b57-a6fd-be876e63cf35", "key": "conormcbride", "fullname": "Conor McBride" } }, { "alias": { "url": "https://researchr.org/alias/james-mckinna", "id": "61ec6e7a-4463-43d2-a572-7c698065f43b", "key": "james-mckinna", "name": "James McKinna" } } ] }, { "type": "article", "journal": "From Semantics to Computer Science; Essays in Honour of Gilles Kahn", "volumenumber": "", "issuenumber": "", "firstpage": 139, "lastpage": 164, "id": "c3c16f3b-90c7-429e-8232-5c6b5d37dcb7", "key": "coquand2009simple", "title": "A simple type-theoretic language: Mini-TT", "month": "", "year": "2009", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/coquand2009simple", "authors": [ { "alias": { "url": "https://researchr.org/alias/thierry-coquand", "id": "4c7d3354-af12-4a8a-b442-9c1af76f0e73", "key": "thierry-coquand", "name": "Thierry Coquand" } }, { "alias": { "url": "https://researchr.org/alias/yoshiki-kinoshita", "id": "af48ded1-35d7-4f55-a6e8-92836e7a65fd", "key": "yoshiki-kinoshita", "name": "Yoshiki Kinoshita" } }, { "alias": { "url": "https://researchr.org/alias/bengt-nordstr%C3%B6m", "id": "ab6b9fe3-0436-4b14-b609-4c1fb8da44a1", "key": "bengt-nordström", "name": "Bengt Nordström" } }, { "alias": { "url": "https://researchr.org/alias/makoto-takeyama", "id": "b80c531e-fc08-43ce-a7b7-6fdc7e4e7991", "key": "makoto-takeyama", "name": "Makoto Takeyama" } } ] }, { "type": "article", "journal": "Electronic Proceedings in Theoretical Computer Science", "volumenumber": "53", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "c51b74a7-32b8-4e7f-bb7c-8f4e21258313", "key": "SacerdotiCoen2011", "title": "Nonuniform Coercions via Unification Hints", "month": "Mar", "year": "2011", "doi": "10.4204/eptcs.53.2", "note": "", "abstract": "", "url": "https://researchr.org/publication/SacerdotiCoen2011", "authors": [ { "alias": { "url": "https://researchr.org/alias/sacerdoti-coen%2C-claudio", "id": "0f5466cb-d21a-47c7-b24c-25b8878c1b17", "key": "sacerdoti-coen,-claudio", "name": "Sacerdoti Coen, Claudio" } }, { "alias": { "url": "https://researchr.org/alias/tassi%2C-enrico", "id": "c6ffe8da-436f-4a3b-a10d-9eb240492554", "key": "tassi,-enrico", "name": "Tassi, Enrico" } } ] }, { "type": "article", "journal": "Fundam. Inform.", "volumenumber": "102", "issuenumber": "2", "firstpage": 177, "lastpage": 207, "id": "c6afe5e4-9d04-41f6-96fb-499d14d90465", "key": "LohMS10", "title": "A Tutorial Implementation of a Dependently Typed Lambda Calculus", "month": "", "year": "2010", "doi": "http://dx.doi.org/10.3233/FI-2010-304", "note": "", "abstract": "", "url": "https://researchr.org/publication/LohMS10", "authors": [ { "alias": { "url": "https://researchr.org/alias/andres-l%C3%B6h", "id": "b61e18e6-b231-44d5-b663-c06307f81056", "key": "andres-löh", "name": "Andres Löh" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" }, "person": { "url": "https://researchr.org/profile/conormcbride", "id": "0cbfa47f-c2dd-4b57-a6fd-be876e63cf35", "key": "conormcbride", "fullname": "Conor McBride" } }, { "alias": { "url": "https://researchr.org/alias/wouter-swierstra", "id": "3f5edd78-ed16-40b2-9851-a3d170f4b5f4", "key": "wouter-swierstra", "name": "Wouter Swierstra" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "23", "issuenumber": "5", "firstpage": 552, "lastpage": 593, "id": "c7c1064a-ff6b-4718-b001-815351eb62ac", "key": "Brady13-Idris", "title": "Idris, a general-purpose dependently typed programming language: Design and implementation", "month": "", "year": "2013", "doi": "http://dx.doi.org/10.1017/S095679681300018X", "note": "", "abstract": "", "url": "https://researchr.org/publication/Brady13-Idris", "authors": [ { "alias": { "url": "https://researchr.org/alias/edwin-brady", "id": "071438f4-d83e-481f-973b-9fb75a2a6605", "key": "edwin-brady", "name": "Edwin Brady" }, "person": { "url": "https://researchr.org/profile/edwinbrady", "id": "deefc76b-14bb-4e95-b2b3-cbb4874ea695", "key": "edwinbrady", "fullname": "Edwin Brady" } } ] }, { "type": "inproceedings", "conference": "types", "conferenceYear": "", "booktitle": "Types for Proofs and Programs, International Workshop TYPES 93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers", "volume": "806", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/henk-barendregt", "id": "a55061d2-5c56-4fe1-ad9e-72a4a4be3730", "key": "henk-barendregt", "name": "Henk Barendregt" } }, { "alias": { "url": "https://researchr.org/alias/tobias-nipkow", "id": "cd77d116-8911-42a5-ab5a-72d3f868215e", "key": "tobias-nipkow", "name": "Tobias Nipkow" } } ], "firstpage": 19, "lastpage": 61, "id": "c8026008-73bb-49d8-beb6-4c19d1d497e3", "key": "JuttingMP93", "title": "Checking Algorithms for Pure Type Systems", "month": "", "year": "1993", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/JuttingMP93", "authors": [ { "alias": { "url": "https://researchr.org/alias/l.-s.-van-benthem-jutting", "id": "5207c76e-b8ac-4b7e-a2f2-b9de8b166b10", "key": "l.-s.-van-benthem-jutting", "name": "L. S. van Benthem Jutting" } }, { "alias": { "url": "https://researchr.org/alias/james-mckinna", "id": "61ec6e7a-4463-43d2-a572-7c698065f43b", "key": "james-mckinna", "name": "James McKinna" } }, { "alias": { "url": "https://researchr.org/alias/robert-pollack", "id": "9f3b0cb2-688f-48e4-87ae-8072ce373e16", "key": "robert-pollack", "name": "Robert Pollack" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "27", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "ca969c2f-8bf2-4f4f-8481-4ea9cedc4006", "key": "ZilianiS17", "title": "A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading", "month": "", "year": "2017", "doi": "http://dx.doi.org/10.1017/S0956796817000028", "note": "", "abstract": "", "url": "https://researchr.org/publication/ZilianiS17", "authors": [ { "alias": { "url": "https://researchr.org/alias/beta-ziliani", "id": "afd45095-08cd-4ac9-bbcc-2a46fb13501f", "key": "beta-ziliani", "name": "Beta Ziliani" } }, { "alias": { "url": "https://researchr.org/alias/matthieu-sozeau", "id": "915a6b4d-ac46-409a-b405-1e31079029ee", "key": "matthieu-sozeau", "name": "Matthieu Sozeau" } } ] }, { "type": "inproceedings", "conference": "pldi", "conferenceYear": "", "booktitle": "PLDI \u002721: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 20211", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/stephen-n.-freund", "id": "c04ddd17-5c51-4850-8292-ffca5fab1499", "key": "stephen-n.-freund", "name": "Stephen N. Freund" } }, { "alias": { "url": "https://researchr.org/alias/eran-yahav", "id": "0fb9d877-e8c3-4a0b-94cb-2011bdc4a3d5", "key": "eran-yahav", "name": "Eran Yahav" } } ], "firstpage": 158, "lastpage": 174, "id": "cc506de2-3406-40cd-83b4-d6555adc73f0", "key": "SammlerLKMD021", "title": "RefinedC: automating the foundational verification of C code with refined ownership types", "month": "", "year": "2021", "doi": "https://doi.org/10.1145/3453483.3454036", "note": "", "abstract": "", "url": "https://researchr.org/publication/SammlerLKMD021", "authors": [ { "alias": { "url": "https://researchr.org/alias/michael-sammler", "id": "9228d961-c332-41e4-9d28-d84dacca7752", "key": "michael-sammler", "name": "Michael Sammler" } }, { "alias": { "url": "https://researchr.org/alias/rodolphe-lepigre", "id": "f7fb9b24-1a56-43cf-b878-79bb6ae248cb", "key": "rodolphe-lepigre", "name": "Rodolphe Lepigre" } }, { "alias": { "url": "https://researchr.org/alias/robbert-krebbers", "id": "4af5e5e8-154a-4c27-bd7e-8698e988adfd", "key": "robbert-krebbers", "name": "Robbert Krebbers" } }, { "alias": { "url": "https://researchr.org/alias/kayvan-memarian", "id": "706a68bb-12be-4895-88dc-f02e701918b1", "key": "kayvan-memarian", "name": "Kayvan Memarian" } }, { "alias": { "url": "https://researchr.org/alias/derek-dreyer", "id": "f0b63475-1479-452c-b944-30b8b783767c", "key": "derek-dreyer", "name": "Derek Dreyer" } }, { "alias": { "url": "https://researchr.org/alias/deepak-garg-0001", "id": "a934040a-806d-437b-a587-ecae5193719d", "key": "deepak-garg-0001", "name": "Deepak Garg 0001" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "13", "issuenumber": "2", "firstpage": 295, "lastpage": 316, "id": "cc510761-fca2-47e7-b90d-7b108031bb65", "key": "LevinP03", "title": "TinkerType: a language for playing with formal systems", "month": "", "year": "2003", "doi": "http://dx.doi.org/10.1017/S0956796802004550", "note": "", "abstract": "TinkerType is a pragmatic framework for compact and modular description of formal systems (type systems, operational semantics, logics, etc.). A family of related systems is broken down into a set of clauses – individual inference rules – and a set of features controlling the inclusion of clauses in particular systems. Simple static checks are used to help maintain consistency of the generated systems. We present TinkerType and its implementation and describe its application to two substantial repositories of typed lambda-calculi. The first repository covers a broad range of typing features, including subtyping, polymorphism, type operators and kinding, computational effects, and dependent types. It describes both declarative and algorithmic aspects of the systems, and can be used with our tool, the TinkerType Assembler, to generate calculi either in the form of typeset collections of inference rules or as executable ML typecheckers. The second repository addresses a smaller collection of systems, and provides modularized proofs of basic safety properties.", "url": "https://researchr.org/publication/LevinP03", "authors": [ { "alias": { "url": "https://researchr.org/alias/michael-y.-levin", "id": "c7c6fff2-c9c1-401a-87bc-c474f9fbb640", "key": "michael-y.-levin", "name": "Michael Y. Levin" } }, { "alias": { "url": "https://researchr.org/alias/benjamin-c.-pierce", "id": "5d9887b3-bd50-4862-87ce-efd6bb07fbd8", "key": "benjamin-c.-pierce", "name": "Benjamin C. Pierce" }, "person": { "url": "https://researchr.org/profile/benjamincpierce", "id": "f83b031e-03b1-4c4f-8e76-b0f63c37357e", "key": "benjamincpierce", "fullname": "Benjamin C. Pierce" } } ] }, { "type": "article", "journal": "PACMPL", "volumenumber": "1", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "cf1e91eb-6af0-4d09-a5cc-de674adb7969", "key": "EbnerURAM17", "title": "A metaprogramming framework for formal verification", "month": "", "year": "2017", "doi": "http://doi.acm.org/10.1145/3110278", "note": "", "abstract": "", "url": "https://researchr.org/publication/EbnerURAM17", "authors": [ { "alias": { "url": "https://researchr.org/alias/gabriel-ebner", "id": "507d6741-034b-4fce-bc27-5b9eb329f290", "key": "gabriel-ebner", "name": "Gabriel Ebner" } }, { "alias": { "url": "https://researchr.org/alias/sebastian-ullrich", "id": "7807da24-f80f-4274-95bd-018d26525119", "key": "sebastian-ullrich", "name": "Sebastian Ullrich" }, "person": { "url": "https://researchr.org/profile/sebastianullrich", "id": "af6a9ce4-253d-4cd1-868e-b26560d5e223", "key": "sebastianullrich", "fullname": "Sebastian Ullrich" } }, { "alias": { "url": "https://researchr.org/alias/jared-roesch", "id": "d9d442b5-1d9c-45cf-96ed-19a010a90438", "key": "jared-roesch", "name": "Jared Roesch" } }, { "alias": { "url": "https://researchr.org/alias/jeremy-avigad", "id": "8b346f05-14af-47dd-a45a-f21dfacc60ad", "key": "jeremy-avigad", "name": "Jeremy Avigad" } }, { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } } ] }, { "type": "inproceedings", "conference": "itp", "conferenceYear": "", "booktitle": "Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings", "volume": "8558", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/gerwin-klein", "id": "a5a9deaf-ca41-4193-99f6-416c66c30bd2", "key": "gerwin-klein", "name": "Gerwin Klein" } }, { "alias": { "url": "https://researchr.org/alias/ruben-gamboa", "id": "8177c038-718d-4128-9b37-5170e8f20837", "key": "ruben-gamboa", "name": "Ruben Gamboa" } } ], "firstpage": 499, "lastpage": 514, "id": "d4924628-dc95-4841-9d4c-f5283cc50b74", "key": "SozeauT14", "title": "Universe Polymorphism in Coq", "month": "", "year": "2014", "doi": "http://dx.doi.org/10.1007/978-3-319-08970-6_32", "note": "", "abstract": "", "url": "https://researchr.org/publication/SozeauT14", "authors": [ { "alias": { "url": "https://researchr.org/alias/matthieu-sozeau", "id": "915a6b4d-ac46-409a-b405-1e31079029ee", "key": "matthieu-sozeau", "name": "Matthieu Sozeau" } }, { "alias": { "url": "https://researchr.org/alias/nicolas-tabareau", "id": "a5fc85c1-5274-4b6b-9fcc-bad6ef290711", "key": "nicolas-tabareau", "name": "Nicolas Tabareau" } } ] }, { "id": "d4fcbccf-1e33-4c51-9087-f728c63cb582", "key": "Gundry2012", "title": "A tutorial implementation of dynamic pattern unification: A dependently typed programming language implementation pearl", "month": "", "year": "2012", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Gundry2012", "authors": [ { "alias": { "url": "https://researchr.org/alias/adam-gundry", "id": "1e8b8469-910b-47ca-9da7-cd1797d252d8", "key": "adam-gundry", "name": "Adam Gundry" } }, { "alias": { "url": "https://researchr.org/alias/conor-mcbride", "id": "9a2d88ee-c553-4be4-86b4-26ffe23d33ed", "key": "conor-mcbride", "name": "Conor McBride" }, "person": { "url": "https://researchr.org/profile/conormcbride", "id": "0cbfa47f-c2dd-4b57-a6fd-be876e63cf35", "key": "conormcbride", "fullname": "Conor McBride" } } ] }, { "id": "d607bbb9-1810-4d9a-ad58-c807844ef451", "key": "Eisenberg2021", "title": "An Existential Crisis Resolved: Type inference for first-class existential types ", "month": "", "year": "2021", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Eisenberg2021", "authors": [ { "alias": { "url": "https://researchr.org/alias/richard-a.-eisenberg", "id": "351698b7-ddbf-44ca-969a-00ba578a305f", "key": "richard-a.-eisenberg", "name": "Richard A. Eisenberg" } }, { "alias": { "url": "https://researchr.org/alias/guillaume-duboc", "id": "12d10dce-d213-4fb3-8d17-f8f9fe4be111", "key": "guillaume-duboc", "name": " Guillaume Duboc" } }, { "alias": { "url": "https://researchr.org/alias/stephanie-weirich", "id": "6e5f4081-0f75-4178-a2ec-9822fdb2e8eb", "key": "stephanie-weirich", "name": "Stephanie Weirich" } }, { "alias": { "url": "https://researchr.org/alias/daniel-lee", "id": "0737265f-9b35-4b74-a3d6-ae52f7046196", "key": "daniel-lee", "name": "Daniel Lee" } } ] }, { "type": "article", "journal": "Logical frameworks", "volumenumber": "1", "issuenumber": "", "firstpage": 255, "lastpage": 279, "id": "d61d9a3e-32e3-4150-bd57-cfe778206770", "key": "coquand1991algorithm", "title": "An algorithm for testing conversion in type theory", "month": "", "year": "1991", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/coquand1991algorithm", "authors": [ { "alias": { "url": "https://researchr.org/alias/coquand%2C-thierry", "id": "f53e8184-2ba8-44de-9519-fe82813bd391", "key": "coquand,-thierry", "name": "Coquand, Thierry" } } ] }, { "type": "article", "journal": "Log. Methods Comput. Sci.", "volumenumber": "8", "issuenumber": "1", "firstpage": 0, "lastpage": 0, "id": "da649782-7197-4b78-8812-f10660ca5159", "key": "DBLP:journals-corr-abs-1202-4905", "title": "A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions", "month": "", "year": "2012", "doi": "10.2168/LMCS-8(1:18)2012", "note": "", "abstract": "", "url": "https://researchr.org/publication/DBLP%3Ajournals-corr-abs-1202-4905", "authors": [ { "alias": { "url": "https://researchr.org/alias/andrea-asperti", "id": "3c4b5963-1e85-449b-ad7e-f3c33cc74f2c", "key": "andrea-asperti", "name": "Andrea Asperti" } }, { "alias": { "url": "https://researchr.org/alias/wilmer-ricciotti", "id": "ddeb9a9f-850a-40be-956d-f3f8396e31a9", "key": "wilmer-ricciotti", "name": "Wilmer Ricciotti" } }, { "alias": { "url": "https://researchr.org/alias/claudio-sacerdoti-coen", "id": "f4f960e1-9117-4ba8-9dd8-d6b343c0251e", "key": "claudio-sacerdoti-coen", "name": "Claudio Sacerdoti Coen" } }, { "alias": { "url": "https://researchr.org/alias/enrico-tassi", "id": "7adb9678-d0e4-4325-86a7-5313c26bcba9", "key": "enrico-tassi", "name": "Enrico Tassi" } } ] }, { "type": "article", "journal": "Proc. ACM Program. Lang.", "volumenumber": "4", "issuenumber": "ICFP", "firstpage": 0, "lastpage": 0, "id": "de5b48d0-ff55-4619-beb2-6e5e4e5e87e7", "key": "SerranoHJV20", "title": "A quick look at impredicativity", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3408971", "note": "", "abstract": "", "url": "https://researchr.org/publication/SerranoHJV20", "authors": [ { "alias": { "url": "https://researchr.org/alias/alejandro-serrano-0001", "id": "0ebc9e59-de62-4a4f-a3ef-04b23af9673a", "key": "alejandro-serrano-0001", "name": "Alejandro Serrano 0001" } }, { "alias": { "url": "https://researchr.org/alias/jurriaan-hage", "id": "3d9f2653-40e3-4c79-b969-d9f4834a083f", "key": "jurriaan-hage", "name": "Jurriaan Hage" } }, { "alias": { "url": "https://researchr.org/alias/simon-peyton-jones", "id": "736004e6-c73f-480b-9613-910e2b75f32f", "key": "simon-peyton-jones", "name": "Simon Peyton Jones" } }, { "alias": { "url": "https://researchr.org/alias/dimitrios-vytiniotis", "id": "264950b5-1355-4834-bf49-b80d535bb435", "key": "dimitrios-vytiniotis", "name": "Dimitrios Vytiniotis" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "23", "issuenumber": "1", "firstpage": 1, "lastpage": 37, "id": "df8ad83a-a40f-454c-bef9-479285ea9a86", "key": "Pientka13", "title": "An insider\u0027s look at LF type reconstruction: everything you (n)ever wanted to know", "month": "", "year": "2013", "doi": "http://dx.doi.org/10.1017/S0956796812000408", "note": "", "abstract": "", "url": "https://researchr.org/publication/Pientka13", "authors": [ { "alias": { "url": "https://researchr.org/alias/brigitte-pientka", "id": "ffa902a1-f230-4f09-b858-3bfb3d5d5878", "key": "brigitte-pientka", "name": "Brigitte Pientka" } } ] }, { "type": "inproceedings", "conference": "cpp", "conferenceYear": "", "booktitle": "Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/assia-mahboubi", "id": "ef2599ee-5dfe-4331-9e65-f4f588174e93", "key": "assia-mahboubi", "name": "Assia Mahboubi" } }, { "alias": { "url": "https://researchr.org/alias/magnus-o.-myreen", "id": "f13fe7f1-af0c-46df-af4b-599f18569829", "key": "magnus-o.-myreen", "name": "Magnus O. Myreen" } } ], "firstpage": 166, "lastpage": 180, "id": "e4b05c9b-6104-449f-a5c9-951f1ddd8ce2", "key": "StarkSK19", "title": "Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutions", "month": "", "year": "2019", "doi": "https://doi.org/10.1145/3293880.3294101", "note": "", "abstract": "", "url": "https://researchr.org/publication/StarkSK19", "authors": [ { "alias": { "url": "https://researchr.org/alias/kathrin-stark", "id": "57ee14ce-17d0-49da-9969-ce64c736d159", "key": "kathrin-stark", "name": "Kathrin Stark" } }, { "alias": { "url": "https://researchr.org/alias/steven-sch%C3%A4fer", "id": "fb52f5d8-6bf0-4ebe-bcca-74f61284683f", "key": "steven-schäfer", "name": "Steven Schäfer" } }, { "alias": { "url": "https://researchr.org/alias/jonas-kaiser", "id": "6b3263af-e63c-4175-b401-f63e80f3ad5c", "key": "jonas-kaiser", "name": "Jonas Kaiser" } } ] }, { "type": "article", "journal": "J. Funct. Program.", "volumenumber": "30", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "e4eafee4-05c8-4406-a807-ccc9b74a0528", "key": "CockxA20", "title": "Elaborating dependent (co)pattern matching: No pattern left behind", "month": "", "year": "2020", "doi": "https://doi.org/10.1017/S0956796819000182", "note": "", "abstract": "", "url": "https://researchr.org/publication/CockxA20", "authors": [ { "alias": { "url": "https://researchr.org/alias/jesper-cockx", "id": "379545f4-fdfd-42b3-8892-9a73768dbaba", "key": "jesper-cockx", "name": "Jesper Cockx" }, "person": { "url": "https://researchr.org/profile/jespercockx", "id": "46dd4d29-926d-4723-bd06-81f3726e7558", "key": "jespercockx", "fullname": "Jesper Cockx" } }, { "alias": { "url": "https://researchr.org/alias/andreas-abel-0001", "id": "4f66562d-b754-48d7-8d3c-2dc719f48983", "key": "andreas-abel-0001", "name": "Andreas Abel 0001" }, "person": { "url": "https://researchr.org/profile/andreasabel", "id": "7769fdd0-5885-4718-af1d-8942aa05f1b1", "key": "andreasabel", "fullname": "Andreas Abel" } } ] }, { "type": "inproceedings", "conference": "icfp", "conferenceYear": "", "booktitle": "Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/kathleen-fisher", "id": "e0e131f2-6a9a-4b6c-804b-058cdfb5d2e2", "key": "kathleen-fisher", "name": "Kathleen Fisher" } }, { "alias": { "url": "https://researchr.org/alias/john-h.-reppy", "id": "cbd6dce9-1d8e-44f3-9aa8-496429609329", "key": "john-h.-reppy", "name": "John H. Reppy" } } ], "firstpage": 424, "lastpage": 436, "id": "e504166e-7c8f-431a-8aa1-3bf2d0ac117a", "key": "KarachaliasSVJ15", "title": "GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and laziness", "month": "", "year": "2015", "doi": "http://doi.acm.org/10.1145/2784731.2784748", "note": "", "abstract": "", "url": "https://researchr.org/publication/KarachaliasSVJ15", "authors": [ { "alias": { "url": "https://researchr.org/alias/georgios-karachalias", "id": "357131c8-0996-4465-9615-4e043acf9ffd", "key": "georgios-karachalias", "name": "Georgios Karachalias" } }, { "alias": { "url": "https://researchr.org/alias/tom-schrijvers", "id": "f6239b3a-81b6-4253-bfc9-7c85fca3e839", "key": "tom-schrijvers", "name": "Tom Schrijvers" } }, { "alias": { "url": "https://researchr.org/alias/dimitrios-vytiniotis", "id": "264950b5-1355-4834-bf49-b80d535bb435", "key": "dimitrios-vytiniotis", "name": "Dimitrios Vytiniotis" } }, { "alias": { "url": "https://researchr.org/alias/simon-l.-peyton-jones", "id": "59fbb17a-d9bb-481a-8767-ea15fd71af8f", "key": "simon-l.-peyton-jones", "name": "Simon L. Peyton Jones" }, "person": { "url": "https://researchr.org/profile/simonlpeytonjones", "id": "45da5dca-2a82-4907-ad77-1278f7b30c9f", "key": "simonlpeytonjones", "fullname": "Simon L. Peyton Jones" } } ] }, { "type": "article", "journal": "CoRR", "volumenumber": "abs/2001.04301", "issuenumber": "", "firstpage": 0, "lastpage": 0, "id": "eaf4e77c-610a-4b12-b2bd-d4cfdc74cf0f", "key": "DBLP:journals-corr-abs-2001-04301", "title": "Tabled Typeclass Resolution", "month": "", "year": "2020", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/DBLP%3Ajournals-corr-abs-2001-04301", "authors": [ { "alias": { "url": "https://researchr.org/alias/daniel-selsam", "id": "3cb8c492-9382-4399-9cf4-ff32bdbb37b5", "key": "daniel-selsam", "name": "Daniel Selsam" } }, { "alias": { "url": "https://researchr.org/alias/sebastian-ullrich", "id": "7807da24-f80f-4274-95bd-018d26525119", "key": "sebastian-ullrich", "name": "Sebastian Ullrich" }, "person": { "url": "https://researchr.org/profile/sebastianullrich", "id": "af6a9ce4-253d-4cd1-868e-b26560d5e223", "key": "sebastianullrich", "fullname": "Sebastian Ullrich" } }, { "alias": { "url": "https://researchr.org/alias/leonardo-de-moura", "id": "1da7fc11-0c67-416b-ad3f-975b2266dcba", "key": "leonardo-de-moura", "name": "Leonardo de Moura" } } ] }, { "type": "article", "journal": "J. Autom. Reasoning", "volumenumber": "29", "issuenumber": "3-4", "firstpage": 365, "lastpage": 387, "id": "ebcfba5f-dbd0-4bbd-90a3-913a00834920", "key": "Wiedijk02", "title": "A New Implementation of Automath", "month": "", "year": "2002", "doi": "", "note": "", "abstract": "", "url": "https://researchr.org/publication/Wiedijk02", "authors": [ { "alias": { "url": "https://researchr.org/alias/freek-wiedijk", "id": "2ef046b6-83ff-4cef-b08b-94867fcf46fd", "key": "freek-wiedijk", "name": "Freek Wiedijk" }, "person": { "url": "https://researchr.org/profile/freekwiedijk", "id": "09c27b39-7abb-45ea-afd0-1e55e99b76b2", "key": "freekwiedijk", "fullname": "Freek Wiedijk" } } ] }, { "type": "inproceedings", "conference": "itp", "conferenceYear": "", "booktitle": "Interactive Theorem Proving - 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings", "volume": "9236", "number": "", "series": "Lecture Notes in Computer Science", "address": "", "organization": "", "publisher": "Springer", "editors": [ { "alias": { "url": "https://researchr.org/alias/christian-urban", "id": "c842235b-de23-42a4-8d5a-14a0bec36ea8", "key": "christian-urban", "name": "Christian Urban" } }, { "alias": { "url": "https://researchr.org/alias/xingyuan-zhang", "id": "df557d4c-bcaf-40f4-9ac4-b3d9ff362a75", "key": "xingyuan-zhang", "name": "Xingyuan Zhang" } } ], "firstpage": 359, "lastpage": 374, "id": "ed1da482-0d69-44ad-b521-33f3dcd9f3e5", "key": "SchaferTS15", "title": "Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions", "month": "", "year": "2015", "doi": "http://dx.doi.org/10.1007/978-3-319-22102-1_24", "note": "", "abstract": "", "url": "https://researchr.org/publication/SchaferTS15", "authors": [ { "alias": { "url": "https://researchr.org/alias/steven-sch%C3%A4fer", "id": "fb52f5d8-6bf0-4ebe-bcca-74f61284683f", "key": "steven-schäfer", "name": "Steven Schäfer" } }, { "alias": { "url": "https://researchr.org/alias/tobias-tebbi", "id": "13fd6f28-af3b-4fdd-9580-2937cfe8c811", "key": "tobias-tebbi", "name": "Tobias Tebbi" } }, { "alias": { "url": "https://researchr.org/alias/gert-smolka", "id": "c4c13ba6-1080-4e36-b3a1-6ad57af85b9d", "key": "gert-smolka", "name": "Gert Smolka" } } ] }, { "type": "article", "journal": "Proc. ACM Program. Lang.", "volumenumber": "4", "issuenumber": "OOPSLA", "firstpage": 0, "lastpage": 0, "id": "ef607395-f6cc-49ff-aff2-efbb687e3fa6", "key": "RouvoetAPKV20", "title": "Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3428248", "note": "", "abstract": "There is a large gap between the specification of type systems and the implementation of their type checkers,\r\nwhich impedes reasoning about the soundness of the type checker with respect to the specification. A\r\nvision to close this gap is to automatically obtain type checkers from declarative programming language\r\nspecifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages\r\nto a single correctness proof for the specification language. This vision is obstructed by an aspect common\r\nto all programming languages: name resolution. Naming and scoping are pervasive and complex aspects\r\nof the static semantics of programming languages. Implementations of type checkers for languages with\r\nname binding features such as modules, imports, classes, and inheritance interleave collection of binding\r\ninformation (i.e., declarations, scoping structure, and imports) and querying that information. This requires\r\nscheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after\r\nall relevant binding structure has been collected. Type checkers for concrete languages accomplish stability\r\nusing language-specific knowledge about the type system.\r\n\r\nIn this paper we give a language-independent characterization of necessary and sufficient conditions to\r\nguarantee stability of name and type queries during type checking in terms of critical edges in an incomplete\r\nscope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing\r\ninformation. This yields type checkers for the specified languages that are sound by construction—i.e., they\r\nschedule queries so that the answers are stable, and only accept programs that are name- and type-correct\r\naccording to the declarative language specification. We implement this approach, and evaluate it against\r\nspecifications of a small module and record language, as well as subsets of Java and Scala.", "url": "https://researchr.org/publication/RouvoetAPKV20", "authors": [ { "alias": { "url": "https://researchr.org/alias/arjen-rouvoet", "id": "fc775c60-38ca-474a-9b64-bf22b7f332ab", "key": "arjen-rouvoet", "name": "Arjen Rouvoet" }, "person": { "url": "https://researchr.org/profile/arjenrouvoet", "id": "467ce72b-6a13-4307-92b5-63517f8cd7e4", "key": "arjenrouvoet", "fullname": "Arjen Rouvoet" } }, { "alias": { "url": "https://researchr.org/alias/hendrik-van-antwerpen", "id": "5635cc9f-d3f1-48bc-978b-7a9333184b9b", "key": "hendrik-van-antwerpen", "name": "Hendrik van Antwerpen" } }, { "alias": { "url": "https://researchr.org/alias/casper-bach-poulsen", "id": "d86c748b-3c68-4b5c-97f3-6b10587b35de", "key": "casper-bach-poulsen", "name": "Casper Bach Poulsen" }, "person": { "url": "https://researchr.org/profile/casperbachpoulsen", "id": "639f2dee-ca9e-47c1-b3ce-658b5a12b017", "key": "casperbachpoulsen", "fullname": "Casper Bach Poulsen" } }, { "alias": { "url": "https://researchr.org/alias/robbert-krebbers", "id": "4af5e5e8-154a-4c27-bd7e-8698e988adfd", "key": "robbert-krebbers", "name": "Robbert Krebbers" } }, { "alias": { "url": "https://researchr.org/alias/eelco-visser", "id": "f68ba0ee-899e-4c4c-9d8a-6fed5092830a", "key": "eelco-visser", "name": "Eelco Visser" }, "person": { "url": "https://researchr.org/profile/eelcovisser", "id": "f0fbf7c0-9729-4ec8-b3c9-5f30dbd9614b", "key": "eelcovisser", "fullname": "Eelco Visser" } } ] }, { "type": "inproceedings", "conference": "icfp", "conferenceYear": "", "booktitle": "Proceedings of the 5th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2020, Virtual Event, USA, August 23, 2020", "volume": "", "number": "", "series": "", "address": "", "organization": "", "publisher": "ACM", "editors": [ { "alias": { "url": "https://researchr.org/alias/james-mckinna", "id": "61ec6e7a-4463-43d2-a572-7c698065f43b", "key": "james-mckinna", "name": "James McKinna" } }, { "alias": { "url": "https://researchr.org/alias/cyrus-omar", "id": "45892369-36b3-42d1-ad85-5e703d49f652", "key": "cyrus-omar", "name": "Cyrus Omar" } } ], "firstpage": 11, "lastpage": 23, "id": "f1bbf007-2e96-4ac3-8a31-c9e08115bcd5", "key": "JuanD20", "title": "Practical dependent type checking using twin types", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3406089.3409030", "note": "", "abstract": "", "url": "https://researchr.org/publication/JuanD20", "authors": [ { "alias": { "url": "https://researchr.org/alias/v%C3%ADctor-l%C3%B3pez-juan", "id": "a7ad0067-f02e-4996-be0e-697afc801d02", "key": "víctor-lópez-juan", "name": "Víctor López Juan" } }, { "alias": { "url": "https://researchr.org/alias/nils-anders-danielsson", "id": "8b58a10d-0854-4ed5-bea6-45999080e21f", "key": "nils-anders-danielsson", "name": "Nils Anders Danielsson" } } ] }, { "type": "article", "journal": "PACMPL", "volumenumber": "4", "issuenumber": "POPL", "firstpage": 0, "lastpage": 0, "id": "f8ac3947-5366-4c4f-9cc2-ed7ef9c7de8b", "key": "ChangBTB20", "title": "Dependent type systems as macros", "month": "", "year": "2020", "doi": "https://doi.org/10.1145/3371071", "note": "", "abstract": "", "url": "https://researchr.org/publication/ChangBTB20", "authors": [ { "alias": { "url": "https://researchr.org/alias/stephen-chang", "id": "d013787e-916b-4dcd-9f3d-18669b386e19", "key": "stephen-chang", "name": "Stephen Chang" } }, { "alias": { "url": "https://researchr.org/alias/michael-ballantyne", "id": "df088358-9ff5-4ea2-83f2-18edd8e5107f", "key": "michael-ballantyne", "name": "Michael Ballantyne" } }, { "alias": { "url": "https://researchr.org/alias/milo-turner", "id": "e875d72d-fe77-4786-af04-eaffadc15a4d", "key": "milo-turner", "name": "Milo Turner" } }, { "alias": { "url": "https://researchr.org/alias/william-j.-bowman", "id": "8f8fd933-3135-4d09-a2f6-7dde2ff08a37", "key": "william-j.-bowman", "name": "William J. Bowman" } } ] } ] }