Лаборатория языковых инструментов

Over last years bidirectional type checking become pretty much default approach. Bidirectional rules are designed in a way that makes type checking syntax-directed, thus providing a straightforward interpretation in a form of an algorithm. We'll take a look at the case of Simply-Typed λ-calculus, contrast traditional presentation with bidirectional one, see an implementation of a corresponding type-checker, discuss possible extensions and criteria for guiding design of bespoke bidirectional systems.

Speaker: Alexander Chichigin (ML engineer @ Calejo)

Google Meet: https://meet.google.com/myu-dhmz-gvu