Generic bidirectional typing for dependent type theories

Add to your list(s) Download to your calendar using vCal

• Thiago Felicissimo, INRIA
• Tuesday 03 October 2023, 11:00-12:00
• FW26, Computer Laboratory.

If you have a question about this talk, please contact nk480.

Algebraic/logical framework presentations of dependent type theories suffer from the verbosity of the required type annotations, which destroys any hope of practical usability. In order to restore usability, standard presentations usually omit the majority of these annotations, but this has a cost: because knowing them is still important when typing terms, it becomes unclear how to do this algorithmically.

A solution to this problem is provided by bidirectional typing, in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how the rules should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal.

The goal of this work is to give a generic account of bidirectional typing for a wide class of dependent type theories. For this, we start by giving a general definition of type theories (or equivalently, a logical framework), which differs from previous frameworks by allowing for the usual unannotated syntaxes most often used in practice. Each theory then gives rise to a declarative and a bidirectional typing system, the latter being defined only for the inferable and checkable terms (for non-degenerate theories, these coincide respectively with neutrals and normal forms). We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish, for weak normalizing theories, the decidability of inference for inferable terms, and the decidability of checking for checkable terms.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FW26, Computer Laboratory

Note that ex-directory lists are not shown.