publication . Other literature type . Conference object . 2020

Knowing When to Ask: Sound scheduling of name resolution in type checkers derived from declarative specifications (Extended Version)

Rouvoet, Arjen; van Antwerpen, Hendrik; Bach Poulsen, Casper; Krebbers, Robbert; Visser, Eelco;
Open Access English
  • Published: 15 Oct 2020
  • Publisher: Zenodo
Abstract
Extended version of the OOPSLA '20 paper "Knowing When to Ask".<br> <br> <em>Abstract:</em><br> There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolu...
Subjects
free text keywords: Statix, Constraint and Logic Programming, Type Systems, Specification
Download fromView all 3 versions
Zenodo
Other literature type . 2020
Provider: Datacite
Zenodo
Other literature type . 2020
Provider: Datacite
ZENODO
Conference object . 2020
Provider: ZENODO
Any information missing or wrong?Report an Issue