A Mechanization of Howe's Method in Beluga

David Thibodeau

Bisimulation proofs are central to programming languages as they are used to establish important properties such as contextual equivalence. In this talk, I describe the mechanisation in Beluga of a proof that similarity in the call-by-name lambda-calculus is a precongruence using Howe's method. This proof makes use of Beluga's advanced features from copatterns to represent similarity as a coinductive relation to contextual LF to painlessly represent and reason about substitution properties of our calculus.