5 found
  1.  24
    Kripke-style models for typed lambda calculus.John C. Mitchell & Eugenio Moggi - 1991 - Annals of Pure and Applied Logic 51 (1-2):99-124.
    Mitchell, J.C. and E. Moggi, Kripke-style models for typed lambda calculus, Annals of Pure and Applied Logic 51 99–124. The semantics of typed lambda calculus is usually described using Henkin models, consisting of functions over some collection of sets, or concrete cartesian closed categories, which are essentially equivalent. We describe a more general class of Kripke-style models. In categorical terms, our Kripke lambda models are cartesian closed subcategories of the presheaves over a poset. To those familiar with Kripke models of (...)
    Direct download (5 more)  
    Export citation  
    Bookmark   3 citations  
  2.  28
    Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's type theory. An introduction. The international series of monographs on computer science, no. 7. Clarendon Press, Oxford University Press, Oxford and New York1990, x + 221 pp. [REVIEW]John C. Mitchell - 1992 - Journal of Symbolic Logic 57 (1):272-274.
    Direct download (4 more)  
    Export citation  
  3.  20
    On Play by Means of Computing Machines .A Theory of Higher Order Probabilities.Knowledge and Efficient Computation.Realizability Semantics for Error-Tolerant Logics. [REVIEW]William J. Rapaport, Nimrod Megiddo, Avi Wigderson, Haim Gaifman, Silvio Micali, John C. Mitchell & Michael J. O'Donnell - 1988 - Journal of Symbolic Logic 53 (2):669.
  4.  17
    Linear logic proof games and optimization.Patrick D. Lincoln, John C. Mitchell & Andre Scedrov - 1996 - Bulletin of Symbolic Logic 2 (3):322-338.
    § 1. Introduction. Perhaps the most surprising recent development in complexity theory is the discovery that the class NP can be characterized using a form of randomized proof checker that only examines a constant number of bits of the “proof” that a string is in a language [6, 5, 31, 3, 4]. More specifically, writing ∣x∣ for the length of a string x, a language L in the class NP of languages recognizable in Nondeterministic polynomial time is traditionally given by (...)
    Direct download (11 more)  
    Export citation  
  5.  34
    2001 annual meeting of the association for symbolic logic.Joan Feigenbaum, Haim Gaifman, Jean-Yves Girard, C. Ward Henson, Denis Hirschfeldt, Carl G. Jockusch Jr, Saul Kripke, Salma Kuhlmann, John C. Mitchell & Ernest Schimmerling - 2001 - Bulletin of Symbolic Logic 7 (3):420-435.