Verification of the UpDown Scheme

 

Title: Verification of the UpDown Scheme
Author: Johannes Hölzl
Submission date: 2015-01-28
Abstract: The UpDown scheme is a recursive scheme used to compute the stiffness matrix on a special form of sparse grids. Usually, when discretizing a Euclidean space of dimension d we need O(n^d) points, for n points along each dimension. Sparse grids are a hierarchical representation where the number of points is reduced to O(n * log(n)^d). One disadvantage of such sparse grids is that the algorithm now operate recursively in the dimensions and levels of the sparse grid.

The UpDown scheme allows us to compute the stiffness matrix on such a sparse grid. The stiffness matrix represents the influence of each representation function on the L^2 scalar product. For a detailed description see Dirk Pflüger's PhD thesis. This formalization was developed as an interdisciplinary project (IDP) at the Technische Universität München.

BibTeX:
@article{UpDown_Scheme-AFP,
  author  = {Johannes Hölzl},
  title   = {Verification of the UpDown Scheme},
  journal = {Archive of Formal Proofs},
  month   = jan,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/UpDown_Scheme.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Separation_Logic_Imperative_HOL