WIP: Formalizing the Concordium Consensus Protocol in Coq (CoqPL 2019 - The Fifth International Workshop on Coq for Programming Languages)

Blogs (1) >>

Sun 13 - Sat 19 January 2019 Cascais, Portugal

Who

Thomas Dinsdale-Young, Bas Spitters, Søren Eller Thomsen, Daniel Tschudi

Track

CoqPL 2019

Time Zone

The program is currently displayed in (GMT) Belfast.

Use conference time zone: (GMT) BelfastSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 19 Jan 2019 12:05 - 12:30 at Sala VI - Contributed Talks 2 Chair(s): Enrico Tassi

Abstract

We report an industrial application of Coq: our work towards formalizing the Concordium blockchain consensus protocol.

File attachments

Abstract (coqpl19-final16a.pdf)	291KiB
Slides (coqpl-2019.pdf)	269KiB

Thomas Dinsdale-Young

Bas Spitters

Aarhus University

Denmark

Søren Eller Thomsen

Aarhus University

Denmark

Daniel Tschudi

Aarhus University

Time Zone

The program is currently displayed in (GMT) Belfast.

Use conference time zone: (GMT) BelfastSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Sat 19 Jan
Displayed time zone: Belfast change

11:15 - 12:30	Contributed Talks 2CoqPL at Sala VI Chair(s): Enrico Tassi INRIA

11:15 25m Talk		Towards Mechanising Probabilistic Properties of a Blockchain CoqPL Kiran Gopinathan University College London, Ilya Sergey Yale-NUS College and National University of Singapore File Attached
11:40 25m Talk		Verifying Finality for Blockchain Systems CoqPL Karl Palmskog University of Texas at Austin, Milos Gligoric University of Texas at Austin, Lucas Peña University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign File Attached
12:05 25m Talk		WIP: Formalizing the Concordium Consensus Protocol in Coq CoqPL Thomas Dinsdale-Young , Bas Spitters Aarhus University, Søren Eller Thomsen Aarhus University, Daniel Tschudi Aarhus University File Attached