Type theory as a language workbench

de Muijnck-Hughes, Jan and Allais, Guillaume and Brady, Edwin; Lämmel, Ralf and Mosses, Peter and Steimann, Friedrich, eds. (2023) Type theory as a language workbench. In: Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), 109 . Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl, Germany. ISBN 9783959772679 (https://doi.org/10.4230/OASIcs.EVCS.2023.9)

Preview

Text. Filename: Muijnck_Hughes_etal_EVCS_2023_Type_theory_as_a_language_workbench.pdf Final Published Version License: Download (656kB)| Preview

Abstract

Language Workbenches offer language designers an expressive environment in which to create their Domain Specific Languages (DSLs). Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Vélo that showcases not only dependently typed techniques to realise and manipulate Intermediate Representations (IRs), but that dependently typed languages make fine language workbenches. Vélo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IR design that includes support for well-typed holes, how Common Sub-Expression Elimination (CSE) is achieved in a well-typed setting, and how the mechanised type-soundness proof for Vélo is the source of the evaluator.

ORCID iDs

de Muijnck-Hughes, Jan ORCID: https://orcid.org/0000-0003-2185-8543

Allais, Guillaume ORCID: https://orcid.org/0000-0002-4091-657X

• Share and Export
  

  Dublin CoreRIS (EndNote Online, Zotero, Ref manager, etc)Data Cite XMLEP3 XMLMPEG-21 DIDLMETSMODSOpenURL ContextObject in SpanRefWorksEndNoteReferBibTeXASCII CitationRDF+N3RIOXX2 XMLMultiline CSVOpenURL ContextObjectRDF+XMLSimple MetadataRDF+N-TriplesAtomHTML CitationJSON
• Item metadata

  Item type:	Book Section
  ID code:	86199
  Dates:	Date Event 21 March 2023 Published 11 November 2022 Accepted
  Subjects:	Science > Mathematics > Computer software
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	20 Jul 2023 11:25
  Last modified:	22 Dec 2024 01:09
  Related URLs:	Related item
  URI:	https://strathprints.strath.ac.uk/id/eprint/86199