Michelson, the stack-based virtual machine of the Tezos blockchain, integrates type-checking for program execution completion but not program correctness. Manual stack tracking is efficient but less ergonomic to write in than a higher-level lambda calculus with variables. Compiling McBride’s Quantitative Type Theory to Michelson allows for compile-time verification of semantic predicates and automatic stack optimisation by virtue of the type-theoretic usage accounting system.
CITATION STYLE
Goes, C. (2020). Compiling Quantitative Type Theory to Michelson for Compile-Time Verification and Run-time Efficiency in Juvix. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12478 LNCS, pp. 146–160). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-61467-6_10
Mendeley helps you to discover research relevant for your work.