Document Open Access Logo

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact)

Author Takashi Suwa

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.12.1.14.pdf
  • Filesize: 0.6 MB
  • 5 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Functional languages
  • Software and its engineering → Software verification and validation
  • Theory of computation → Type structures
Keywords
  • Metaprogramming
  • Staged computation
  • Dependent types
  • Refinement types
  • Tensor shape checking

Metrics

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2026 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

Based on the method proposed in the corresponding paper, we implemented a prototype type-checker (and a simple interpreter) for compile-time tensor shape checking. we ported a number of DNN-related example programs offered by ocaml-torch to our language and checked them by using the prototype implementation. The results indicated that our method can be considered effective enough to accommodate realistic tensor-handling programs.

Cite As Get BibTex

Takashi Suwa. Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 14:1-14:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/DARTS.12.1.14

Author Details

Takashi Suwa
  • Kyoto University, Japan
  • Imiron Co., Ltd., Tokyo, Japan

Funding

This work is partially supported by JSPS KAKENHI Grant Numbers 20H00582 and 26H02493, Japan.

Acknowledgements

The authors wish to thank the anonymous reviewers and (past) members of our laboratory for various fruitful comments and feedbacks. We are also grateful to Shivankur Gupta for implementing a basic code-generating backend for OCaml during his internship.

Related Article

  • Takashi Suwa and Atsushi Igarashi, "Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types", in 40th European Conference on Object-Oriented Programming (ECOOP 2026), LIPIcs, Vol. 372, pp. 28:1-28:31, 2026. https://doi.org/10.4230/LIPIcs.ECOOP.2026.28

References

  1. Jane Street Capital. ocaml-torch. https://github.com/janestreet/torch, 2023. Accessed: 2025-02-27.
  2. GHC Team. Glasgow Haskell Compiler. https://www.haskell.org/ghc/. Accessed: 2025-03-22.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact