@InProceedings{demuijnckhughes_et_al:OASIcs.EVCS.2023.9, author = {de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin}, title = {{Type Theory as a Language Workbench}}, booktitle = {Eelco Visser Commemorative Symposium (EVCS 2023)}, pages = {9:1--9:13}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-267-9}, ISSN = {2190-6807}, year = {2023}, volume = {109}, editor = {L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.9}, URN = {urn:nbn:de:0030-drops-177797}, doi = {10.4230/OASIcs.EVCS.2023.9}, annote = {Keywords: dependent types, language workbenches, idris2, dsl, edsl, intrinsically scoped, well typed, co-De Bruijn} }