[msp-interest] [MSP101] Liang-Ting Chen: A formal treatment of bidirectional typing (LT210, 2pm Fri 30-May)

[Dilsat Yuksel]

Hi,

Next Friday, the MSP101 talk will be given by Liang-Ting Chen (Institute of Information Science, Academia Sinica, Taiwan). See the details of the talk below.

Best,
Dilsat

**********************************************************************

Date: Friday, 30 May at 14:00

Room: LT210, Livingstone Tower

Zoom link: https://strath.zoom.us/j/85449272187?pwd=0qNkQqybiaKgBpbEBRv38x11x4db5n.1
Live stream on Youtube: https://www.youtube.com/@msp101strathclyde4

Speaker: Liang-Ting Chen

Title: A formal treatment of bidirectional typing

Abstract: In this talks, we consider a general and formal theory of bidirectional typing for simply typed languages: for every signature that specifies a mode-correct bidirectionally typed language, there exists a proof-relevant type synthesiser which, given an input abstract syntax tree, constructs a typing derivation if any, gives its refutation if not, or reports that the input does not have enough type annotations.

Sufficient conditions for deriving a type synthesiser such as soundness, completeness, and mode-correctness are established for all signatures. We propose a preprocessing step, which helps the user to deal with missing type annotations. The entire theory is implemented in Agda, serving as a verified generator of proof-relevant type synthesisers as a by-product.

**********************************************************************

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.strath.ac.uk/archives/msp-interest/attachments/20250523/041884b5/attachment.html