Bidirectional Type Checking
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