Viðburðir eftir árum

ICE-TCS seminar: Niccolò Veltri

Labelled transition systems in homotopy type theory

  • 19.3.2018, 12:10 - 13:00


Date and time: Monday, 19 March 2018 from 12:10 till 13:00
Place: Room M1.11 at Reykjavik University

Title: Labelled transition systems in homotopy type theory

Speaker: Niccolò Veltri (IT University Copenhagen), WWW:

Abstract: In this talk, I will show a formalization of labelled transition systems (LTSs) in homotopy type theory (HoTT). LTSs are a very versatile tool, typically employed in operational semantics of programming languages. One possible way to describe LTSs is as coalgebras for the functor F(X) = Pfin(A x X), where A is a type of actions and Pfin is the finite powerset functor. Pfin can be implemented in HoTT as a higher inductive type (Frumin et al. 2018).

We will formalize different notions of bisimulation for LTSs and prove that they coincide. Moreover, we will construct the final coalgebra of Pfin, building on an existing implementation of coinductive types in HoTT (Ahrens et al. 2015). In a similar way, one can define the final coalgebra of F, which is used for describing all possible runs of a LTS.