Titlebook: Leveraging Applications of Formal Methods, Verification and Validation: Applications; 9th International Sy Tiziana Margaria,Bernhard Steffe

只看該作者 · 發(fā)表于 2025-3-27 14:43:34

Compiling Quantitative Type Theory to?Michelson for Compile-Time Verification and Run-time Efficiencess. 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.

只看該作者 · 發(fā)表于 2025-3-27 20:11:26

只看該作者 · 發(fā)表于 2025-3-28 01:31:00

Making Tezos Smart Contracts More Reliable with Coqning formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.

只看該作者 · 發(fā)表于 2025-3-28 04:36:23

0302-9743 of Formal Methods, ISoLA 2020, which was planned to take place during October 20–30, 2020, on Rhodes, Greece. The event itself was postponed to 2021 due to the COVID-19 pandemic...The papers presented were carefully reviewed and selected for inclusion in the proceedings. ..Each volume focusses on an

只看該作者 · 發(fā)表于 2025-3-28 07:53:34

只看該作者 · 發(fā)表于 2025-3-28 12:39:37

		自動登錄	找回密碼
密碼			To register

關(guān)于派博傳思			派博傳思旗下網(wǎng)站			友情鏈接
派博傳思介紹	公司地理位置	論文服務(wù)流程	影響因子官網(wǎng)	吾愛論文網(wǎng)	大講堂	北京大學(xué)	Oxford Uni.	Harvard Uni.
發(fā)展歷史沿革	期刊點評	投稿經(jīng)驗總結(jié)	SCIENCEGARD	IMPACTFACTOR	派博系數(shù)	清華大學(xué)	Yale Uni.	Stanford Uni.
\|Archiver\|手機(jī)版\|小黑屋\| 派博傳思國際 ( 京公網(wǎng)安備110108008328) GMT+8, 2025-10-13 00:49
Copyright © 2001-2015 派博傳思京公網(wǎng)安備110108008328 版權(quán)所有 All rights reserved