CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL (bibtex)

by Izumi Asakura, Hidehiko Masuhara and Tomoyuki Aotani

Reference:

CertSkel: a Verified Compiler for a Coq-embedded GPGPU DSL (Izumi Asakura, Hidehiko Masuhara and Tomoyuki Aotani), In Proceedings of The Third International Workshop on Coq for Programming Languages (CoqPL 2017), colocated with PoPL'17, 2017. ()

Bibtex Entry:

@inproceedings{asakura2017coqpl,
  author = {Izumi Asakura and Hidehiko Masuhara and Tomoyuki Aotani},
  url = {https://popl17.sigplan.org/track/main},
  pdf = {coqpl2017.pdf},
  title = {{CertSkel}: a Verified Compiler for a {Coq}-embedded {GPGPU DSL}},
  booktitle = {Proceedings of The Third International Workshop on Coq for Programming Languages (CoqPL 2017), colocated with PoPL'17},
  year = 2017,
  optpages = {},
  month = jan,
  location = {Paris, France},
  note = {},
  date = {2017-01-21}
}