Zero-Cost Coercions for Program and Proof Reuse

Larry Diehl; Aaron Stump

doi:10.48550/arxiv.1802.00787

Back

Zero-Cost Coercions for Program and Proof Reuse

Preprint

Open access

Zero-Cost Coercions for Program and Proof Reuse

Larry Diehl and Aaron Stump

ArXiv.org

02/02/2018

DOI: 10.48550/arxiv.1802.00787

Files and links (1)

url

https://doi.org/10.48550/arXiv.1802.00787View

Preprint (Author's original)This preprint has not been evaluated by subject experts through peer review. Preprints may undergo extensive changes and/or become peer-reviewed journal articles. Open Access

Abstract

We introduce the notion of identity coercions between non-indexed and indexed variants of inductive datatypes, such as lists and vectors. An identity coercion translates one type to another such that the coercion function definitionally reduces to the identity function. This allows us to reuse vector programs to derive list programs (and vice versa), without any runtime cost. This also allows us to reuse vector proofs to derive list proofs (and vice versa), without the cost of equational reasoning proof obligations. Our work is formalized in Cedille, a dependently typed programming language based on a type-annotated Curry-style type the- ory with implicit (or, erased) products (or, dependent functions), and relies crucially on erasure to introduce definitional equalities between underlying untyped terms.

Computer Science - Programming Languages

Details

Title: Subtitle: Zero-Cost Coercions for Program and Proof Reuse
Creators: Larry Diehl
Aaron Stump
Resource Type: Preprint
Publication Details: ArXiv.org
DOI: 10.48550/arxiv.1802.00787
ISSN: 2331-8422
Language: English
Date posted: 02/02/2018
Academic Unit: Computer Science
Record Identifier: 9984410852902771

Metrics

3 Record Views