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

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical

### Session UpDown_Scheme

- Grid_Point
- Grid
- Triangular_Function
- UpDown_Scheme
- Up
- Down
- Up_Down
- Imperative

### Depends on

- Automatic Data Refinement
- A Separation Logic Framework for Imperative HOL

### Auto-related entries

- Binary codes that do not preserve primitivity
- Monadification, Memoization and Dynamic Programming
- Simple Firewall
- Information Flow Noninterference via Slicing
- Inter-Procedural Information Flow Noninterference via Slicing

## Cite

×

UpDown_Scheme-AFP

    @article{UpDown_Scheme-AFP,
      author  = {Johannes Hölzl},
      title   = {Verification of the UpDown Scheme},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/UpDown_Scheme.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 20, 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
- Jan 30, 2015 : Isabelle2014