{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T22:16:00Z","timestamp":1649196960221},"reference-count":72,"publisher":"Elsevier","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1016\/b978-0-444-51621-3.50011-6","type":"book-chapter","created":{"date-parts":[[2012,4,21]],"date-time":"2012-04-21T15:46:39Z","timestamp":1335023199000},"page":"801-845","source":"Crossref","is-referenced-by-count":0,"title":["Russell's Orders in Kripke's Theory of Truth and Computational Type Theory"],"prefix":"10.1016","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Twan","family":"Laan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Constable","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0010","series-title":"Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures","year":"1992"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0015","series-title":"The semantics of reflected proof. In LICS90","first-page":"95","author":"Allen","year":"1990"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0020","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1016\/j.jal.2005.10.005","article-title":"Innovations in computational type theory using Nuprl","volume":"4","author":"Allen","year":"2006","journal-title":"Journal of Applied Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0025","series-title":"A non-type-theoretic definition of Martin-Lof's types","first-page":"215","author":"Allen","year":"1987"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0030","series-title":"Lambda calculi with types","first-page":"117","author":"Barendregt","year":"1992"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0035","series-title":"Theoretical Aspects of Computer Software","first-page":"475","article-title":"Some normalization properties of Martin- Lof's type theory, and applications","author":"Basin","year":"1991"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0040","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1145\/2363.2528","article-title":"Proofs as programs","volume":"7","author":"Bates","year":"1985","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0045","series-title":"Foundations of Constructive Mathematics","author":"Beeson","year":"1985"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0050","series-title":"Texts in Theoretical Computer Science","article-title":"Interactive Theorem Proving and Program Development; Coq'Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0055","first-page":"29","article-title":"Formal foundations of computer security","volume":"14","author":"Bickford","year":"2008","journal-title":"Formal Logical Methods for System Security and Correctness"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0060","unstructured":"M. Bickford. Automated proof of authentication protocols in a logic of events. VERIFY-2010, 6th International Workshop, Edinburgh, 2010."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0065","series-title":"Foundations of Constructive Analysis","author":"Bishop","year":"1967"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0070","series-title":"Symposium on Constructivity in Computer Science","first-page":"165","author":"Chirimar","year":"1991"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0075","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0080","series-title":"The Calculi of Lambda Conversion","author":"Church","year":"1941"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0085","doi-asserted-by":"crossref","first-page":"747","DOI":"10.2307\/2272393","article-title":"Comparison of Russell's resolution of the semantic antinomies with that of Tarski","volume":"41","author":"Church","year":"1976","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0090","series-title":"Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman","first-page":"21","article-title":"Computational complexity and induction for partial computable functions in type theory","author":"Constable","year":"2001"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0095","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1016\/0304-3975(93)90085-8","article-title":"Computational foundations of basic recursive function theory","volume":"121","author":"Constable","year":"1993","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0100","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0105","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Information and Computation"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0110","series-title":"Combinatory Logic I","author":"Curry","year":"1958"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0115","series-title":"Combinatory Logic II","author":"Curry","year":"1972"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0120","series-title":"Oxford logic guides 39","article-title":"Elements of Intuitionism","author":"Dummett","year":"2000"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0125","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2269764","article-title":"Systems of predicative analysis","volume":"29","author":"Feferman","year":"1964","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0130","doi-asserted-by":"crossref","first-page":"75","DOI":"10.2307\/2274093","article-title":"Toward useful type-free theories I","volume":"49","author":"Feferman","year":"1984","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0135","volume":"volume I","author":"Frege","year":"1962"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0140","series-title":"Introductionto HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0145","series-title":"Edinburgh LCF: a mechanized logic of computation","author":"Gordon","year":"1979"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0150","unstructured":"D. Gries, ed. Proceedings of the 2ndIEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1987."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0155","series-title":"LICS88","first-page":"372","article-title":"Notational definition - a formal account","author":"Griffin","year":"1988"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0160","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0304-3975(90)90108-T","article-title":"Type checking with universes","volume":"89","author":"Harper","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0165","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/0747-7171(92)90026-Z","article-title":"Constructing type systems over an operational semantics","volume":"14","author":"Harper","year":"1992","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0170","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic","first-page":"1879","year":"1967"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0175","volume":"volume 1","year":"1975"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0180","series-title":"TPHOLs","first-page":"287","article-title":"Metaprl - a modular logical environment","author":"Hickey","year":"2003"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0185","series-title":"Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen","article-title":"Grundz\u00fcge der Theoretischen Logik","author":"Hilbert","year":"1928"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0190","series-title":"The computational behaviour of Girard's paradox","first-page":"205","author":"Howe","year":"1987"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0195","unstructured":"D. J. Howe. Equality in lazy computation systems. In LICS89, pp. 198203, Asilomar Conference Center, Pacific Grove, California, June 1989. IEEE Computer Society Press."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0200","series-title":"Algebraic Methodology and Software Technology","first-page":"85","article-title":"Semantic foundations for embedding HOL in Nuprl","author":"Howe","year":"1996"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0205","series-title":"Theorem Proving in HigherOrder Logics","article-title":"A type annotation scheme for Nuprl","author":"Howe","year":"1998"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0210","series-title":"The Nuprl Proof Development System, Version 4-1 Reference Manual and User's Guide","author":"Jackson","year":"1994"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0215","series-title":"Enhancing the Nuprl Proo f Development System and Applying it to Computational Abstract Algebra","author":"Jackson","year":"1995"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0220","series-title":"STACS '87","first-page":"22","article-title":"Natural semantics","author":"Kahn","year":"1987"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0225","first-page":"195","article-title":"A reflection on Russell's ramified types and Kripke's hierarchy of truths","volume":"4","author":"Kamareddine","year":"1996","journal-title":"Journal of the Interest Group in Pure and Applied Logic"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0230","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1023\/A:1011286100450","article-title":"A correspondence between Martin-Lof type theory, the ramified theory of types and pure type systems","volume":"10","author":"Kamareddine","year":"2001","journal-title":"Journal of Logic, Language and Information"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0235","series-title":"A Modern Perspective on Type Theory","author":"Kamareddine","year":"2004"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0240","series-title":"Dependent intersection: A new way of defining records in type theory","first-page":"86","author":"Kopylov","year":"2003"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0245","series-title":"The Nuprl Proof Development System, Version 5.1 Reference Manual and User's Guide","author":"Kreitz","year":"2003"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0250","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1017\/S0956796803004854","article-title":"Building reliable, high-performance networks with the nuprl proof development system","volume":"14","author":"Kreitz","year":"2004","journal-title":"Journal of Functional Programming"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0255","doi-asserted-by":"crossref","first-page":"690","DOI":"10.2307\/2024634","article-title":"Outline of a theory of truth","volume":"72","author":"Kripke","year":"1975","journal-title":"Journal of Philosophy"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0260","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/BF00370835","article-title":"A modern elaboration of the Ramified Theory of Types","volume":"57","author":"Laan","year":"1996","journal-title":"Studia Logica"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0265","series-title":"The Evolution of Type Theory in Logic and Mathematics","author":"Laan","year":"1997"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0270","series-title":"Building reliable, high-performance communication systems from components","first-page":"80","author":"Liu","year":"1999"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0275","series-title":"An intuitionistic theory of types: predicative part","first-page":"73","author":"Martin-Lof","year":"1975"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0280","series-title":"Proceedings of the Sixth International Congress for Logic, Methodology, and Philosophy of Science","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0285","series-title":"Studies in Proof Theory. Bibliopolis","article-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0290","series-title":"Recursive types and type constraints in second-order Lambda calculus","first-page":"30","author":"Mendler","year":"1987"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0295","series-title":"Approaches to Natural Language","article-title":"The proper treatment of quantification in ordinary English","author":"Montague","year":"1973"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0300","series-title":"LICS91","first-page":"96","article-title":"An evaluation semantics for classical proofs","author":"Murthy","year":"1991"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0305","series-title":"Programming in Martin- Lof's Type Theory","author":"Nordstrom","year":"1990"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0310","series-title":"A structural approach to operational semantics","author":"Plotkin","year":"1981"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0315","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1112\/plms\/s2-25.1.338","article-title":"The foundations of mathematics","volume":"25","author":"Ramsey","year":"1926","journal-title":"Proceedings of the London Mathematical Society"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0320","series-title":"Type-theoretical grammar","author":"Ranta","year":"1994"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0325","series-title":"The Principles of Mathematics","author":"Russell","year":"1903"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0330","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","article-title":"Mathematical logic as based on the theory of types","volume":"30","author":"Russell","year":"1908","journal-title":"American Journal of Mathematics"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0335","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM J. Comput."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0340","first-page":"261","article-title":"Der Wahrheitsbegriff in den formalisierten Sprachen","volume":"1","author":"Tarski","year":"1936","journal-title":"Studia Philosophica"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0345","series-title":"Een nadere bewijstheoretische analyse van GSTT's","author":"Terlouw","year":"1989"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0350","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual - Version V8.0, April 2004."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0355","doi-asserted-by":"crossref","unstructured":"H. Weyl. Das Kontinuum. Veit, Leipzig, 1918. German; also in: Das Kontinuum und andere Monographien, Chelsea Publishing Company, New York, 1960.","DOI":"10.1515\/9783112451144"},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0360","unstructured":"A. N. Whitehead and B. Russell. Principia Mathematica, volumes I,II,III. Cambridge University Press, 1910,1927. All references are to the first volume, unless otherwise stated."},{"key":"10.1016\/B978-0-444-51621-3.50011-6_bb0365","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF01449999","article-title":"Untersuchungen \u00f6ber die Grundlagen der Mengenlehre","volume":"65","author":"Zermelo","year":"1908","journal-title":"Mathematische Annalen"}],"container-title":["Handbook of the History of Logic","Sets and Extensions in the Twentieth Century"],"original-title":[],"deposited":{"date-parts":[[2022,1,13]],"date-time":"2022-01-13T15:01:49Z","timestamp":1642086109000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780444516213500116"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"references-count":72,"URL":"https:\/\/doi.org\/10.1016\/b978-0-444-51621-3.50011-6","relation":{},"ISSN":["1874-5857"],"issn-type":[{"value":"1874-5857","type":"print"}],"subject":[],"published":{"date-parts":[[2012]]}}}