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: Saskatchewan, Central America change

10:30 - 12:30: Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
10:30 - 11:00
Talk
CoqPL
Arthur Azevedo de AmorimCarnegie Mellon University, USA
File Attached
11:00 - 11:30
Talk
CoqPL
File Attached
11:30 - 12:00
Talk
CoqPL
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
12:00 - 12:30
Talk
CoqPL
Media Attached File Attached