36 citations · 143 across the 40 of their papers we have counts for
Showing 2021Show all
2 papers · 1 filter
cs.LO2021★ 1 cited
Reduction Free Normalisation for a proof irrelevant type of propositions
Thierry Coquand
We show normalisation and decidability of convertibility for a type theory with a hierarchy of universes and a proof irrelevant type of propositions, close to the type system used…
math.RA2021
Constructive basic theory of central simple algebras
Thierry Coquand, Henri Lombardi, Stefan Neuwirth
We provide a constructive treatment of basic results in the theory of central simple algebras. One main issue is the fact that one starting result, Wedderburn's Theorem stating tha…