Thierry Coquand

University of Gothenburg — Sweden

Computer Science · Physical Sciences

34h-index5.5kcitations273works1.32yr avg
OpenAlex↗ORCID↗Google Scholar↗Lab page↗

Accepting Students?

No reports yet. Know if this professor is taking students?

Research Topics

Logic, programming, and type systems(129), Logic, Reasoning, and Knowledge(93), Advanced Algebra and Logic(47), Computability, Logic, AI Algorithms(45), Homotopy and Cohomology in Algebraic Topology(34)

Publications273 total

An Introduction to Lorenzen's ‘Algebraic and Logistic Investigations on Free Lattices’ (1951)
History and Philosophy of Logic·2025· 9 citedOpen Access
Chatelet's Theorem in Synthetic Algebraic Geometry
arXiv (Cornell University)·2025Open Access
A Foundation for Synthetic Stone Duality
arXiv (Cornell University)·2024Open Access
In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl
arXiv (Cornell University)·2024· 1 citedOpen Access
A foundation for synthetic algebraic geometry
Mathematical Structures in Computer Science·2024· 2 citedOpen Access
The equivariant model structure on cartesian cubical sets
arXiv (Cornell University)·2024Open Access
Projective Space in Synthetic Algebraic Geometry
arXiv (Cornell University)·2024Open Access
The Regular Element Property in Constructive Mathematics
arXiv (Cornell University)·2024Open Access
A Variation of Reynolds-Hurkens Paradox
Lecture notes in computer science·2024
Heitmann dimension of distributive lattices and commutative rings
arXiv (Cornell University)·2023Open Access
Some Remarks About Dependent Type Theory
2023
A variation of Reynolds-Hurkens Paradox
arXiv (Cornell University)·2023Open Access
Reduction Free Normalisation for a proof irrelevant type of propositions
Logical Methods in Computer Science·2023· 1 citedOpen Access
Azumaya algebras and Barr Theorem
arXiv (Cornell University)·2023Open Access
A Foundation for Synthetic Algebraic Geometry
arXiv (Cornell University)·2023Open Access
Constructive Theory of Ordinals
WORLD SCIENTIFIC eBooks·2023· 2 citedOpen Access
Type Theory with Explicit Universe Polymorphism (revised and extended version)
arXiv (Cornell University)·2022· 1 citedOpen Access
Controlling unfolding in type theory
arXiv (Cornell University)·2022· 3 citedOpen Access
Canonicity and homotopy canonicity for cubical type theory
Logical Methods in Computer Science·2022· 1 citedOpen Access
Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism
Theoretical Computer Science·2022· 5 citedOpen Access
page 1 of 14Next →

Frequent Co-authors

Carl A. Gunter(4), Simon Huber(3), Val Breazu-Tannen(3), Marc Bezem(3), Peter Dybjer(3), Gérard Huet(2), Cyril Cohen(2), Andre Scedrov(2), Giovanni Sambin(2), Jan M. Smith(2), Glynn Winskel(2), Henri Lombardi(2), Randy Pollack(2), Makoto Takeyama(2), Andreas Abel(2), Henrik Persson(2), Bas Spitters(2), Christine Paulin(1), Anders Mörtberg(1), Silvio Valentini(1)