English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We present an extensive mechanization of the meta-theory of Martin-L\"of TypeTheory (MLTT) in the Coq proof assistant. Our development builds onpre-existing work in Agda to show not only the decidability of conversion, butalso the decidability of type checking, using an approach guided bybidirectional type checking. From our proof of decidability, we obtain acertified and executable type checker for a full-fledged version of MLTT withsupport for $\Pi$, $\Sigma$, $\mathbb{N}$, and identity types, and oneuniverse. Furthermore, our development does not rely on impredicativity,induction-recursion or any axiom beyond MLTT with a schema for indexedinductive types and a handful of predicative universes, narrowing the gapbetween the object theory and the meta-theory to a mere difference inuniverses. Finally, we explain our formalization choices, geared towards amodular development relying on Coq's features, e.g. meta-programming facilitiesprovided by tactics and universe polymorphism.

Martin-L\"of \`a la Coq