Code underlying the publication: Building a Correct-By-Construction Type Checker for a Dependently Typed Core Language
4TU.ResearchDatavia 4TU.ResearchData (via DataCite) · updated 31 October 2024
What's in it
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.
Files and services
- DataCite REST API (JSON)api.datacite.orgOpen
Similar datasets
Data and code underlying the publication: Spatial optimization of circular timber hubs4TU.ResearchDataDataset for: Introducing a circular construction hub for building material circularity in city: A case study in Leiden, the Netherlands4TU.ResearchDataConstruction; building costs, building phase, type of buildingCBSData underlying the publication: An investigation of digital infrastructure’s role in repair and reuse of timber-based components in multi-story timber buildings: an interdisciplinary case study of digital product passport4TU.ResearchDataConstruction; category of purpose of new buildings, building phase, regionCBSConstruction; costs of buildings, building phase, type of clientCBSLinking full-text grey literature to underlying research and post-publication data: An Enhanced Publications Project 2011-2012DANS Data Station Social Sciences and HumanitiesData underlying the publication: Spatial Parameters for Circular Construction Hubs4TU.ResearchData
More from 4TU.ResearchData6,749 datasets
Data for thesis chapter "Suitability assessment of GNN-based metamodels for BGI allocation"Code for thesis chapter "Suitability assessment of GNN-based metamodels for BGI allocation"Data supporting the publication: Vision-Informed Short-Horizon Prediction for the Squeeze Flow of Soft MaterialsResearch Data and Code Supporting the PhD Dissertation: Learning Interpretable Robot Dynamics for Control — From Physical Structure to Latent CoordinatesData and scripts underlying the dissertation: Sodium Borohydride as Granular fuel: Experimental Characterisation and DEM ModellingData underlying Chapter 3 of the PhD thesis: Organic acids and bipolar membrane electrodialysis for enhanced ammonia recovery from scrubber effluents.