Coquand, Thierry Canonicity and normalization for dependent type theory. (English) Zbl 1454.03019 Theor. Comput. Sci. 777, 184-191 (2019). MSC: 03B38 03B40 PDFBibTeX XMLCite \textit{T. Coquand}, Theor. Comput. Sci. 777, 184--191 (2019; Zbl 1454.03019) Full Text: DOI arXiv
Coquand, Thierry Type theory and formalisation of mathematics. (English) Zbl 1489.68395 Weil, Pascal (ed.), Computer science – theory and applications. 12th international computer science symposium in Russia, CSR 2017, Kazan, Russia, June 8–12, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10304, 1-6 (2017). MSC: 68V20 03B35 03B38 03B40 PDFBibTeX XMLCite \textit{T. Coquand}, Lect. Notes Comput. Sci. 10304, 1--6 (2017; Zbl 1489.68395) Full Text: DOI
Coquand, Thierry; Jaber, Guilhem A computational interpretation of forcing in type theory. (English) Zbl 1312.03021 Dybjer, Peter (ed.) et al., Epistemology versus ontology. Essays on the philosophy and foundations of mathematics in honour of Per Martin-Löf. Based on the conference, “Philosophy and foundations of mathematics: Epistemological and ontological aspects”, Uppsala, Sweden, May 5–8, 2009. Dordrecht: Springer (ISBN 978-94-007-4434-9/hbk; 978-94-007-4435-6/ebook). Logic, Epistemology, and the Unity of Science 27, 203-213 (2012). MSC: 03B15 03B40 03E40 68N18 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Jaber}, Log. Epistemol. Unity Sci. 27, 203--213 (2012; Zbl 1312.03021) Full Text: DOI Link
Coquand, Thierry; Spiwack, Arnaud A proof of strong normalisation using domain theory. (English) Zbl 1131.68038 Log. Methods Comput. Sci. 3, No. 4, Paper 12, 16 p. (2007). MSC: 68N18 03B40 68N30 68Q55 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{A. Spiwack}, Log. Methods Comput. Sci. 3, No. 4, Paper 12, 16 p. (2007; Zbl 1131.68038) Full Text: DOI
Abel, Andreas; Coquand, Thierry Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. (English) Zbl 1121.68026 Fundam. Inform. 77, No. 4, 345-395 (2007). MSC: 68N30 03B40 68N18 PDFBibTeX XMLCite \textit{A. Abel} and \textit{T. Coquand}, Fundam. Inform. 77, No. 4, 345--395 (2007; Zbl 1121.68026)
Coquand, Thierry The completeness of typing for context-semantics. (English) Zbl 1146.03005 Fundam. Inform. 77, No. 4, 293-301 (2007). Reviewer: Martin W. Bunder (Wollongong) MSC: 03B40 PDFBibTeX XMLCite \textit{T. Coquand}, Fundam. Inform. 77, No. 4, 293--301 (2007; Zbl 1146.03005)
Barthe, Gilles; Coquand, Thierry Remarks on the equational theory of non-normalizing pure type systems. (English) Zbl 1088.68033 J. Funct. Program. 16, No. 2, 137-155 (2006). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{G. Barthe} and \textit{T. Coquand}, J. Funct. Program. 16, No. 2, 137--155 (2006; Zbl 1088.68033) Full Text: DOI
Abel, Andreas; Coquand, Thierry Untyped algorithmic equality for Martin-Löf’s logical framework with surjective pairs. (English) Zbl 1112.68346 Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 23-38 (2005). MSC: 68N30 03B40 68N18 PDFBibTeX XMLCite \textit{A. Abel} and \textit{T. Coquand}, Lect. Notes Comput. Sci. 3461, 23--38 (2005; Zbl 1112.68346) Full Text: DOI
Coquand, Thierry Completeness theorems and \(\lambda\)-calculus. (English) Zbl 1112.03307 Urzyczyn, Paweł (ed.), Typed lambda calculi and applications. 7th international conference, TLCA 2005, Nara, Japan, April 21–23, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25593-1/pbk). Lecture Notes in Computer Science 3461, 1-9 (2005). MSC: 03B40 PDFBibTeX XMLCite \textit{T. Coquand}, Lect. Notes Comput. Sci. 3461, 1--9 (2005; Zbl 1112.03307) Full Text: DOI
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto A logical framework with dependently typed records. (English) Zbl 1095.03017 Fundam. Inform. 65, No. 1-2, 113-134 (2005). Reviewer: Neculai Curteanu (Iaşi) MSC: 03B70 68N18 03F35 03B35 03B40 68Q65 68Q60 68Q55 68T15 68T20 PDFBibTeX XMLCite \textit{T. Coquand} et al., Fundam. Inform. 65, No. 1--2, 113--134 (2005; Zbl 1095.03017)
Barthe, Gilles; Coquand, Thierry Remarks on the equational theory of non-normalizing pure type systems. (English) Zbl 1088.68032 J. Funct. Program. 14, No. 2, 191-209 (2004). MSC: 68N18 03B40 PDFBibTeX XMLCite \textit{G. Barthe} and \textit{T. Coquand}, J. Funct. Program. 14, No. 2, 191--209 (2004; Zbl 1088.68032) Full Text: DOI
Coquand, Thierry; Pollack, Randy; Takeyama, Makoto A logical framework with dependently typed records. (English) Zbl 1052.68018 Hofmann, Martin (ed.), Typed lambda calculi and applications. 6th international conference, TLCA 2003, Valencia, Spain, June 10–12, 2003. Proceedings. Berlin: Springer (ISBN 3-540-40332-9/pbk). Lect. Notes Comput. Sci. 2701, 105-119 (2003). Reviewer: Neculai Curteanu (Iaşi) MSC: 68N18 03B70 03B40 68Q55 68Q60 68Q65 68T15 PDFBibTeX XMLCite \textit{T. Coquand} et al., Lect. Notes Comput. Sci. 2701, 105--119 (2003; Zbl 1052.68018) Full Text: Link
Barthe, Gilles; Coquand, Thierry An introduction to dependent type theory. (English) Zbl 1065.68025 Barthe, Gilles (ed.) et al., Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Berlin: Springer (ISBN 3-540-44044-5). Lect. Notes Comput. Sci. 2395, 1-41 (2002). MSC: 68N18 68Q55 68-02 03B40 PDFBibTeX XMLCite \textit{G. Barthe} and \textit{T. Coquand}, Lect. Notes Comput. Sci. 2395, 1--41 (2002; Zbl 1065.68025) Full Text: Link
Altenkirch, Thorsten; Coquand, Thierry A finitary subsystem of the polymorphic \(\lambda\)-calculus. (English) Zbl 0981.03020 Abramsky, Samson (ed.), Typed lambda calculi and applications. 5th international conference, TLCA 2001, Kraków, Poland, May 2-5, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2044, 22-28 (2001). MSC: 03B40 PDFBibTeX XMLCite \textit{T. Altenkirch} and \textit{T. Coquand}, Lect. Notes Comput. Sci. 2044, 22--28 (2001; Zbl 0981.03020) Full Text: Link
Coquand, Thierry; Dybjer, Peter Intuitionistic model constructions and normalization proofs. (English) Zbl 0883.03009 Math. Struct. Comput. Sci. 7, No. 1, 75-94 (1997). Reviewer: N.Bernard (Le Bourget du Lac) MSC: 03B40 03B70 03F35 68Q55 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{P. Dybjer}, Math. Struct. Comput. Sci. 7, No. 1, 75--94 (1997; Zbl 0883.03009) Full Text: DOI
Coquand, Thierry Infinite objects in type theory. (English) Zbl 1527.03008 Barendregt, Henk (ed.) et al., TYPES ’93. Types for proofs and programs. International workshop, Nijmegen, the Netherlands, May 24–28, 1993. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 806, 62-78 (1994). MSC: 03B38 03B40 03B70 68N18 PDFBibTeX XMLCite \textit{T. Coquand}, Lect. Notes Comput. Sci. 806, 62--78 (1994; Zbl 1527.03008) Full Text: DOI
Coquand, Thierry; Herbelin, Hugo \(A\)-translation and looping combinators in pure type systems. (English) Zbl 0817.03007 J. Funct. Program. 4, No. 1, 77-88 (1994). MSC: 03B40 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{H. Herbelin}, J. Funct. Program. 4, No. 1, 77--88 (1994; Zbl 0817.03007) Full Text: DOI
Coquand, Thierry A new paradox in type theory. (English) Zbl 0821.03005 Prawitz, D. (ed.) et al., Logic, methodology and philosophy of science IX. Proceedings of the ninth international congress of logic, methodology and philosophy of science, Uppsala, Sweden, August 7-14, 1991. Amsterdam: North-Holland. Stud. Logic Found. Math. 134, 555-570 (1994). Reviewer: M.W.Bunder (Wollongong) MSC: 03B40 03B15 PDFBibTeX XMLCite \textit{T. Coquand}, Stud. Logic Found. Math. 134, 555--570 (1994; Zbl 0821.03005)
Coquand, Thierry An algorithm for testing conversion in type theory. (English) Zbl 0754.03041 Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 255-279 (1991). Reviewer: Song Fangmin (Nanjing) MSC: 03F35 03B40 03B70 PDFBibTeX XMLCite \textit{T. Coquand}, in: Logical frameworks. Proceedings of the first annual workshop ''Logical frameworks: design, implementation and experiment'', held in Sophia- Antipolis, France, May 7-11, 1990. Cambridge etc.: Cambridge University Press. 255--279 (1991; Zbl 0754.03041)
Breazu-Tannen, V.; Coquand, T.; Gunter, C. A.; Scedrov, A. Inheritance and explicit coercion. (English) Zbl 0716.68012 Logic in computer science, Proc. 4th Annual Symp., Pacific Grove/CA (USA) 1989, 112-129 (1989). MSC: 68N01 68N15 03B40 68Q55 PDFBibTeX XML
Coquand, Thierry; Gunter, Carl; Winskel, Glynn Domain theoretic models of polymorphism. (English) Zbl 0683.03007 Inf. Comput. 81, No. 2, 123-167 (1989). Reviewer: G.Ciobanu MSC: 03B40 18B35 68Q60 PDFBibTeX XMLCite \textit{T. Coquand} et al., Inf. Comput. 81, No. 2, 123--167 (1989; Zbl 0683.03007) Full Text: DOI
Breazu-Tannen, Val; Coquand, Thierry Extensional models for polymorphism. (English) Zbl 0713.03005 Theor. Comput. Sci. 59, No. 1-2, 85-114 (1988). MSC: 03B40 68Q55 PDFBibTeX XMLCite \textit{V. Breazu-Tannen} and \textit{T. Coquand}, Theor. Comput. Sci. 59, No. 1--2, 85--114 (1988; Zbl 0713.03005) Full Text: DOI Link
Coquand, Thierry; Huet, Gérard The calculus of constructions. (English) Zbl 0654.03045 Inf. Comput. 76, No. 2-3, 95-120 (1988). Reviewer: T.Coquand MSC: 03F35 03B40 68N01 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Huet}, Inf. Comput. 76, No. 2--3, 95--120 (1988; Zbl 0654.03045) Full Text: DOI
Coquand, Thierry; Gunter, Carl; Winskel, Glynn dI-domains as a model of polymorphism. (English) Zbl 0644.68041 Mathematical foundations of programming language semantics, Proc. Workshop, New Orleans/La. 1987, Lect. Notes Comput. Sci. 298, 344-363 (1988). MSC: 68Q65 68N01 03B40 PDFBibTeX XML
Coquand, Thierry; Ehrhard, Thomas An equational presentation of higher order logic. (English) Zbl 0643.03050 Category theory and computer science, Proc. Conf., Edinburgh/U.K. 1987, Lect. Notes Comput. Sci. 283, 40-56 (1987). Reviewer: M.Eytan MSC: 03G30 03F35 68Q60 18D30 03B40 PDFBibTeX XML
Breazu-Tannen, Val; Coquand, Thierry Extensional models for polymorphism. (English) Zbl 0636.03005 TAPSOFT ’87, Proc. Int. Conf. Software development, Pisa/Italy 1987, Vol. 2: Functional and logic programming and specifications, Lect. Notes Comput. Sci. 250, 291-307 (1987). MSC: 03B40 68N01 PDFBibTeX XML
Coquand, Thierry Sur l’analogie entre les propositions et les types. (French) Zbl 0648.03006 Combinators and functional programming languages, Proc. 13th Spring Sch. LITP, Val d’Ajol/France 1985, Lect. Notes Comput. Sci. 242, 71-84 (1986). MSC: 03B40 68Q60 03F35 PDFBibTeX XML
Coquand, Thierry; Huet, Gérard A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction. (English) Zbl 0591.68036 J. Symb. Comput. 1, 323-328 (1985). MSC: 68Q65 68Q60 03Fxx 03B35 03B15 03B40 03F55 68T15 00A15 PDFBibTeX XMLCite \textit{T. Coquand} and \textit{G. Huet}, J. Symb. Comput. 1, 323--328 (1985; Zbl 0591.68036) Full Text: DOI
Coquand, Thierry; Huet, Gérard Constructions: A higher order proof system for mechanizing mathematics. (English) Zbl 0581.03007 Computer algebra, EUROCAL ’85, Proc. Eur. Conf., Linz/Austria 1985, Vol. 1, Lect. Notes Comput. Sci. 203, 151-184 (1985). Reviewer: J.Zlatuska MSC: 03B35 03B40 03B15 68T15 03F50 68Q65 03F55 PDFBibTeX XML