Fridlender, Daniel; Pagano, Miguel A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation. (English) Zbl 1273.03106 Hasegawa, Masahito (ed.), Typed lambda calculi and applications. 11th international conference, TLCA 2013, Eindhoven, The Netherlands, June 26–28, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38945-0/pbk). Lecture Notes in Computer Science 7941, 140-155 (2013). Reviewer: Johan Georg Granström (Zürich) MSC: 03B70 03F55 PDFBibTeX XMLCite \textit{D. Fridlender} and \textit{M. Pagano}, Lect. Notes Comput. Sci. 7941, 140--155 (2013; Zbl 1273.03106) Full Text: DOI
Hart, Bradd (ed.); Kucera, Thomas G. (ed.); Pillay, Anand (ed.); Scott, Philip J. (ed.); Seely, Robert A. G. (ed.) Models, logics, and higher-dimensional categories: A tribute to the work of Mihály Makkai. Proceedings of a conference, CRM, Montréal, Canada, June 18–20, 2009. (English) Zbl 1243.03004 CRM Proceedings and Lecture Notes 53. Providence, RI: American Mathematical Society (AMS) (ISBN 978-0-8218-7281-9/pbk). x, 426 p. (2011). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03-06 03C45 03C52 03C90 03G30 18C10 18D05 18D30 00B25 00B30 PDFBibTeX XMLCite \textit{B. Hart} (ed.) et al., Models, logics, and higher-dimensional categories: A tribute to the work of Mihály Makkai. Proceedings of a conference, CRM, Montréal, Canada, June 18--20, 2009. Providence, RI: American Mathematical Society (AMS) (2011; Zbl 1243.03004)
van den Berg, Benno; Garner, Richard Types are weak \(\omega \)-groupoids. (English) Zbl 1229.18007 Proc. Lond. Math. Soc. (3) 102, No. 2, 370-394 (2011). Reviewer: Ulrich Knauer (Oldenburg) MSC: 18D05 03B15 18D50 PDFBibTeX XMLCite \textit{B. van den Berg} and \textit{R. Garner}, Proc. Lond. Math. Soc. (3) 102, No. 2, 370--394 (2011; Zbl 1229.18007) Full Text: DOI arXiv
Tupailo, Sergei Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe. (English) Zbl 1022.03045 Ann. Pure Appl. Logic 120, No. 1-3, 165-196 (2003). Reviewer: Andrea Cantini (Firenze) MSC: 03F50 03F65 03E70 03F25 PDFBibTeX XMLCite \textit{S. Tupailo}, Ann. Pure Appl. Logic 120, No. 1--3, 165--196 (2003; Zbl 1022.03045) Full Text: DOI
Valentini, Silvio On the formal points of the formal topology of the binary tree. (English) Zbl 1024.03064 Arch. Math. Logic 41, No. 7, 603-618 (2002). MSC: 03F65 54A05 03F35 03F50 PDFBibTeX XMLCite \textit{S. Valentini}, Arch. Math. Logic 41, No. 7, 603--618 (2002; Zbl 1024.03064) Full Text: DOI
Fridlender, Daniel A proof-irrelevant model of Martin-Löf’s logical framework. (English) Zbl 1029.03049 Math. Struct. Comput. Sci. 12, No. 6, 771-795 (2002). MSC: 03F50 03F35 03B40 PDFBibTeX XMLCite \textit{D. Fridlender}, Math. Struct. Comput. Sci. 12, No. 6, 771--795 (2002; Zbl 1029.03049) Full Text: DOI
Tsukada, Yasuyuki Martin-Löf’s type theory as an open-ended framework. (English) Zbl 1320.03065 Int. J. Found. Comput. Sci. 12, No. 1, 31-67 (2001); errata ibid. 12, No. 5, 695 (2001). MSC: 03B70 03F35 68N18 PDFBibTeX XMLCite \textit{Y. Tsukada}, Int. J. Found. Comput. Sci. 12, No. 1, 31--67 (2001; Zbl 1320.03065) Full Text: DOI
Severi, Paula; Szasz, Nora Studies of a theory of specifications with built-in program extraction. (English) Zbl 1010.68092 J. Autom. Reasoning 27, No. 1, 61-87 (2001). MSC: 68Q60 PDFBibTeX XMLCite \textit{P. Severi} and \textit{N. Szasz}, J. Autom. Reasoning 27, No. 1, 61--87 (2001; Zbl 1010.68092) Full Text: DOI
Kamareddine, Fairouz; Laan, Twan A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems. (English) Zbl 0977.03011 J. Logic Lang. Inf. 10, No. 3, 375-402 (2001). MSC: 03B35 03F35 PDFBibTeX XMLCite \textit{F. Kamareddine} and \textit{T. Laan}, J. Logic Lang. Inf. 10, No. 3, 375--402 (2001; Zbl 0977.03011) Full Text: DOI
Hinzen, Wolfram Anti-realist semantics. (English) Zbl 0969.03011 Erkenntnis 52, No. 3, 281-311 (2000). MSC: 03A05 PDFBibTeX XMLCite \textit{W. Hinzen}, Erkenntnis 52, No. 3, 281--311 (2000; Zbl 0969.03011) Full Text: DOI
Setzer, Anton Extending Martin-Löf type theory by one Mahlo-universe. (English) Zbl 0943.03046 Arch. Math. Logic 39, No. 3, 155-181 (2000). Reviewer: Anton Setzer (Uppsala) MSC: 03F35 03F15 PDFBibTeX XMLCite \textit{A. Setzer}, Arch. Math. Logic 39, No. 3, 155--181 (2000; Zbl 0943.03046) Full Text: DOI
Fridlender, Daniel An interpretation of the fan theorem in type theory. (English) Zbl 0943.03047 Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1657, 93-105 (1999). MSC: 03F35 PDFBibTeX XMLCite \textit{D. Fridlender}, Lect. Notes Comput. Sci. 1657, 93--105 (1999; Zbl 0943.03047)
Dybjer, Peter; Setzer, Anton A finite axiomatization of inductive-recursive definitions. (English) Zbl 0931.03069 Girard, Jean-Yves (ed.), Typed lambda calculi and applications. 4th international conference, TLCA ’99. L’Aquila, Italy, April 7–9, 1999. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1581, 129-146 (1999). MSC: 03F35 03E35 PDFBibTeX XMLCite \textit{P. Dybjer} and \textit{A. Setzer}, Lect. Notes Comput. Sci. 1581, 129--146 (1999; Zbl 0931.03069)
Rathjen, Michael; Griffor, Edward R.; Palmgren, Erik Inaccessibility in constructive set theory and type theory. (English) Zbl 0926.03074 Ann. Pure Appl. Logic 94, No. 1-3, 181-200 (1998). MSC: 03F50 03E55 03E70 03F65 03F35 PDFBibTeX XMLCite \textit{M. Rathjen} et al., Ann. Pure Appl. Logic 94, No. 1--3, 181--200 (1998; Zbl 0926.03074) Full Text: DOI
Setzer, Anton Well-ordering proofs for Martin-Löf type theory. (English) Zbl 0928.03067 Ann. Pure Appl. Logic 92, No. 2, 113-159 (1998). Reviewer: G.Mints (Stanford) MSC: 03F50 03F35 03F15 PDFBibTeX XMLCite \textit{A. Setzer}, Ann. Pure Appl. Logic 92, No. 2, 113--159 (1998; Zbl 0928.03067) Full Text: DOI
Leslie, Neil Tail-recursive non-canonical constants and continuations in Martin-Löf’s type theory. (English) Zbl 0924.68138 Grundy, Jim (ed.) et al., International refinement workshop and formal methods Pacific 1998. Proceedings of IRW/FMP ’98. Canberra, Australia, September 29 - October 2, 1998. Berlin: Springer. Springer Series in Discrete Mathematics and Theoretical Computer Science. 213-229 (1998). MSC: 68Q60 PDFBibTeX XMLCite \textit{N. Leslie}, in: International refinement workshop and formal methods Pacific 1998. Proceedings of IRW/FMP '98. Canberra, Australia, September 29 - October 2, 1998. Berlin: Springer. 213--229 (1998; Zbl 0924.68138)
Valentini, Silvio The forget-restore principle: A paradigmatic example. (English) Zbl 0937.03069 Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19-21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 275-283 (1998). MSC: 03F50 03F35 03B40 PDFBibTeX XMLCite \textit{S. Valentini}, in: Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19--21, 1995. Oxford: Clarendon Press. 275--283 (1998; Zbl 0937.03069)
Coquand, Catarina A realizability interpretation of Martin-Löf’s type theory. (English) Zbl 0937.03068 Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19-21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 73-82 (1998). MSC: 03F35 PDFBibTeX XMLCite \textit{C. Coquand}, in: Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19--21, 1995. Oxford: Clarendon Press. 73--82 (1998; Zbl 0937.03068)
Betarte, Gustavo; Tasistro, Alvaro Extension of Martin-Löf’s type theory with record types and subtyping. (English) Zbl 0930.03088 Sambin, Giovanni (ed.) et al., Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19–21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36, 21-39 (1998). MSC: 03F35 68Q65 PDFBibTeX XMLCite \textit{G. Betarte} and \textit{A. Tasistro}, in: Twenty-five years of constructive type theory. Proceedings of a congress, Venice, Italy, Ocober 19--21, 1995. Oxford: Clarendon Press. 21--39 (1998; Zbl 0930.03088)
Tasistro, Alvaro Abstract insertion sort in an extension of type theory with record types and subtyping. (English) Zbl 0927.03058 Giménez, Eduardo (ed.) et al., Types for proofs and programs. International workshop TYPES ’96, Aussois, France, December 15–19, 1996. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1512, 354-372 (1998). MSC: 03B70 68Q65 03F35 68P10 PDFBibTeX XMLCite \textit{A. Tasistro}, Lect. Notes Comput. Sci. 1512, 354--372 (1998; Zbl 0927.03058)
Fridlender, Daniel Higman’s lemma in type theory. (English) Zbl 0927.03080 Giménez, Eduardo (ed.) et al., Types for proofs and programs. International workshop TYPES ’96, Aussois, France, December 15–19, 1996. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1512, 112-133 (1998). MSC: 03F35 03B35 PDFBibTeX XMLCite \textit{D. Fridlender}, Lect. Notes Comput. Sci. 1512, 112--133 (1998; Zbl 0927.03080)
Hedberg, Michael A coherence theorem for Martin-Löf’s type theory. (English) Zbl 0917.03028 J. Funct. Program. 8, No. 4, 413-436 (1998). MSC: 03F35 03G30 03B40 PDFBibTeX XMLCite \textit{M. Hedberg}, J. Funct. Program. 8, No. 4, 413--436 (1998; Zbl 0917.03028) Full Text: DOI
Betarte, Gustavo Dependent record types and algebraic structures in type theory. (English) Zbl 0898.68048 Göteborg: Univ. Göteborg, Department of Computer Science, iii, 138, 69 p. (1998). MSC: 68Q65 68-02 PDFBibTeX XMLCite \textit{G. Betarte}, Dependent record types and algebraic structures in type theory. Göteborg: Univ. Göteborg, Department of Computer Science (1998; Zbl 0898.68048)
Dybjer, Peter Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. (English) Zbl 0898.68047 Theor. Comput. Sci. 176, No. 1-2, 329-335 (1997). MSC: 68Q60 PDFBibTeX XMLCite \textit{P. Dybjer}, Theor. Comput. Sci. 176, No. 1--2, 329--335 (1997; Zbl 0898.68047) Full Text: DOI
Setzer, Anton Translating set theoretical proofs into type theoretical programs. (English) Zbl 0884.03054 Gottlob, Georg (ed.) et al., Computational logic and proof theory. 5th Kurt Gödel Colloquium, KGC ’97. Vienna, Austria. August 25–29, 1997. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1289, 278-289 (1997). MSC: 03F03 03B70 03F05 03E70 03F35 PDFBibTeX XMLCite \textit{A. Setzer}, Lect. Notes Comput. Sci. 1289, 278--289 (1997; Zbl 0884.03054)
Fu, Yuxi Constructive sets in computable sets. (English) Zbl 0883.03043 J. Comput. Sci. Technol. 12, No. 5, 425-440 (1997). MSC: 03F50 03F35 03E70 PDFBibTeX XMLCite \textit{Y. Fu}, J. Comput. Sci. Technol. 12, No. 5, 425--440 (1997; Zbl 0883.03043) Full Text: DOI
Maguolo, Dario; Valentini, Silvio An intuitionistic version of Cantor’s theorem. (English) Zbl 0859.03029 Math. Log. Q. 42, No. 4, 446-448 (1996). MSC: 03F35 03F55 18D15 PDFBibTeX XMLCite \textit{D. Maguolo} and \textit{S. Valentini}, Math. Log. Q. 42, No. 4, 446--448 (1996; Zbl 0859.03029) Full Text: DOI
Preller, A.; Simonet, G. Functional completeness of the free locally cartesian closed category and interpretations of Martin-Löf’s theory of dependent types. (English) Zbl 0860.03044 Math. Struct. Comput. Sci. 6, No. 4, 387-408 (1996). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 03G30 18D30 18A15 03F35 PDFBibTeX XMLCite \textit{A. Preller} and \textit{G. Simonet}, Math. Struct. Comput. Sci. 6, No. 4, 387--408 (1996; Zbl 0860.03044) Full Text: DOI
Valentini, Silvio Decidability in intuitionistic type theory is functionally decidable. (English) Zbl 0854.03008 Math. Log. Q. 42, No. 3, 300-304 (1996). Reviewer: J.M.Plotkin (East Lansing) MSC: 03B25 03F35 03F55 PDFBibTeX XMLCite \textit{S. Valentini}, Math. Log. Q. 42, No. 3, 300--304 (1996; Zbl 0854.03008) Full Text: DOI
Fu, Yuxi Recursive models of general inductive types. (English) Zbl 0846.68063 Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 26, No. 2, 115-131 (1996). MSC: 68Q55 PDFBibTeX XMLCite \textit{Y. Fu}, Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 26, No. 2, 115--131 (1996; Zbl 0846.68063)
Palmgren, Erik The Friedman-translation for Martin-Löf’s type theory. (English) Zbl 0827.03035 Math. Log. Q. 41, No. 3, 314-326 (1995). MSC: 03F50 03F35 03B15 03F25 03B40 PDFBibTeX XMLCite \textit{E. Palmgren}, Math. Log. Q. 41, No. 3, 314--326 (1995; Zbl 0827.03035) Full Text: DOI
Griffor, Edward; Rathjen, Michael The strength of some Martin-Löf type theories. (English) Zbl 0819.03047 Arch. Math. Logic 33, No. 5, 347-385 (1994). Reviewer: M.Yasuhara (Princeton) MSC: 03F35 03F50 PDFBibTeX XMLCite \textit{E. Griffor} and \textit{M. Rathjen}, Arch. Math. Logic 33, No. 5, 347--385 (1994; Zbl 0819.03047) Full Text: DOI
Song, Fangmin On the generalization of disjoint union and the definability of finite types in Martin-Löf’s type theory. (Chinese) Zbl 0921.03055 Chin. Ann. Math., Ser. A 15, No. 4, 472-477 (1994). MSC: 03F35 PDFBibTeX XMLCite \textit{F. Song}, Chin. Ann. Math., Ser. A 15, No. 4, 472--477 (1994; Zbl 0921.03055)
Dybjer, Peter Inductive families. (English) Zbl 0808.03044 Formal Asp. Comput. 6, No. 4, 440-465 (1994). MSC: 03F35 03B70 PDFBibTeX XMLCite \textit{P. Dybjer}, Formal Asp. Comput. 6, No. 4, 440--465 (1994; Zbl 0808.03044) Full Text: DOI
Song, Fangmin Adding new forms of judgements to Martin-Löf’s type theory. (Chinese) Zbl 0827.03034 Chin. Ann. Math., Ser. A 15, No. 2, 177-184 (1994). Reviewer: Li Xiang (Guiyang) MSC: 03F35 03B25 PDFBibTeX XMLCite \textit{F. Song}, Chin. Ann. Math., Ser. A 15, No. 2, 177--184 (1994; Zbl 0827.03034)
Grasmik, A. V. Representation of \(\Sigma\)-programs in the intuitionistic theory of types. (Russian) Zbl 0816.03016 Vychisl. Sist. 148, 32-39 (1993). Reviewer: G.Mints (Stanford) MSC: 03B70 03F35 68N01 03D25 PDFBibTeX XMLCite \textit{A. V. Grasmik}, Vychisl. Sist. 148, 32--39 (1993; Zbl 0816.03016)
Palmgren, Erik An information system interpretation of Martin-Löf’s partial type theory with universes. (English) Zbl 0789.03045 Inf. Comput. 106, No. 1, 26-60 (1993). MSC: 03F35 68Q55 03B15 PDFBibTeX XMLCite \textit{E. Palmgren}, Inf. Comput. 106, No. 1, 26--60 (1993; Zbl 0789.03045) Full Text: DOI
Harper, Robert Constructing type systems over an operational semantics. (English) Zbl 0766.68088 J. Symb. Comput. 14, No. 1, 71-84 (1992). MSC: 68Q55 03F35 PDFBibTeX XMLCite \textit{R. Harper}, J. Symb. Comput. 14, No. 1, 71--84 (1992; Zbl 0766.68088) Full Text: DOI
Palmgren, Erik Type-theoretic interpretation of iterated, strictly positive inductive definitions. (English) Zbl 0787.03052 Arch. Math. Logic 32, No. 2, 75-99 (1992). MSC: 03F35 PDFBibTeX XMLCite \textit{E. Palmgren}, Arch. Math. Logic 32, No. 2, 75--99 (1992; Zbl 0787.03052) Full Text: DOI
Palmgren, Erik; Stoltenberg-Hansen, Viggo Remarks on Martin-Löf’s partial type theory. (English) Zbl 0787.03051 BIT 32, No. 1, 70-83 (1992). MSC: 03F35 PDFBibTeX XMLCite \textit{E. Palmgren} and \textit{V. Stoltenberg-Hansen}, BIT 32, No. 1, 70--83 (1992; Zbl 0787.03051) Full Text: DOI
Luo, Zhaohui A unifying theory of dependent types: The schematic approach. (English) Zbl 0978.03521 Nerode, A. (ed.) et al., Logical foundations of computer science. Tver ’92, 2nd international symposium, Tver, Russia, July 20-24, 1992. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 620, 293-304 (1992). MSC: 03B70 PDFBibTeX XMLCite \textit{Z. Luo}, Lect. Notes Comput. Sci. 620, 293--304 (1992; Zbl 0978.03521)
Swaen, M. D. G. A characterization of ML in many-sorted arithmetic with conditional application. (English) Zbl 0767.03030 J. Symb. Log. 57, No. 3, 924-953 (1992). Reviewer: M.D.G.Swaen (Amsterdam) MSC: 03F50 03F35 PDFBibTeX XMLCite \textit{M. D. G. Swaen}, J. Symb. Log. 57, No. 3, 924--953 (1992; Zbl 0767.03030) Full Text: DOI
Ranta, Aarne Constructing possible worlds. (English) Zbl 0838.03046 Theoria 57, No. 1-2, 77-100 (1991). MSC: 03F50 PDFBibTeX XMLCite \textit{A. Ranta}, Theoria 57, No. 1--2, 77--100 (1991; Zbl 0838.03046) Full Text: DOI
Dybjer, Peter Inductive sets and families in Martin-Löf’s type theory and their set- theoretic semantics. (English) Zbl 0755.03033 Logical frameworks, Proc. 1st Annu. Workshop, Sophia-Antipolis/Fr. 1990, 280-306 (1991). Reviewer: M.W.Bunder (Wollongong) MSC: 03F35 03B40 PDFBibTeX XMLCite \textit{P. Dybjer}, 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. 280--306 (1991; Zbl 0755.03033)
Hedberg, Michael Normalising the associative law: An experiment with Martin-Löf’s type theory. (English) Zbl 0732.03023 Formal Aspects Comput. 3, No. 2, 218-252 (1991). Reviewer: N.Curteanu (Iaşi) MSC: 03B70 03F35 68N01 68Q60 03-04 68T15 PDFBibTeX XMLCite \textit{M. Hedberg}, Formal Asp. Comput. 3, No. 2, 218--252 (1991; Zbl 0732.03023) Full Text: DOI
Luo, Zhaohui A higher-order calculus and theory abstraction. (English) Zbl 0719.03004 Inf. Comput. 90, No. 1, 107-137 (1991). Reviewer: Z.Luo MSC: 03B15 03F35 68Q60 03B70 PDFBibTeX XMLCite \textit{Z. Luo}, Inf. Comput. 90, No. 1, 107--137 (1991; Zbl 0719.03004) Full Text: DOI
Palmgren, Erik A construction of Type:Type in Martin-Löf’s partial type theory with one universe. (English) Zbl 0747.03027 J. Symb. Log. 56, No. 3, 1012-1015 (1991). Reviewer: R.Murawski (Poznań) MSC: 03F35 PDFBibTeX XMLCite \textit{E. Palmgren}, J. Symb. Log. 56, No. 3, 1012--1015 (1991; Zbl 0747.03027) Full Text: DOI
Hallnäs, Lars On the syntax of infinite objects: An extension of Martin-Löf’s theory of expressions. (English) Zbl 0733.03043 Colog-88, Proc. Int. Conf., Tallinn/USSR 1988, Lect. Not. Comput. Sci. 417, 94-104 (1990). MSC: 03F35 68Q55 PDFBibTeX XML
Renardel de Lavalette, Gerard R. Extended bar induction in applicative theories. (English) Zbl 0717.03024 Ann. Pure Appl. Logic 50, No. 2, 139-189 (1990). Reviewer: Song Fangmin MSC: 03F50 PDFBibTeX XMLCite \textit{G. R. Renardel de Lavalette}, Ann. Pure Appl. Logic 50, No. 2, 139--189 (1990; Zbl 0717.03024) Full Text: DOI
Pitts, Andrew M.; Taylor, Paul A note on Russell’s paradox in locally Cartesian closed categories. (English) Zbl 0702.03036 Stud. Log. 48, No. 3, 377-387 (1989). MSC: 03F35 03G30 18D15 PDFBibTeX XMLCite \textit{A. M. Pitts} and \textit{P. Taylor}, Stud. Log. 48, No. 3, 377--387 (1989; Zbl 0702.03036) Full Text: DOI
Smith, Jan M. Propositional functions and families of types. (English) Zbl 0694.03038 Notre Dame J. Formal Logic 30, No. 3, 442-458 (1989). Reviewer: Li Xiang MSC: 03F35 68Q65 68Q60 PDFBibTeX XMLCite \textit{J. M. Smith}, Notre Dame J. Formal Logic 30, No. 3, 442--458 (1989; Zbl 0694.03038) Full Text: DOI
Jacobs, Bart The inconsistency of higher order extensions of Martin-Löf’s type theory. (English) Zbl 0692.03034 J. Philos. Logic 18, No. 4, 399-422 (1989). Reviewer: B.van Rootselaar MSC: 03F35 PDFBibTeX XMLCite \textit{B. Jacobs}, J. Philos. Log. 18, No. 4, 399--422 (1989; Zbl 0692.03034) Full Text: DOI
Lindström, Ingrid A construction of non-well-founded sets within Martin-Löf’s type theory. (English) Zbl 0669.03028 J. Symb. Log. 54, No. 1, 57-64 (1989). Reviewer: R.Murawski MSC: 03F35 03F55 PDFBibTeX XMLCite \textit{I. Lindström}, J. Symb. Log. 54, No. 1, 57--64 (1989; Zbl 0669.03028) Full Text: DOI
Smith, Jan M. The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. (English) Zbl 0661.03045 J. Symb. Log. 53, No. 3, 840-845 (1988). Reviewer: J.Smith MSC: 03F35 03F30 PDFBibTeX XMLCite \textit{J. M. Smith}, J. Symb. Log. 53, No. 3, 840--845 (1988; Zbl 0661.03045) Full Text: DOI
Nordström, Bengt Terminating general recursion. (English) Zbl 0659.68020 BIT 28, No. 3, 605-619 (1988). Reviewer: B.Nordström MSC: 68Q60 03B70 03B15 68N01 PDFBibTeX XMLCite \textit{B. Nordström}, BIT 28, No. 3, 605--619 (1988; Zbl 0659.68020) Full Text: DOI
Rezus, Adrian Semantics of constructive type theory. (English) Zbl 0632.03047 Libertas Math. 6, 1-82 (1986). Reviewer: B.van Rootselaar MSC: 03F50 03B40 PDFBibTeX XMLCite \textit{A. Rezus}, Libertas Math. 6, 1--82 (1986; Zbl 0632.03047)
Nordström, Bengt Multilevel functions in Martin-Löf’s type theory. (English) Zbl 0585.68031 Programs as data objects, Proc. Workshop, Copenhagen/Den. 1985, Lect. Notes Comput. Sci. 217, 206-221 (1986). MSC: 68P05 68N01 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
Dybjer, Peter Program verification in a logical theory of constructions. (English) Zbl 0568.68015 Functional programming languages and computer architecture, 2nd Conf., Nancy/France 1985, Lect. Notes Comput. Sci. 201, 334-349 (1985). MSC: 68Q60 PDFBibTeX XML
Nordström, Bengt; Smith, Jan Propositions and specifications of programs in Martin-Löf’s type theory. (English) Zbl 0551.68027 BIT 24, 288-301 (1984). MSC: 68Q65 68Q60 PDFBibTeX XMLCite \textit{B. Nordström} and \textit{J. Smith}, BIT 24, 288--301 (1984; Zbl 0551.68027) Full Text: DOI
Schwichtenberg, Helmut On Martin-Löf’s theory of types. (English) Zbl 0537.03039 Atti degli incontri di logica matematica, Siena/Italia 1982, 299-325 (1983). Reviewer: B.van Rootselaar MSC: 03F50 03F05 03B15 03F55 PDFBibTeX XML