Mentions légales du service

Skip to content
Snippets Groups Projects
Commit da4f840a authored by Samuel Mimram's avatar Samuel Mimram
Browse files

Fix.

parent ad103a1c
No related branches found
No related tags found
No related merge requests found
Pipeline #1185476 passed
...@@ -146,7 +146,7 @@ ...@@ -146,7 +146,7 @@
lab: Inria Rennes (Gallinette team) lab: Inria Rennes (Gallinette team)
title: Generic bidirectional typing for dependent type theories title: Generic bidirectional typing for dependent type theories
abstract: | abstract: |
Bidirectional typing is a discipline in which the typing judgment is decomposed into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they 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 mostly informal and not fully developed. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. We also establish the decidability of bidirectional typing for normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype, available at https://github.com/thiagofelicissimo/BiTTs, and used in practice with many theories. Bidirectional typing is a discipline in which the typing judgment is decomposed into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they 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 mostly informal and not fully developed. In this work, we give a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. We also establish the decidability of bidirectional typing for normalizing theories, yielding a generic type-checking algorithm that has been implemented in [a prototype](https://github.com/thiagofelicissimo/BiTTs), and used in practice with many theories.
- date: 2024-12-11 13:30 - date: 2024-12-11 13:30
team: COSYNUS team: COSYNUS
room: Grace Hopper room: Grace Hopper
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment