1 Search Results for "Brouwer, Jonathan"

Document
DOI: 10.4230/OASIcs.EVCS.2023.6
Dependently Typed Languages in Statix

Authors: Jonathan Brouwer, Jesper Cockx, and Aron Zwaan

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.
Cite as

Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently Typed Languages in Statix. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brouwer_et_al:OASIcs.EVCS.2023.6,
  author =	{Brouwer, Jonathan and Cockx, Jesper and Zwaan, Aron},
  title =	{{Dependently Typed Languages in Statix}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{6:1--6:8},
  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-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.6},
  URN =		{urn:nbn:de:0030-drops-177769},
  doi =		{10.4230/OASIcs.EVCS.2023.6},
  annote =	{Keywords: Spoofax, Statix, Dependent Types, Scope Graphs, Calculus of Constructions}
}
  • Refine by Author
  • 1 Brouwer, Jonathan
  • 1 Cockx, Jesper
  • 1 Zwaan, Aron

  • Refine by Classification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Functional languages
  • 1 Software and its engineering → Semantics

  • Refine by Keyword
  • 1 Calculus of Constructions
  • 1 Dependent Types
  • 1 Scope Graphs
  • 1 Spoofax
  • 1 Statix

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact