The Coq system is a powerful tool for dependently-typed programming. The

tactic subsystem of Coq provides means for proof automation, which

facilitates a broad range of its application as a proof assistant. At

the same time the attempts to utilize the rich type system of Coq for

writing dependently typed programs often face certain problems. In

particular, elimination for deep dependent types (using such tactics as

inversion/destruct as well as direct pattern matching construct) can be

cumbersome. In the talk we consider some of these difficulties and

present the ways to work them around.

Speaker: Dmitrii Boulytchev

02.11.2019, 17:15.

Venue:room 3248, Faculty of Mathematics and Mechanics, Saint Petersburg State University, Stary Peterhof, Universitetski pr., 28