Write a Blog >>
Mon 20 Jan 2020 14:00 - 14:21 at Maurepas - Proof engineering and user interaction Chair(s): Yves Bertot

Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of machine-checked formalization.

This paper gives a novel presentation of an equational theory for reasoning about structures up to weak bisimulation. The theory is both compositional, making it suitable for defining general-purpose lemmas, and also incremental, meaning that the bisimulation can be created interactively. To prove the theory’s soundness, this paper also introduces generalized parametric coinduction, which addresses expressivity problems of earlier works and provides a practical framework for coinductive reasoning. The paper presents the resulting equational theory for streams, but the technique applies to other structures too.

All of the results in this paper have been proved in Coq, and the generalized parametric coinduction framework is available as a Coq library.

Slides (cpp20_gpaco_talk.pdf)2.56MiB

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Proof engineering and user interactionCPP at Maurepas
Chair(s): Yves Bertot INRIA
An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University of Pennsylvania
DOI Pre-print Media Attached File Attached
Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
Qingxiang Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in Prague
DOI Pre-print
REPLICA: REPL Instrumentation for Coq Analysis
Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University of California, San Diego
DOI Pre-print Media Attached