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

Conference Day
Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

10:30 - 12:30
Contributed TalksCoqPL at Maurepas
Chair(s): Amin Timanyimec-Distrinet KU-Leuven
10:30
30m
Talk
Deriving Instances with Dependent Types
CoqPL
Arthur Azevedo de AmorimCarnegie Mellon University, USA
File Attached
11:00
30m
Talk
The use of Coq for Common Criteria Evaluations
CoqPL
File Attached
11:30
30m
Talk
Verifying concurrent Go code in Coq with Goose
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
30m
Talk
A Tutorial on Equations
CoqPL
Media Attached File Attached