The following pages link to Thierry Coquand (Q375196):
Displayed 50 items.
- A constructive version of Laplace's proof on the existence of complex roots (Q375197) (← links)
- (Q402419) (redirect page) (← links)
- Revisiting Zariski main theorem from a constructive point of view (Q402421) (← links)
- Curves and coherent Prüfer rings (Q607061) (← links)
- Games with 1-backtracking (Q636360) (← links)
- Treatise on intuitionistic type theory (Q639262) (← links)
- Independence results in formal topology (Q651321) (← links)
- Constructive finite free resolutions (Q663308) (← links)
- Another proof of the intuitionistic Ramsey theorem (Q685402) (← links)
- The paradox of trees in type theory (Q688725) (← links)
- Proof-theoretical analysis of order relations (Q701722) (← links)
- Generating non-Noetherian modules constructively (Q706187) (← links)
- Isomorphism is equality (Q740487) (← links)
- Extensional models for polymorphism (Q749518) (← links)
- Constructive characterizations of bar subsets (Q866574) (← links)
- Space of valuations (Q1006605) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- The calculus of constructions (Q1108266) (← links)
- Duplication of directed graphs and exponential blow up of proofs (Q1125056) (← links)
- Two applications of Boolean models (Q1128177) (← links)
- Inheritance as implicit coercion (Q1175335) (← links)
- Categories of embeddings (Q1263665) (← links)
- A Boolean model of ultrafilters (Q1304549) (← links)
- An analysis of Ramsey's theorem (Q1327381) (← links)
- Metric Boolean algebras and constructive measure theory (Q1407569) (← links)
- Compact spaces and distributive lattices. (Q1408349) (← links)
- Proofs and programs (Q1408657) (← links)
- Inductively generated formal topologies. (Q1412832) (← links)
- On a theorem of Kronecker about algebraic varieties (Q1426642) (← links)
- An elementary proof of Wiebe's theorem (Q1703086) (← links)
- About Stone's notion of spectrum (Q1772250) (← links)
- A note on measures with values in a partially ordered vector space (Q1780505) (← links)
- Syntactic forcing models for coherent logic (Q1788327) (← links)
- Combinatorial topology and constructive mathematics (Q1788338) (← links)
- Domain theoretic models of polymorphism (Q1824612) (← links)
- Valuations and Dedekind's Prague theorem (Q1840477) (← links)
- A syntactical proof of the Marriage Lemma. (Q1853584) (← links)
- A modern perspective on type theory. From its origins until today (Q1887432) (← links)
- A constructive topological proof of van der Waerden's theorem (Q1910731) (← links)
- An algorithm for type-checking dependent types (Q1916364) (← links)
- About Goodman's theorem (Q1942040) (← links)
- The strength of Martin-Löf type theory with a superuniverse. I (Q1976875) (← links)
- Intuitionistic choice and classical logic (Q1976877) (← links)
- Loop-checking and the uniform word problem for join-semilattices with an inflationary endomorphism (Q2123048) (← links)
- A Kripke model for simplicial sets (Q2257308) (← links)
- An adequacy theorem for dependent type theory (Q2311883) (← links)
- The univalence axiom in cubical sets (Q2319981) (← links)
- Lattice-ordered groups generated by an ordered group and regular systems of ideals (Q2326029) (← links)
- Spectral schemes as ringed lattices (Q2379681) (← links)
- Type theory and formalisation of mathematics (Q2399357) (← links)