Write a Blog >>
Sat 25 Jan 2020 11:30 - 12:00 at Maurepas - Contributed Talks Chair(s): Amin Timany

This paper describes Goose, a subset of Go that can be translated to a Coq model. The Coq model plugs into Iris for concurrency proofs, giving an end-to-end system for writing and verifying concurrent systems. We have used Goose as part of our work on Perennial to verify a concurrent, crash-safe mail server that gets good performance.

(coqpl20-final4.pdf)432KiB
Goose CoqPL 2020 - slides (goose coqpl2020-slides.pdf)321KiB

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

CoqPL-2020-papers
10:30 - 12:30: CoqPL - Contributed Talks at Maurepas
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
CoqPL-2020-papers10:30 - 11:00
Talk
Arthur Azevedo de AmorimCarnegie Mellon University, USA
File Attached
CoqPL-2020-papers11:00 - 11:30
Talk
File Attached
CoqPL-2020-papers11:30 - 12:00
Talk
Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA
Link to publication File Attached
CoqPL-2020-papers12:00 - 12:30
Talk
Media Attached File Attached