KIT | KIT-Bibliothek | Impressum | Datenschutz

The Safety of Call Arity

Breitner, Joachim

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.



Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Zeitschriftenaufsatz
Jahr 2015
Sprache Englisch
Identifikator ISSN: 2150-914X
KITopen-ID: 1000049754
Erschienen in Archive of Formal Proofs
Seiten online
Externe Relationen Siehe auch
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page