Higher-Ranked Annotation Polymorphic Dependency Analysis

Fabian Thorand, Jurriaan Hage

Research output: Chapter in Book/Report/Conference proceedingConference contribution

22 Downloads (Pure)

Abstract

The precision of a static analysis can be improved by increasing the context-sensitivity of the analysis. In a type-based formulation of static analysis for functional languages this can be achieved by, e.g., introducing let-polyvariance or subtyping. In this paper we go one step further by defining a higher-ranked polyvariant type system so that even properties of lambda-bound identifiers can be generalized over. We do this for dependency analysis, a generic analysis that can be instantiated to a range of different analyses that in this way all can profit. We prove that our analysis is sound with respect to a call-by-name semantics and that it satisfies a so-called noninterference property. We provide a type reconstruction algorithm that we have proven to be terminating, and sound and complete with respect to its declarative specification. Our principled description can serve as a blueprint for making other analyses higher-ranked.
Original languageEnglish
Title of host publicationProgramming Languages and Systems. ESOP 2020
EditorsPeter Müller
PublisherSpringer
Pages656-683
Number of pages28
ISBN (Electronic)9783030449148
ISBN (Print)9783030449131
DOIs
Publication statusPublished - 18 Apr 2020
Event29th European Symposium on Programming 2020 - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020

Publication series

NameLecture Notes in Computer Science
Volume12075
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference29th European Symposium on Programming 2020
Abbreviated titleESOP 2020
Country/TerritoryIreland
CityDublin
Period25/04/2030/04/20

Fingerprint

Dive into the research topics of 'Higher-Ranked Annotation Polymorphic Dependency Analysis'. Together they form a unique fingerprint.

Cite this