Formalising MiniSail in Isabelle
Sail is a language for specifying instruction-set architectures and has been used to model various production and research architectures. Designed to be engineer friendly, Sail is an imperative first-order language with a light-weight dependent type system. The latest redesign of the Sail type system has been done in conjunction with the development of a core calculus, MiniSail, along with paper proofs of type safety.
This talk presents work to mechanise MiniSail in Isabelle, making use of the Nominal2 Isabelle library to address binding structures and alpha-equivalence. The mechanisation includes the definition of the MiniSail type system and operational semantics, as well as proofs of preservation and progress. We outline the experience of using Nominal2 to do this mechanisation and the follow-on work to mechanise a Sail type-validator and a Sail to MiniSail converter.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
20:00 - 21:00 | Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan Shankar SRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | ||
20:00 5mTalk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry Rozplokhas Saint Petersburg State University and JetBrains Research, Andrey Vyatkin Saint Petersburg State University, Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research Media Attached | ||
20:05 5mTalk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário Pereira NOVA LINCS & Nova School of Sciences and Tecnhology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
20:10 5mTalk | Gradualizing the Calculus of Inductive Constructions CPP Lightning Talks Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile Pre-print | ||
20:15 5mTalk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid Jakobsson Nomadic Labs, Colin González Université de Paris, Irif -- Nomadic Labs, Bruno Bernardo Nomadic Labs, Raphaël Cauderlier Nomadic Labs | ||
20:20 5mTalk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören Bleikertz Digital Asset, Andreas Lochbihler Digital Asset, Ognjen Marić Digital Asset, Simon Meier Digital Asset, Phoebe Nichols Digital Asset, Matthias Schmalz Digital Asset, Ratko G. Veprek Digital Asset File Attached | ||
20:25 5mTalk | Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks | ||
20:30 5mTalk | Formalization of Combinatorics on Words in Isabelle/HOL CPP Lightning Talks Štěpán Holub Charles University, Štěpán Starosta Faculty of Information Technology, Czech Technical University in Prague Link to publication Media Attached File Attached | ||
20:35 5mTalk | Formalising MPC-in-the-head-based zero-knowledge CPP Lightning Talks Nikolaj Sidorenco Aarhus University, Sabine Oechsner Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University File Attached | ||
20:40 5mTalk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander Kogtenkov Schaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
20:45 5mTalk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark Wassell University of Cambridge | ||
20:50 5mTalk | How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks File Attached | ||
20:55 5mTalk | Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias Kappé Cornell University | ||