License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2015.9
URN: urn:nbn:de:0030-drops-56406
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5640/
Jagannathan, Suresh
Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk)
Abstract
Understanding, discovering, and proving useful properties of sophisticated data structures are central problems in program verification. A particularly challenging exercise for shape analyses
involves reasoning about sophisticated shape transformers that preserve the shape of a data structure (e.g., the data structure skeleton is always maintained as a balanced tree) or the relationship among values contained therein (e.g., the in-order relation of the elements of a tree or the parent-child relation of the elements of a heap) across program transformations.
In this talk, we consider the specification and verification of such transformers for ML programs. The structural properties preserved by transformers can often be naturally expressed as inductively-defined relations over the recursive structure evident in the definitions of the datatypes they manipulate. By carefully augmenting a refinement type system with support for reasoning about structural relations over algebraic datatypes, we realize an expressive yet decidable specification language, capable of capturing useful structural invariants, which can nonetheless be automatically verified using off-the-shelf type checkers and theorem provers. Notably, our technique generalizes to definitions of parametric relations for polymorphic data types which, in turn, lead to highly composable specifications over higher-order polymorphic shape transformers.
BibTeX - Entry
@InProceedings{jagannathan:LIPIcs:2015:5640,
author = {Suresh Jagannathan},
title = {{Relational Refinement Types for Higher-Order Shape Transformers (Invited Talk)}},
booktitle = {35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
pages = {9--9},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-97-2},
ISSN = {1868-8969},
year = {2015},
volume = {45},
editor = {Prahladh Harsha and G. Ramalingam},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5640},
URN = {urn:nbn:de:0030-drops-56406},
doi = {10.4230/LIPIcs.FSTTCS.2015.9},
annote = {Keywords: Relational Specifications; Inductive and Parametric Relations; Refinement Types, Shape Analysis, Data Structure Verification}}
}
|
Keywords: |
|
Relational Specifications; Inductive and Parametric Relations; Refinement Types, Shape Analysis, Data Structure Verification} |
|
Collection: |
|
35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) |
|
Issue Date: |
|
2015 |
|
Date of publication: |
|
14.12.2015 |
