### Abstract

This document accompanies the article "The Design and Implementation of a Verification Technique for GPU Kernels" by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. It formalises all of the definitions provided in Sections 3 and 4 of the article.

### License

BSD License

### Topics

- Computer science/Programming languages/Language definitions

### Session GPU_Kernel_PL

- Misc
- KPL_syntax
- KPL_wellformedness
- KPL_state
- KPL_execution_thread
- KPL_execution_group
- KPL_execution_kernel
- Kernel_programming_language

## Cite

×

GPU_Kernel_PL-AFP

    @article{GPU_Kernel_PL-AFP,
      author  = {John Wickerson},
      title   = {Syntax and semantics of a GPU kernel programming language},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/GPU_Kernel_PL.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
- Aug 28, 2014 : Isabelle2014
- Apr 6, 2014 : Isabelle2013-2