Syntactical extensibility of proof assistants

Bohdan Liesnikov


Date: Wed, January 11, 2023
Time: 14:00
Room: Turing 0.E420
Note: This is a PhD Go/No-Go meeting


Dependently-typed languages are attracting more attention in the recent years.

Functional programmers want more advanced types and major functional languages like Haskell and Scala are trying to oblige. Mathematicians want more advanced tactics and faster type-checking to formalise more results. Type-theorists want to keep tinkering with the languages. We believe an answer to these demands is a language with common core and different syntactical extensions to cater to different groups.

In this talk I will describe some of the things I did until now in my PhD and how do I plan to proceed.

The talk will be about 10-15 minutes.

Previous: Thomas Lamiaux |
Next: Sina Hazratpour |