Formal development of a type-safe intermediate language for tensor expressions.
This Coq development accompanies and builds on the presentation in the article
TeIL: a type-safe imperative tensor intermediate language.
The article discusses type-safety for TeIL, a proof of which is developed in the safety subdirectory of this repository.
Generally, the contents of this repository are as follows:
safetycontains a Coq development culminating in a type-safety (memory-safety) proof for TeIL.equations/deepcontains another deep embedding of TeIL into Coq using paramteric higher-order abstract syntax (PHOAS). This facilitates simple proofs of the equations in Section 3.6 of TeIL: a type-safe imperative tensor intermediate language.equations/shallowcontains a shallow embedding of TeIL expressions into Coq. This enables even simpler verification of the equations in Section 3.6 of TeIL: a type-safe imperative tensor intermediate language.
Note that a precursor of TeIL is presented in the article Modeling of languages for tensor manipulation, together with pen-and-paper proofs.