{"data":{"id":"10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f","type":"dois","attributes":{"doi":"10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f","prefix":"10.4121","suffix":"6f239149-2526-42a0-8d07-d0e9d6714f7f","identifiers":[],"alternateIdentifiers":[],"creators":[{"name":"Liesnikov, Bohdan","nameType":"Personal","givenName":"Bohdan","familyName":"Liesnikov","nameIdentifiers":[{"nameIdentifier":"0009-0000-2216-8830","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]},{"name":"Cockx, Jesper","givenName":"Jesper","familyName":"Cockx","affiliation":[],"nameIdentifiers":[]}],"titles":[{"title":"Code underlying the publication: Building a Correct-By-Construction Type Checker for a Dependently Typed Core Language"}],"publisher":"4TU.ResearchData","container":{},"publicationYear":2024,"subjects":[{"subject":"Computer Software","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"0803"},{"subject":"FOS: Computer and information sciences","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"Information and Computing Sciences","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"08"},{"subject":"dependent types"},{"subject":"core language"},{"subject":"type theory"},{"subject":"typechecking"},{"subject":"type-checking"}],"contributors":[{"name":"TU Delft, Faculty Of Electrical Engineering, Mathematics And Computer Science, Department Of Software Technology ","nameType":"Organizational","affiliation":[],"contributorType":"Other","nameIdentifiers":[]}],"dates":[{"date":"2024-10-31","dateType":"Issued"}],"language":"en","types":{"ris":"COMP","bibtex":"misc","citeproc":"article","schemaOrg":"SoftwareSourceCode","resourceType":"Software","resourceTypeGeneral":"Software"},"relatedIdentifiers":[{"relationType":"IsSupplementTo","relatedIdentifier":"10.1007/978-981-97-8943-6_4","relatedIdentifierType":"DOI"},{"relationType":"References","relatedIdentifier":"https://conf.researchr.org/details/aplas-2024/aplas-2024-research-papers/13/Building-A-Correct-By-Construction-Type-Checker-for-a-Dependently-Typed-Core-Language","relatedIdentifierType":"URL"}],"relatedItems":[],"sizes":[],"formats":["git repository cotaining an Agda project, built using nix"],"version":"2","rightsList":[{"rights":"Creative Commons Zero v1.0 Universal","rightsUri":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","schemeUri":"https://spdx.org/licenses/","rightsIdentifier":"cc0-1.0","rightsIdentifierScheme":"SPDX"}],"descriptions":[{"description":"This repository contains source code for the paper. We develop a correct-by-construction typechecker for a subset of Agda's internal language. This code assumes that the input has already been scope-checked and is presented to the core in a well-scoped form. The typechecker uses erasure extensively and doesn't develop any meta-theory, relying on the typing rules as the source of truth. The implementation was developed by the authors of the paper through 2023 and 2024.","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[{"awardTitle":"A trustworthy and extensible core language for Agda","funderName":"NWO","awardNumber":"VI.Veni.202.216 "}],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjQvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40MTIxLzZGMjM5MTQ5LTI1MjYtNDJBMC04RDA3LUQwRTlENjcxNEY3RjwvaWRlbnRpZmllcj4KICA8Y3JlYXRvcnM+CiAgICA8Y3JlYXRvcj4KICAgICAgPGNyZWF0b3JOYW1lIG5hbWVUeXBlPSJQZXJzb25hbCI+Qm9oZGFuIExpZXNuaWtvdjwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+Qm9oZGFuPC9naXZlbk5hbWU+CiAgICAgIDxmYW1pbHlOYW1lPkxpZXNuaWtvdjwvZmFtaWx5TmFtZT4KICAgICAgPG5hbWVJZGVudGlmaWVyIG5hbWVJZGVudGlmaWVyU2NoZW1lPSJodHRwczovL29yY2lkLm9yZy8iPjAwMDktMDAwMC0yMjE2LTg4MzA8L25hbWVJZGVudGlmaWVyPgogICAgPC9jcmVhdG9yPgogICAgPGNyZWF0b3I+CiAgICAgIDxjcmVhdG9yTmFtZT5KZXNwZXIgQ29ja3g8L2NyZWF0b3JOYW1lPgogICAgICA8Z2l2ZW5OYW1lPkplc3BlcjwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5Db2NreDwvZmFtaWx5TmFtZT4KICAgIDwvY3JlYXRvcj4KICA8L2NyZWF0b3JzPgogIDx0aXRsZXM+CiAgICA8dGl0bGU+Q29kZSB1bmRlcmx5aW5nIHRoZSBwdWJsaWNhdGlvbjogQnVpbGRpbmcgYSBDb3JyZWN0LUJ5LUNvbnN0cnVjdGlvbiBUeXBlIENoZWNrZXIgZm9yIGEgRGVwZW5kZW50bHkgVHlwZWQgQ29yZSBMYW5ndWFnZTwvdGl0bGU+CiAgPC90aXRsZXM+CiAgPHB1Ymxpc2hlcj40VFUuUmVzZWFyY2hEYXRhPC9wdWJsaXNoZXI+CiAgPHB1YmxpY2F0aW9uWWVhcj4yMDI0PC9wdWJsaWNhdGlvblllYXI+CiAgPHJlc291cmNlVHlwZSByZXNvdXJjZVR5cGVHZW5lcmFsPSJTb2Z0d2FyZSI+U29mdHdhcmU8L3Jlc291cmNlVHlwZT4KICA8c3ViamVjdHM+CiAgICA8c3ViamVjdCBzdWJqZWN0U2NoZW1lPSJBdXN0cmFsaWFuIGFuZCBOZXcgWmVhbGFuZCBTdGFuZGFyZCBSZXNlYXJjaCBDbGFzc2lmaWNhdGlvbiAoQU5aU1JDKSwgMjAwOCIgY2xhc3NpZmljYXRpb25Db2RlPSIwODAzIj5Db21wdXRlciBTb2Z0d2FyZTwvc3ViamVjdD4KICAgIDxzdWJqZWN0IHN1YmplY3RTY2hlbWU9IkF1c3RyYWxpYW4gYW5kIE5ldyBaZWFsYW5kIFN0YW5kYXJkIFJlc2VhcmNoIENsYXNzaWZpY2F0aW9uIChBTlpTUkMpLCAyMDA4IiBjbGFzc2lmaWNhdGlvbkNvZGU9IjA4Ij5JbmZvcm1hdGlvbiBhbmQgQ29tcHV0aW5nIFNjaWVuY2VzPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+ZGVwZW5kZW50IHR5cGVzPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+Y29yZSBsYW5ndWFnZTwvc3ViamVjdD4KICAgIDxzdWJqZWN0PnR5cGUgdGhlb3J5PC9zdWJqZWN0PgogICAgPHN1YmplY3Q+dHlwZWNoZWNraW5nPC9zdWJqZWN0PgogICAgPHN1YmplY3Q+dHlwZS1jaGVja2luZzwvc3ViamVjdD4KICA8L3N1YmplY3RzPgogIDxjb250cmlidXRvcnM+CiAgICA8Y29udHJpYnV0b3IgY29udHJpYnV0b3JUeXBlPSJPdGhlciI+CiAgICAgIDxjb250cmlidXRvck5hbWUgbmFtZVR5cGU9Ik9yZ2FuaXphdGlvbmFsIj5UVSBEZWxmdCwgRmFjdWx0eSBvZiBFbGVjdHJpY2FsIEVuZ2luZWVyaW5nLCBNYXRoZW1hdGljcyBhbmQgQ29tcHV0ZXIgU2NpZW5jZSwgRGVwYXJ0bWVudCBvZiBTb2Z0d2FyZSBUZWNobm9sb2d5IDwvY29udHJpYnV0b3JOYW1lPgogICAgPC9jb250cmlidXRvcj4KICA8L2NvbnRyaWJ1dG9ycz4KICA8ZGF0ZXM+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iSXNzdWVkIj4yMDI0LTEwLTMxPC9kYXRlPgogIDwvZGF0ZXM+CiAgPGxhbmd1YWdlPmVuPC9sYW5ndWFnZT4KICA8cmVsYXRlZElkZW50aWZpZXJzPgogICAgPHJlbGF0ZWRJZGVudGlmaWVyIHJlbGF0ZWRJZGVudGlmaWVyVHlwZT0iRE9JIiByZWxhdGlvblR5cGU9IklzU3VwcGxlbWVudFRvIj4xMC4xMDA3Lzk3OC05ODEtOTctODk0My02XzQ8L3JlbGF0ZWRJZGVudGlmaWVyPgogICAgPHJlbGF0ZWRJZGVudGlmaWVyIHJlbGF0ZWRJZGVudGlmaWVyVHlwZT0iVVJMIiByZWxhdGlvblR5cGU9IlJlZmVyZW5jZXMiPmh0dHBzOi8vY29uZi5yZXNlYXJjaHIub3JnL2RldGFpbHMvYXBsYXMtMjAyNC9hcGxhcy0yMDI0LXJlc2VhcmNoLXBhcGVycy8xMy9CdWlsZGluZy1BLUNvcnJlY3QtQnktQ29uc3RydWN0aW9uLVR5cGUtQ2hlY2tlci1mb3ItYS1EZXBlbmRlbnRseS1UeXBlZC1Db3JlLUxhbmd1YWdlPC9yZWxhdGVkSWRlbnRpZmllcj4KICA8L3JlbGF0ZWRJZGVudGlmaWVycz4KICA8Zm9ybWF0cz4KICAgIDxmb3JtYXQ+Z2l0IHJlcG9zaXRvcnkgY290YWluaW5nIGFuIEFnZGEgcHJvamVjdCwgYnVpbHQgdXNpbmcgbml4PC9mb3JtYXQ+CiAgPC9mb3JtYXRzPgogIDx2ZXJzaW9uPjI8L3ZlcnNpb24+CiAgPHJpZ2h0c0xpc3Q+CiAgICA8cmlnaHRzIHJpZ2h0c1VSST0iaHR0cHM6Ly9jcmVhdGl2ZWNvbW1vbnMub3JnL3B1YmxpY2RvbWFpbi96ZXJvLzEuMC8iPkNDMDwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KICA8ZGVzY3JpcHRpb25zPgogICAgPGRlc2NyaXB0aW9uIGRlc2NyaXB0aW9uVHlwZT0iQWJzdHJhY3QiPiZsdDtwJmd0O1RoaXMgcmVwb3NpdG9yeSBjb250YWlucyBzb3VyY2UgY29kZSBmb3IgdGhlIHBhcGVyLiBXZSBkZXZlbG9wIGEgY29ycmVjdC1ieS1jb25zdHJ1Y3Rpb24gdHlwZWNoZWNrZXIgZm9yIGEgc3Vic2V0IG9mIEFnZGEncyBpbnRlcm5hbCBsYW5ndWFnZS4gVGhpcyBjb2RlIGFzc3VtZXMgdGhhdCB0aGUgaW5wdXQgaGFzIGFscmVhZHkgYmVlbiBzY29wZS1jaGVja2VkIGFuZCBpcyBwcmVzZW50ZWQgdG8gdGhlIGNvcmUgaW4gYSB3ZWxsLXNjb3BlZCBmb3JtLiBUaGUgdHlwZWNoZWNrZXIgdXNlcyBlcmFzdXJlIGV4dGVuc2l2ZWx5IGFuZCBkb2Vzbid0IGRldmVsb3AgYW55IG1ldGEtdGhlb3J5LCByZWx5aW5nIG9uIHRoZSB0eXBpbmcgcnVsZXMgYXMgdGhlIHNvdXJjZSBvZiB0cnV0aC4gVGhlIGltcGxlbWVudGF0aW9uIHdhcyBkZXZlbG9wZWQgYnkgdGhlIGF1dGhvcnMgb2YgdGhlIHBhcGVyIHRocm91Z2ggMjAyMyBhbmQgMjAyNC4mbHQ7L3AmZ3Q7PC9kZXNjcmlwdGlvbj4KICA8L2Rlc2NyaXB0aW9ucz4KICA8ZnVuZGluZ1JlZmVyZW5jZXM+CiAgICA8ZnVuZGluZ1JlZmVyZW5jZT4KICAgICAgPGZ1bmRlck5hbWU+TldPPC9mdW5kZXJOYW1lPgogICAgICA8YXdhcmROdW1iZXI+VkkuVmVuaS4yMDIuMjE2IDwvYXdhcmROdW1iZXI+CiAgICAgIDxhd2FyZFRpdGxlPkEgdHJ1c3R3b3J0aHkgYW5kIGV4dGVuc2libGUgY29yZSBsYW5ndWFnZSBmb3IgQWdkYTwvYXdhcmRUaXRsZT4KICAgIDwvZnVuZGluZ1JlZmVyZW5jZT4KICA8L2Z1bmRpbmdSZWZlcmVuY2VzPgo8L3Jlc291cmNlPg==","url":"https://data.4tu.nl/datasets/6f239149-2526-42a0-8d07-d0e9d6714f7f","contentUrl":null,"metadataVersion":1,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"api","isActive":true,"state":"findable","reason":null,"viewCount":0,"viewsOverTime":[],"downloadCount":0,"downloadsOverTime":[],"referenceCount":0,"citationCount":1,"citationsOverTime":[{"year":"2024","total":1}],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2024-08-16T13:44:59.000Z","registered":"2024-08-16T13:45:00.000Z","published":"2024","updated":"2024-10-31T07:16:48.000Z"},"relationships":{"client":{"data":{"id":"delft.data4tu","type":"clients"}},"provider":{"data":{"id":"scpr","type":"providers"}},"media":{"data":{"id":"10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f","type":"media"}},"references":{"data":[]},"citations":{"data":[{"id":"10.1007/978-981-97-8943-6_4","type":"dois"}]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}