|
The
Safety
of
Call
Arity
Title: |
The Safety of Call Arity |
Author:
|
Joachim Breitner (joachim /at/ cis /dot/ upenn /dot/ edu)
|
Submission date: |
2015-02-20 |
Abstract: |
We formalize the Call Arity analysis, as implemented in GHC, and prove
both functional correctness and, more interestingly, safety (i.e. the
transformation does not increase allocation).
We use syntax and the denotational semantics from the entry
"Launchbury", where we formalized Launchbury's natural semantics for
lazy evaluation.
The functional correctness of Call Arity is proved with regard to that
denotational semantics. The operational properties are shown with
regard to a small-step semantics akin to Sestoft's mark 1 machine,
which we prove to be equivalent to Launchbury's semantics.
We use Christian Urban's Nominal2 package to define our terms and make
use of Brian Huffman's HOLCF package for the domain-theoretical
aspects of the development. |
Change history: |
[2015-03-16]: This entry now builds on top of the Launchbury entry,
and the equivalency proof of the natural and the small-step semantics
was added. |
BibTeX: |
@article{Call_Arity-AFP,
author = {Joachim Breitner},
title = {The Safety of Call Arity},
journal = {Archive of Formal Proofs},
month = feb,
year = 2015,
note = {\url{https://isa-afp.org/entries/Call_Arity.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Launchbury |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|