Maietti, Maria Emilia; Sabelli, Pietro Equiconsistency of the minimalist foundation with its classical version. (English) Zbl 07957190 Ann. Pure Appl. Logic 176, No. 2, Article ID 103524, 21 p. (2025). MSC: 03B15 03F25 03F55 03F50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Matthews, Richard; Rathjen, Michael Constructing the constructible universe constructively. (English) Zbl 07785165 Ann. Pure Appl. Logic 175, No. 3, Article ID 103392, 25 p. (2024). MSC: 03E45 03E70 03D65 03E10 03F55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Berg, Benno van den; Otten, Daniël Conservativity of Type Theory over Higher-order Arithmetic. arXiv:2308.15288 Preprint, arXiv:2308.15288 [math.LO] (2023). MSC: 03B38 03B16 03F55 03F50 × Cite Format Result Cite Full Text: arXiv
Petersen, Uwe Enhancing induction in a contraction free logic with unrestricted abstraction: from \(\mathbf{Z}\) to \(\mathbf{Z}_2\). (English) Zbl 07603656 Arch. Math. Logic 61, No. 7-8, 1007-1051 (2022). MSC: 03B15 03B47 03F52 × Cite Format Result Cite Review PDF Full Text: DOI
Mainzer, Klaus From mathesis universalis to provability, computability, and constructivity. (English) Zbl 1469.03113 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 203-234 (2019). MSC: 03D10 03D35 03F35 03F60 03B30 03F25 68V15 03B38 55U40 × Cite Format Result Cite Review PDF Full Text: DOI
Berardi, Stefano; Oliva, Paulo; Steila, Silvia An analysis of the Podelski-Rybalchenko termination theorem via bar recursion. (English) Zbl 1444.03140 J. Log. Comput. 29, No. 4, 555-575 (2019). MSC: 03D65 03F35 05D10 03F55 × Cite Format Result Cite Review PDF Full Text: DOI
Takahashi, Yuta; Takemura, Ryo Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms. (English) Zbl 1457.03023 J. Philos. Log. 48, No. 3, 553-570 (2019). MSC: 03B05 03B16 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Kawai, Tatsuji Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions. (English) Zbl 1461.03057 Ann. Pure Appl. Logic 170, No. 8, 891-909 (2019). MSC: 03F55 03F50 03F10 03D65 03F30 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Palmgren, Erik A constructive examination of a Russell-style ramified type theory. (English) Zbl 1522.03040 Bull. Symb. Log. 24, No. 1, 90-106 (2018). MSC: 03B38 03F35 03F50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Pistone, Paolo Polymorphism and the obstinate circularity of second order logic: a victims’ tale. (English) Zbl 1496.03023 Bull. Symb. Log. 24, No. 1, 1-52 (2018). MSC: 03A05 03F03 03F05 03B16 03B38 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Klev, Ansten Truthmaker semantics: Fine versus Martin-Löf. (English) Zbl 1418.03035 Arazim, Pavel (ed.) et al., The Logica yearbook 2016. Proceedings of the 30th annual international symposium Logica, Hejnice Monastery, Czech Republic, June 20–24, 2016. London: College Publications. 87-108 (2017). MSC: 03B20 03B15 03A05 × Cite Format Result Cite Review PDF
van Dalen, Dirk Logic and structure. Translated from the English by Ruy J. G. B. de Queiroz. (Lógica e estrutura.) (Portuguese) Zbl 1394.03001 Cadernos de Lógica e Computação 8. London: College Publications (ISBN 978-1-84890-262-6/pbk). 274 p. (2017). MSC: 03-01 03-02 03B05 03B10 03B15 03B20 03C07 03C20 × Cite Format Result Cite Review PDF
Berger, Ulrich; Hou, Tie A realizability interpretation of Church’s simple theory of types. (English) Zbl 1423.03044 Math. Struct. Comput. Sci. 27, No. 8, 1364-1385 (2017). MSC: 03B20 03B15 03B40 03D78 03F25 × Cite Format Result Cite Review PDF Full Text: DOI
Zeume, Thomas; Harwath, Frederik Order-invariance of two-variable logic is decidable. (English) Zbl 1394.03017 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 807-816 (2016). MSC: 03B25 03B15 03B20 68Q25 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Blot, Valentin Hybrid realizability for intuitionistic and classical choice. (English) Zbl 1394.03021 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 575-584 (2016). MSC: 03B40 03B20 03B15 03E25 03F30 × Cite Format Result Cite Review PDF Full Text: DOI
Swan, Andrew An algebraic weak factorisation system on 01-substitution sets: a constructive proof. (English) Zbl 1403.03124 J. Log. Anal. 8, Paper No. 1, 35 p. (2016). MSC: 03F50 03F55 55U35 03F60 03B15 18A32 18C20 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Escardó, Martín; Xu, Chuangjie A constructive manifestation of the Kleene-Kreisel continuous functionals. (English) Zbl 1402.03020 Ann. Pure Appl. Logic 167, No. 9, 770-793 (2016). MSC: 03B15 03F50 03C90 03D65 × Cite Format Result Cite Review PDF Full Text: DOI
Gentilini, Paolo; Martelli, Maurizio; Rosolini, Giuseppe Explicit constructive logic ECL: a new representation of construction and selection of logical information by an epistemic agent. (English) Zbl 1382.03036 Fundam. Inform. 140, No. 3-4, 357-372 (2015). MSC: 03B15 03B20 03B53 03F50 × Cite Format Result Cite Review PDF Full Text: DOI
Maietti, Maria Emilia; Rosolini, Giuseppe Unifying exact completions. (English) Zbl 1386.03074 Appl. Categ. Struct. 23, No. 1, 43-52 (2015). MSC: 03G30 03B15 18C50 03F55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Olkhovikov, Grigory K.; Schroeder-Heister, Peter On flattening elimination rules. (English) Zbl 1329.03087 Rev. Symb. Log. 7, No. 1, 60-72 (2014). MSC: 03F05 03F07 03B20 03B15 × Cite Format Result Cite Review PDF Full Text: DOI
Brown, Chad E.; Rizkallah, Christine Glivenko and Kuroda for simple type theory. (English) Zbl 1337.03015 J. Symb. Log. 79, No. 2, 485-495 (2014). MSC: 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI Link
Liang, Chuck; Miller, Dale Unifying classical and intuitionistic logics for computational control. (English) Zbl 1367.03058 Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 283-292 (2013). MSC: 03B70 03B05 03B15 03B20 68N15 × Cite Format Result Cite Review PDF Full Text: DOI
Kachapova, F. A generalization of Beth model to functionals of high types. (English) Zbl 1364.03085 Downey, Rod (ed.) et al., Proceedings of the 12th Asian logic conference, Wellington, New Zealand, December 15–20, 2011. Hackensack, NJ: World Scientific (ISBN 978-981-4449-26-7/hbk; 978-981-4449-28-1/ebook). 185-209 (2013). MSC: 03F55 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Bucalo, Anna; Rosolini, Giuseppe Topologies and free constructions. (English) Zbl 1344.03052 Log. Log. Philos. 22, No. 3, 327-346 (2013). MSC: 03G30 03B15 18C50 03B20 03F55 × Cite Format Result Cite Review PDF Full Text: DOI
Maietti, Maria Emilia; Sambin, Giovanni Why topology in the minimalist foundation must be pointfree. (English) Zbl 1341.03097 Log. Log. Philos. 22, No. 2, 167-199 (2013). MSC: 03G30 03B15 18C50 03B20 03F55 × Cite Format Result Cite Review PDF Full Text: DOI
Maietti, Maria Emilia; Rosolini, Giuseppe Quotient completion for the foundation of constructive mathematics. (English) Zbl 1288.03049 Log. Univers. 7, No. 3, 371-402 (2013). MSC: 03G30 03B15 03F55 18C50 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Yang, Fan Expressing second-order sentences in intuitionistic dependence logic. (English) Zbl 1272.03126 Stud. Log. 101, No. 2, 323-342 (2013). MSC: 03B60 03B15 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
van Dalen, Dirk Logic and structure. 5th revised and expanded ed. (English) Zbl 1262.03002 Universitext. London: Springer (ISBN 978-1-4471-4557-8/pbk; 978-1-4471-4558-5/ebook). x, 263 p. (2013). Reviewer: Branislav Boričić (Beograd) MSC: 03-01 03-02 03B05 03B10 03B15 03B20 03C07 03C20 × Cite Format Result Cite Review PDF Full Text: DOI
Benzmüller, Christoph Combining and automating classical and non-classical logics in classical higher-order logics. (English) Zbl 1252.03025 Ann. Math. Artif. Intell. 62, No. 1-2, 103-128 (2011). MSC: 03B35 03B62 03B42 03B45 03B20 03B15 68T27 68T30 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Figueira, Santiago; Gorín, Daniel; Grimson, Rafael On the expressive power of IF-logic with classical negation. (English) Zbl 1328.03029 Beklemishev, Lev D. (ed.) et al., Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18–20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20919-2/pbk). Lecture Notes in Computer Science 6642. Lecture Notes in Artificial Intelligence, 135-145 (2011). MSC: 03B60 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Benzmüller, Christoph; Paulson, Lawrence C. Multimodal and intuitionistic logics in simple type theory. (English) Zbl 1222.03023 Log. J. IGPL 18, No. 6, 881-892 (2010). Reviewer: Viorica Sofronie-Stokkermans (Saarbrücken) MSC: 03B45 03B15 03B20 03B35 68T15 × Cite Format Result Cite Review PDF Full Text: DOI Link
Sørensen, Morten H.; Urzyczyn, Paweł A syntactic embedding of predicate logic into second-order propositional logic. (English) Zbl 1216.03029 Notre Dame J. Formal Logic 51, No. 4, 457-473 (2010). MSC: 03B20 03B15 03B25 × Cite Format Result Cite Review PDF Full Text: DOI
Hermant, Olivier; Lipton, James Completeness and cut-elimination in the intuitionistic theory of types. II. (English) Zbl 1188.03042 J. Log. Comput. 20, No. 2, 597-602 (2010). MSC: 03F05 03B15 × Cite Format Result Cite Review PDF Full Text: DOI
Miranda Perea, Favio Ezequiel Propositional logic of second order. (Spanish) Zbl 1253.03031 Aguilar, M. (ed.) et al., Memorias de la Sociedad Matemática Mexicana. México: Sociedad Matemática Mexicana; México: Universidad Nacional Autónoma de México (UNAM). Aportaciones Matemáticas. Comunicaciones 40, 87-120 (2009). Reviewer: Max A. Freund (San José) MSC: 03B15 03B70 03C85 × Cite Format Result Cite Review PDF
Garner, Richard On the strength of dependent products in the type theory of Martin-Löf. (English) Zbl 1171.03004 Ann. Pure Appl. Logic 160, No. 1, 1-12 (2009). MSC: 03B15 03F55 × Cite Format Result Cite Review PDF Full Text: DOI arXiv
Buisse, Alexandre; Dybjer, Peter The interpretation of intuitionistic type theory in locally Cartesian closed categories – an intuitionistic perspective. (English) Zbl 1286.03029 Bauer, Andrej (ed.) et al., Proceedings of the 24th conference on the mathematical foundations of programming semantics (MFPS XXIV), Philadelphia, PA, USA, May 22–25, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 218, 21-32 (2008). MSC: 03B15 18D15 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Hermant, Olivier; Lipton, James Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively. (English) Zbl 1226.03061 Benzmüller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 115-148 (2008). MSC: 03F05 03B15 × Cite Format Result Cite Review PDF
Constable, Robert L.; Moczydlowski, Wojciech Extracting programs from constructive HOL proofs via IZF set-theoretic semantics. (English) Zbl 1147.03013 Log. Methods Comput. Sci. 4, No. 3, Paper 5, 17 p. (2008). MSC: 03B70 03B15 03B35 03E70 68N30 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Colson, Loïc; Michel, David Pedagogical second-order propositional calculi. (English) Zbl 1155.03008 J. Log. Comput. 18, No. 4, 669-695 (2008). Reviewer: G. E. Mints (Stanford) MSC: 03B20 03B15 03B40 03F07 × Cite Format Result Cite Review PDF Full Text: DOI
Belo, João Filipe Dependently sorted logic. (English) Zbl 1139.03020 Miculan, Marino (ed.) et al., Types for proofs and programs. International conference, TYPES 2007, Cividale des Friuli, Italy, May 2–5, 2007. Revised selected papers. Berlin: Springer (ISBN 978-3-540-68084-0/pbk). Lecture Notes in Computer Science 4941, 33-50 (2008). MSC: 03B70 03B10 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Hindley, J. Roger Basic simple type theory. Paperback reprint with corrections. (English) Zbl 1135.03006 Cambridge Tracts in Theoretical Computer Science 42. Cambridge: Cambridge University Press (ISBN 978-0-521-05422-5/pbk). xii, 186 p. (2008). Reviewer: Reinhard Kahle (Coimbra) MSC: 03B40 03B70 03B20 68-01 03-01 03B15 68N15 68N18 × Cite Format Result Cite Review PDF
Maietti, Maria Emilia Quotients over minimal type theory. (English) Zbl 1151.03032 Cooper, S. Barry (ed.) et al., Computation and logic in the real world. Third conference on computability in Europe, CiE 2007, Siena, Italy, June 18–23, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-73000-2/pbk). Lecture Notes in Computer Science 4497, 517-531 (2007). MSC: 03F65 03F35 03G30 × Cite Format Result Cite Review PDF Full Text: DOI
Pataraia, Dimitri Description of all functions definable by formulae of the 2nd order intuitionistic propositional calculus on some linear Heyting algebras. (English) Zbl 1186.03016 J. Appl. Non-Class. Log. 16, No. 3-4, 457-483 (2006). MSC: 03B15 03B20 06D20 × Cite Format Result Cite Review PDF Full Text: DOI
Urzyczyn, Paweł Predicates as types. (English) Zbl 1127.03318 Schwichtenberg, Helmut (ed.) et al., Proof technology and computation. Papers from the summer school, Marktoberdorf, Germany, July 29–August 10, 2003. Amsterdam: IOS Press (ISBN 1-58603-625-4/hbk). NATO Science Series III: Computer & Systems Sciences 200, 355-386 (2006). MSC: 03B10 03B15 03B20 03B40 03D20 03F30 03F05 × Cite Format Result Cite Review PDF
Saito, Hirofumi Type theory and the theory of meaning – towards an intuitionistic view of language. (English) Zbl 1113.03305 Ann. Jap. Assoc. Philos. Sci. 14, No. 2, 113-121 (2006). MSC: 03A05 03B15 03B65 × Cite Format Result Cite Review PDF Full Text: DOI
Ferreira, Fernando Comments on predicative logic. (English) Zbl 1101.03014 J. Philos. Log. 35, No. 1, 1-8 (2006). MSC: 03B20 03B15 03A05 × Cite Format Result Cite Review PDF Full Text: DOI
Ghilardi, Silvio; Nicolini, Enrica; Zucchelli, Daniele A comprehensive framework for combined decision procedures. (English) Zbl 1171.03306 Gramlich, Bernhard (ed.), Frontiers of combining systems. 5th international workshop, FroCos 2005, Vienna, Austria, September 19–21, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29051-6/pbk). Lecture Notes in Computer Science 3717. Lecture Notes in Artificial Intelligence, 1-30 (2005). MSC: 03B25 03B15 03B20 03B35 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
Gilmore, Paul C. Logicism renewed. Logical foundations for mathematics and computer science. (English) Zbl 1093.03002 Lecture Notes in Logic 23. Wellesley, MA: A K Peters; Urbana, IL: Association for Symbolic Logic (ASL) (ISBN 1-56881-275-2/hbk; 1-56881-276-0/pbk). xvii, 230 p. (2005). Reviewer: Branislav Boričić (Beograd) MSC: 03-02 03A05 03B15 03B70 03F05 03F55 × Cite Format Result Cite Review PDF
Carlström, Jesper Interpreting descriptions in intensional type theory. (English) Zbl 1089.03051 J. Symb. Log. 70, No. 2, 488-514 (2005). MSC: 03F35 03F50 03F55 × Cite Format Result Cite Review PDF Full Text: DOI Link
Dowek, Gilles; Jiang, Ying Eigenvariables, bracketing and the decidability of positive minimal intuitionistic logic. (English) Zbl 1264.03039 Dahn, Ingo (ed.) et al., Proceedings of the workshop on mathematics, logic and computation (satellite event of ICALP 2003), Valencia, Spain, June 12–14, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 85, No. 7, 17-29 (2003). MSC: 03B25 03B15 03B20 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Setzer, Anton Proof theory of Martin-Löf type theory. An overview. (English) Zbl 1127.03320 Math. Sci. Hum., Math. Soc. Sci. 165, 59-99 (2003). MSC: 03F35 03B15 03F55 × Cite Format Result Cite Review PDF
Valentini, Silvio A cartesian closed category in Martin-Löf’s intuitionistic type theory. (English) Zbl 1018.68078 Theor. Comput. Sci. 290, No. 1, 189-219 (2003). MSC: 68T27 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Fairtlough, Matt; Mendler, Michael On the logical content of computational type theory: A solution to Curry’s problem. (English) Zbl 1054.03027 Callaghan, Paul (ed.) et al., Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8–12, 2000. Selected papers. Berlin: Springer (ISBN 3-540-43287-6). Lect. Notes Comput. Sci. 2277, 63-78 (2002). MSC: 03B70 03B45 03B20 03F35 × Cite Format Result Cite Review PDF Full Text: Link
Aczel, Peter; Gambino, Nicola Collection principles in dependent type theory. (English) Zbl 1054.03036 Callaghan, Paul (ed.) et al., Types for proofs and programs. International workshop, TYPES 2000, Durham, GB, December 8–12, 2000. Selected papers. Berlin: Springer (ISBN 3-540-43287-6). Lect. Notes Comput. Sci. 2277, 1-23 (2002). MSC: 03F35 03F55 03E70 × Cite Format Result Cite Review PDF Full Text: Link
López-Escobar, E. G. K.; Miraglia, Francisco Definitions: the primitive concept of logics, or the Leśniewski-Tarski legacy. (English) Zbl 1001.03009 Diss. Math. 401, 184 p. (2002). Reviewer: Jānis Cīrulis (Riga) MSC: 03B15 03B20 03G25 03F50 03-03 01A60 06D20 × Cite Format Result Cite Review PDF Full Text: DOI
Schürmann, Carsten A type-theoretic approach to induction with higher-order encodings. (English) Zbl 1275.03078 Nieuwenhuis, Robert (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 8th international conference, LPAR 2001, Havana, Cuba, December 3–7, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42957-3/pbk). Lecture Notes in Computer Science 2250. Lecture Notes in Artificial Intelligence, 266-281 (2001). MSC: 03B20 03B15 03B70 68N30 × Cite Format Result Cite Review PDF
McLarty, Colin Semantics for first and higher order realizability. (English) Zbl 1031.03082 Anderson, C. Anthony (ed.) et al., Logic, meaning and computation. Essays in memory of Alonzo Church. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 305, 353-363 (2001). MSC: 03G30 03B15 03F30 × Cite Format Result Cite Review PDF
Curi, Giovanni The points of (locally) compact regular formal topologies. (English) Zbl 1011.54001 Schuster, Peter (ed.) et al., Reuniting the antipodes–constructive and nonstandard views of the continuum. Symposium proceedings, San Servolo, Venice, Italy, May 16-22, 1999. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 306, 39-54 (2001). MSC: 54A05 03F55 06D22 03B15 × Cite Format Result Cite Review PDF
Maietti, Maria Emilia; de Paiva, Valeria; Ritter, Eike Categorical models for intuitionistic and linear type theory. (English) Zbl 0955.03069 Tiuryn, Jerzy (ed.), Foundations of software science and computation structures. 3rd international conference, FOSSACS 2000. Held as part of the joint European conferences on theory and practice of software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1784, 223-237 (2000). MSC: 03G30 03F52 03B70 68Q55 18C50 03B20 03F35 18D15 × Cite Format Result Cite Review PDF
Dybjer, Peter A general formulation of simultaneous inductive-recursive definitions in type theory. (English) Zbl 0960.03048 J. Symb. Log. 65, No. 2, 525-549 (2000). MSC: 03F35 03D70 × Cite Format Result Cite Review PDF Full Text: DOI
Troelstra, A. S.; Schwichtenberg, H. Basic proof theory. 2nd ed. (English) Zbl 0957.03053 Cambridge Tracts in Theoretical Computer Science. 43. Cambridge: Cambridge University Press. xii, 417 p. (2000). Reviewer: Anton Setzer (Uppsala) MSC: 03F03 03-02 03-01 03F52 68N17 03F05 03B40 03G30 03B45 03F30 03F35 03B70 × Cite Format Result Cite Review PDF
Bunder, M. W. Proof finding algorithms for implicational logics. (English) Zbl 0972.03022 Theor. Comput. Sci. 232, No. 1-2, 165-186 (2000). Reviewer: G.Mints (Stanford) MSC: 03B47 03B40 03B15 03B20 03B35 × Cite Format Result Cite Review PDF Full Text: DOI
Le Bars, Jean-Marie Counterexamples of the 0-1 law for fragments of existential second-order logic: An overview. (English) Zbl 0958.03022 Bull. Symb. Log. 6, No. 1, 67-82 (2000). Reviewer: Ivor Grattan-Guinness (Bengeo/Herts) MSC: 03C13 03B20 03-02 03B15 × Cite Format Result Cite Review PDF Full Text: DOI Link
Rathjen, Michael The superjump in Martin-Löf type theory. (English) Zbl 0944.03057 Buss, Samuel R. (ed.) et al., Logic colloquium ’98. Proceedings of the annual European summer meeting of the Association for Symbolic Logic, Prague, Czech Republic, August 9-15, 1998. Natick, MA: A K Peters, Ltd. Lect. Notes Log. 13, 363-386 (2000). MSC: 03F50 03F35 03E70 × Cite Format Result Cite Review PDF
Geuvers, Herman; Barendsen, Erik Some logical and syntactical observations concerning the first-order dependent type system \(\lambda P\). (English) Zbl 0939.03016 Math. Struct. Comput. Sci. 9, No. 4, 335-359 (1999). Reviewer: M.W.Bunder (Wollongong) MSC: 03B40 03B20 03B15 × Cite Format Result Cite Review PDF Full Text: DOI
Rosen, Eric An existential fragment of second order logic. (English) Zbl 0936.03009 Arch. Math. Logic 38, No. 4-5, 217-234 (1999). Reviewer: Jānis Cīrulis (Riga) MSC: 03B15 03B20 03B25 03C13 03C85 68Q19 × Cite Format Result Cite Review PDF Full Text: DOI
Barendregt, Henk Problems in type theory. (English) Zbl 0933.03077 Berger, Ulrich (ed.) et al., Computational logic. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 29–August 10, 1997. Berlin: Springer. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 165, 99-111 (1999). MSC: 03F35 03B40 × Cite Format Result Cite Review PDF
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 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF
Sambin, Giovanni; Valentini, Silvio Building up a toolbox for Martin-Löf’s type theory: Subset theory. (English) Zbl 0930.03091 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, 221-244 (1998). MSC: 03F35 03F55 × Cite Format Result Cite Review PDF
Martin-Löf, Per An intuitionistic theory of types. (English) Zbl 0931.03070 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, 127-172 (1998). Reviewer: Victor N.Krivtsov (Moskva) MSC: 03F50 03F35 03F55 03F05 03B20 × Cite Format Result Cite Review PDF
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 × Cite Format Result Cite Review PDF Full Text: DOI
Bourdeau, Michel Intuitionistic type theory: Semantics of proofs and theory of constructions. (La théorie intuitionniste des types: Sémantique des preuves et théorie des constructions.) (French) Zbl 0923.03067 Dialogue 36, No. 2, 323-339 (1997). MSC: 03F50 03F35 03F03 03F55 × Cite Format Result Cite Review PDF Full Text: DOI
Hofmann, Martin An application of category-theoretic semantics to the characterisation of complexity classes using higher-order function algebras. (English) Zbl 0931.03058 Bull. Symb. Log. 3, No. 4, 469-486 (1997). MSC: 03D15 68Q15 03B40 18F20 03G30 03D65 × Cite Format Result Cite Review PDF Full Text: DOI Link Link
Parigot, Michel Proofs of strong normalisation for second order classical natural deduction. (English) Zbl 0941.03063 J. Symb. Log. 62, No. 4, 1461-1479 (1997). MSC: 03F05 03B15 × Cite Format Result Cite Review PDF Full Text: DOI
Hindley, J. Roger Basic simple type theory. (English) Zbl 0906.03012 Cambridge Tracts in Theoretical Computer Science. 42. Cambridge: Cambridge Univ. Press. xi, 186 p. (1997). Reviewer: K.Shvachko (Pereslavl’-Zalesskij) MSC: 03B40 03B70 03B20 68-01 03-01 03B15 68N15 × Cite Format Result Cite Review PDF
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 × Cite Format Result Cite Review PDF Full Text: DOI
Berger, Ulrich Density theorems for the domains-with-totality semantics of dependent types. (English) Zbl 0865.03043 Adámek, J. (ed.) et al., Workshop domains II, Braunschweig, Germany, May 3–5, 1996. Braunschweig: TU Braunschweig, Inf.-Ber., Tech. Univ. Braunschweig. 96-04, 1-35 (1996). Reviewer: U.Berger (München) MSC: 03F10 68Q55 03F35 03F55 × Cite Format Result Cite Review PDF
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 × Cite Format Result Cite Review PDF Full Text: DOI
Joinet, Jean-Baptiste; Schellinx, Harold; Tortora de Falco, Lorenzo Strong normalization for all-style \(\mathbf{LK}^\mathrm{tq}\). (English) Zbl 1415.03056 Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 226-243 (1996). MSC: 03F05 03B10 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Nerode, Anil An appreciation of Kreisel. (English) Zbl 0895.01006 Odifreddi, Piergiorgio (ed.), Kreiseliana: about and around Georg Kreisel. Wellesley, MA: A K Peters. 81-88 (1996). Reviewer: V.Peckhaus (Erlangen) MSC: 01A70 03-03 × Cite Format Result Cite Review PDF
Serebriannikov, O. F. An extension of Gentzen’s analysis of logical deduction to second-order logic. (English) Zbl 0896.03047 Bystrov, Peter I. (ed.) et al., Philosophical logic and logical philosophy. Essays in honour of Vladimir A. Smirnov. Dordrecht: Kluwer Academic Publishers. Synth. Libr. 257, 223-226 (1996). MSC: 03F05 03B15 × Cite Format Result Cite Review PDF
Krivine, Jean-Louis A formal and intuitionistic proof of the completeness theorem of classical logic. (Une preuve formelle et intuitionniste du théorème de complétude de la logique classique.) (French) Zbl 0872.03004 Bull. Symb. Log. 2, No. 4, 405-421 (1996). Reviewer: J.-L.Krivine (Paris) MSC: 03B10 68Q60 03B70 03B40 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI Link
Danos, Vincent; Joinet, Jean-Baptiste; Schellinx, Harold \({\mathbf {LKQ}}\) and \({\mathbf {LKT}}\): Sequent calculi for second order logic based upon dual linear decompositions of classical implication. (English) Zbl 0829.03031 Girard, Jean-Yves (ed.) et al., Advances in linear logic. Based on the linear logic workshop held June 14-18, 1993 at the Mathematical Sciences Institute, Cornell University, Ithaca, New York, USA. Cambridge: Cambridge University Press. Lond. Math. Soc. Lect. Note Ser. 222, 211-224 (1995). Reviewer: G.Mints (Stanford) MSC: 03F05 03B20 03B15 × Cite Format Result Cite Review PDF
Yi, Bo; Xu, Jiafu Analogical type theory. (English) Zbl 0845.03011 J. Symb. Comput. 19, No. 1-3, 3-24 (1995). Reviewer: J.Šefránek (Bratislava) MSC: 03B80 68T27 03F35 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI
Dybjer, Peter Inductive families. (English) Zbl 0808.03044 Formal Asp. Comput. 6, No. 4, 440-465 (1994). MSC: 03F35 03B70 × Cite Format Result Cite Review PDF Full Text: DOI
Pentus, Mati The conjoinability relation in Lambek calculus and linear logic. (English) Zbl 0805.03004 J. Logic Lang. Inf. 3, No. 2, 121-140 (1994). MSC: 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
Połacik, Tomasz Second order propositional operators over Cantor space. (English) Zbl 0790.03005 Stud. Log. 53, No. 1, 93-105 (1994). MSC: 03B15 03B20 × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF
Połacik, Tomasz Operators defined by propositional quantification and their interpretation over Cantor space. (English) Zbl 0806.03008 Rep. Math. Logic 27, 67-79 (1993). MSC: 03B15 03B20 × Cite Format Result Cite Review PDF
Bell, John L. Hilbert’s \(\varepsilon\)-operator in intuitionistic type theories. (English) Zbl 0802.03005 Math. Log. Q. 39, No. 3, 323-337 (1993). MSC: 03B15 03B20 03G30 × Cite Format Result Cite Review PDF Full Text: DOI
Dzierzgowski, Daniel Typical ambiguity and elementary equivalence. (English) Zbl 0799.03004 Math. Log. Q. 39, No. 4, 436-446 (1993). Reviewer: D.Dzierzgowski (Louvain-la-Neuve) MSC: 03B15 03F50 03F55 × Cite Format Result Cite Review PDF Full Text: DOI
Takayama, Yukihide \(QPC_ 2\): A constructive calculus with parameterized specifications. (English) Zbl 0804.68085 J. Symb. Comput. 15, No. 5-6, 641-672 (1993). MSC: 68Q60 68Q65 68N17 03F35 03F50 68T15 × Cite Format Result Cite Review PDF Full Text: DOI
Sambin, Giovanni; Valentini, Silvio Building up a tool-box for Martin-Löf’s type theory. (English) Zbl 0794.03084 Gottlob, Georg (ed.) et al., Computational logic and proof theory. 3rd Kurt Gödel Colloquium, KGC ’93, Brno, Czech Republic, August 24-27, 1993. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 713, 69-70 (1993). MSC: 03F35 × Cite Format Result Cite Review PDF
Wansing, Heinrich The logic of information structures. (English) Zbl 0788.03001 Lecture Notes in Computer Science 681. Lecture Notes in Artificial Intelligence. Berlin: Springer-Verlag. IX, 163 p. DM 46.00 /sc (1993). Reviewer: H.Guggenheimer (West Hempstead) MSC: 03-02 68-02 68T27 03B20 03F05 03B47 03B40 03B15 × Cite Format Result Cite Review PDF Full Text: DOI
Tonino, Hans; Fujita, Ken-etsu On the adequacy of representing higher order intuitionistic logic as a pure type system. (English) Zbl 0763.03007 Ann. Pure Appl. Logic 57, No. 3, 251-276 (1992). MSC: 03B15 03B20 03B40 × Cite Format Result Cite Review PDF 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 × Cite Format Result Cite Review PDF Full Text: DOI
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 × Cite Format Result Cite Review PDF Full Text: DOI