Extensible Datasort Refinements

DOI10.1007/978-3-662-54434-1_18MaRDI QIDQ2988653zbMATH OpenOpenAlexFDO

Authors Joshua Dunfield

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1701.02842

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: Refinement types turn typechecking into lightweight verification. The classic form of refinement type is the datasort refinement, in which datasorts identify subclasses of inductive datatypes. Existing type systems for datasort refinements require that all the refinements of a type be specified when the type is declared; multiple refinements of the same type can be obtained only by duplicating type definitions, and consequently, duplicating code. We enrich the traditional notion of a signature, which describes the inhabitants of datasorts, to allow re-refinement via signature extension, without duplicating definitions. Since arbitrary updates to a signature can invalidate the inversion principles used to check case expressions, we develop a definition of signature well-formedness that ensures that extensions maintain existing inversion principles. This definition allows different parts of a program to extend the same signature in different ways, without conflicting with each other. Each part can be type-checked independently, allowing separate compilation.

Recommendations

• Optimally sorting evolving data
• scientific article; zbMATH DE number 2033275
• Multi-sorted residuation
• Sorting Multidimensional Types: Theory and Application
• Sorting and selection on dynamic data
• A framework for adaptive sorting
• A framework for adaptive sorting
• Extensions of self-improving sorters

Cites work

• scientific article; zbMATH DE number 1956517 (Why is no real title available?)
• A framework for defining logics
• Abstract refinement types
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Complete and easy bidirectional typechecking for higher-rank polymorphism
• Intersection types and computational effects
• Refinement types for logical frameworks and their interpretation as proof irrelevance
• Tridirectional typechecking

Cited in

(3)

• Sort Me If You Can: How to Sort Dynamic Data
• Abstract refinement types
• Exception tracking in an open world

Describes a project that uses

Uses Software

• GitHub
• Forsythe
• Delphin
• Stardust
• Twelf
• Beluga

This page was built for publication: Extensible Datasort Refinements

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988653)