### 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.

### License

BSD License

### History

March 16, 2015
  This entry now builds on top of the Launchbury entry, and the equivalency proof of the natural and the small-step semantics was added.

### Topics

- Computer science/Programming languages/Static analysis

### Session Call_Arity

- BalancedTraces
- SestoftConf
- Sestoft
- SestoftCorrect
- Arity
- AEnv
- Arity-Nominal
- ArityAnalysisSig
- ArityAnalysisAbinds
- ArityAnalysisSpec
- TrivialArityAnal
- Cardinality-Domain
- CardinalityAnalysisSig
- ConstOn
- CardinalityAnalysisSpec
- ArityAnalysisStack
- NoCardinalityAnalysis
- TransformTools
- AbstractTransform
- EtaExpansion
- EtaExpansionSafe
- ArityStack
- ArityEtaExpansion
- ArityEtaExpansionSafe
- ArityTransform
- ArityConsistent
- ArityTransformSafe
- Set-Cpo
- Env-Set-Cpo
- CoCallGraph
- CoCallAnalysisSig
- AList-Utils-HOLCF
- CoCallGraph-Nominal
- CoCallAnalysisBinds
- ArityAnalysisFix
- CoCallFix
- CoCallAnalysisImpl
- CallArityEnd2End
- SestoftGC
- CardArityTransformSafe
- CoCallAritySig
- CoCallAnalysisSpec
- ArityAnalysisFixProps
- CoCallImplSafe
- List-Interleavings
- TTree
- TTree-HOLCF
- AnalBinds
- TTreeAnalysisSig
- CoCallGraph-TTree
- CoCallImplTTree
- Cardinality-Domain-Lists
- TTreeAnalysisSpec
- CoCallImplTTreeSafe
- TTreeImplCardinality
- TTreeImplCardinalitySafe
- CallArityEnd2EndSafe
- ArityAnalysisCorrDenotational

### Depends on

- The Correctness of Launchbury’s Natural Semantics for Lazy Evaluation

## Cite

×

Call_Arity-AFP

    @article{Call_Arity-AFP,
      author  = {Joachim Breitner},
      title   = {The Safety of Call Arity},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Call_Arity.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- May 11, 2015 : Isabelle2014
- Feb 21, 2015 : Isabelle2014
- Feb 20, 2015 : Isabelle2014