Proceedings available here
Welcome
[8:55] Welcome & Introduction (by M. Carbone and R. Neykova)
Invited Talk (chair: M. Carbone)
[9:00] Ilya Sergey. Growing a Smart Contract Language for a High-Throughput Blockchain
Abstract
The Scilla project, aimed at creating a programming language for safe and secure smart contracts, has started in late 2017 as a 100-lines-of-code prototype implemented in the Coq proof assistant. Learning from the mistakes of Ethereum, which had pioneered the area of blockchain-based smart contracts, the aim of Scilla was to provide a smart contract language, which is expressive enough to accommodate most of the reasonable use-cases, while allowing for scalable and tractable formal verification and analysis. Since 2019, Scilla has been powering the application layer of Zilliqa, the world's first publicly deployed sharded blockchain system. Since its public launch, hundreds of unique smart contracts implemented in Scilla have been deployed, including custom tokens, collectibles (NFTs), auctions, multiplayer games, name registries, atomic token swaps, and many others. The design of Scilla has enabled the very first approach for efficiently sharding account-based smart contracts in a Layer-1 scalable blockchain protocol. In my talk, I will describe the motivation, high-level design principles, and semantics of Scilla, and outline the main use cases and the tools provided by the developer community. I will also present a framework for lightweight verification of Scilla programs, and showcase its automated domain-specific analyses, aiming at proving different notions of safety and enabling sharding-based parallelism. Finally, I will outline the pragmatic pitfalls of building a new smart contract language from scratch, and present the future exciting research directions that are enabled by Scilla's take on smart contract implementation.[10:00] Coffee Break
Morning Session (chair: V. Vasconcelos)
[10:30] D. Marshall, D. Orchard. Replicate, Reuse, Repeat: Capturing Non-Linear Communication via Session Types and Graded Modal Types (long paper) (๐ slides)
[11:00] I. Castellani, M. Dezani-Ciancaglini, P. Giannini. Asynchronous Sessions with Input Races (long paper)(๐ slides)
[11:30] M. Latifa, O. Dardha. Capable GV: Capabilities for Session Types in GV. (๐ slides)
[11:50] K. Imai. Polymorphic Multiparty Session Handlers in OCaml
[12:10] M. Vassor, Q. Xi, N. Yoshida. Towards Refined Multiparty Session Types in Rust
[12:30] Lunch Break
Afternoon Session (chair: D. Orchard)
[14:00] D. Costa, A. Mordido, D. Pocas, V. Vasconcelos. Higher-order Context-free Session Types in System F (long paper) (๐ slides)
[14:30] D. Liew, T. Cogumbreiro, J. Lange. Provable GPU Data-Races in Static Race Detection (long paper)
[15:00] H. Zicarelli, T. Cogumbreiro. Veri๏ฌcation of GPU Programs: Evaluation Challenges
[15:20] A. Alsubhi, O. Dardha. Coconut: Typestates for C++
[15:40] S. Butcher, N. Yoshida, F. Zhou. Unreliable Multiparty Communicating Automata
[16:00] Coffee Break
Evening Session (chair: Paola Giannini)
[16:30] M. Cimini. Lang-n-Send: Processes That Send Languages (long paper)
[17:00] L. Bacchiani, M. Bravetti, M. Giunti, J. Mota and A. Ravara. Java Subtypestate Checker. (๐ slides)
[17:20] T. Hildebrandt. DCR Graphs: Maintainable Graph-based Models of Machine Readable and Executable Regulations
[17:40] Closing