Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Fri 18 Jan 2019 11:41 - 12:03 at Sala I - Dependent Types Chair(s): Andreas Abel

In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity.

Guarded recursion in the sense of Nakano has recently been suggested as a possible approach for dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for coinductive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.

(slides.pdf)163KiB

Fri 18 Jan

POPL-2019-Research-Papers
10:35 - 12:03: Research Papers - Dependent Types at Sala I
Chair(s): Andreas AbelGothenburg University
POPL-2019-Research-Papers10:35 - 10:57
Talk
Evan CavalloCarnegie Mellon University, Robert Harper
Link to publication DOI Pre-print File Attached
POPL-2019-Research-Papers10:57 - 11:19
Talk
Thorsten AltenkirchUniversity of Nottingham, Ambrus KaposiUniversity of Nottingham, András KovácsEötvös Loránd University
Link to publication DOI File Attached
POPL-2019-Research-Papers11:19 - 11:41
Talk
Gaetan Gilbert, Jesper CockxChalmers | University of Gothenburg, Matthieu SozeauInria, Nicolas TabareauInria
Link to publication DOI File Attached
POPL-2019-Research-Papers11:41 - 12:03
Talk
Rasmus Ejlers MøgelbergIT University of Copenhagen, Niccolò VeltriIT University of Copenhagen
Link to publication DOI File Attached