Write a Blog >>
Tue 21 Jan 2020 11:13 - 11:35 at Maurepas - Mechanized metatheory Chair(s): Benjamin C. Pierce

We present a new way of embedding functional languages into the Coq proof assistant by using meta-programming. This allows us to develop the meta-theory of the language using the deep embedding and provides a convenient way for reasoning about concrete programs using the shallow embedding. We connect the deep and the shallow embeddings by a soundness theorem. As an instance of our approach, we develop an embedding of a core smart contract language into Coq and verify several important properties of a crowdfunding contract based on a previous formalization of smart contract execution in blockchains.

Tue 21 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

10:30 - 11:35: CPP 2020 - Mechanized metatheory at Maurepas
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
CPP-2020-papers10:30 - 10:51
Yannick ForsterSaarland University, Kathrin StarkSaarland University, Germany
DOI Pre-print Media Attached
CPP-2020-papers10:51 - 11:13
Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile
DOI Pre-print Media Attached File Attached
CPP-2020-papers11:13 - 11:35
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
DOI Pre-print Media Attached File Attached