Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generic bidirectional typing for dependent type theories

Thiago Felicissimo

TL;DR

The paper addresses the challenge of generalizing bidirectional typing to a broad class of dependent type theories. It develops a theory-independent framework with a general definition of type theories, a declarative typing system, a bidirectional system, and proofs of their equivalence, along with decidability results for strongly-normalizing theories. It also implements the framework in BiTTs and demonstrates practicality across diverse theories (MLTT variants, HOL, OTT). The work enables theory-agnostic, efficient type checking with unannotated syntax, reducing annotation overhead while maintaining robust correctness guarantees. This yields a practical tool for prototyping and validating new dependent type theories, with broad potential impact on proof engineering and formal verification workflows.

Abstract

Bidirectional typing is a discipline 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 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 informal. 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. Finally, we establish the decidability of bidirectional typing for normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.

Generic bidirectional typing for dependent type theories

TL;DR

The paper addresses the challenge of generalizing bidirectional typing to a broad class of dependent type theories. It develops a theory-independent framework with a general definition of type theories, a declarative typing system, a bidirectional system, and proofs of their equivalence, along with decidability results for strongly-normalizing theories. It also implements the framework in BiTTs and demonstrates practicality across diverse theories (MLTT variants, HOL, OTT). The work enables theory-agnostic, efficient type checking with unannotated syntax, reducing annotation overhead while maintaining robust correctness guarantees. This yields a practical tool for prototyping and validating new dependent type theories, with broad potential impact on proof engineering and formal verification workflows.

Abstract

Bidirectional typing is a discipline 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 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 informal. 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. Finally, we establish the decidability of bidirectional typing for normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.
Paper Structure (43 sections, 26 theorems, 26 equations, 7 figures, 1 table)

This paper contains 43 sections, 26 theorems, 26 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. A general definition of bidirectional type theories
  3. Raw Syntax
  4. Intrinsically-scoped syntax
  5. Scopes and signatures
  6. Terms and substitutions
  7. Contexts
  8. Substitution application
  9. Patterns
  10. Theories
  11. Sort rules
  12. Constructor rules
  13. Destructor rules
  14. Rewrite rules
  15. Underlying signature
  16. ...and 28 more sections

Key Result

proposition 1

We have $e[\textup{id}_{\gamma}] = e$ and $e[\textup{id}_{\theta}]=e$ for all $e \in \textup{Expr}~\theta~\gamma$, and $\textup{id}_{\delta}[\vec{t}]=\vec{t}$ for all $\vec{t}\in \textup{Sub}~\theta~\gamma~\delta$, and $\textup{id}_{\theta}[\textbf{v}]=\textbf{v}$ for all $\textbf{v} \in \textup{MSu

Figures (7)

  • Figure 1: Application of a variable or metavariable substitution
  • Figure 2: Definition of theories
  • Figure 3: Rewriting relation defined by theory $\mathbb{T}$
  • Figure 4: Declarative typing rules
  • Figure 5: Well-typed theories
  • ...and 2 more figures

Theorems & Definitions (59)

  • Remark 1
  • Remark 3
  • Remark 4
  • proposition 1: Unit laws for $\textup{id}$
  • proof
  • proposition 2: Commutation lemmas
  • proposition 3: Associativity of substitution
  • proof
  • Remark 5
  • proposition 4: Stability of rewriting under substitution
  • ...and 49 more