8 found
  1.  28
    The realm of primitive recursion.Harold Simmons - 1988 - Archive for Mathematical Logic 27 (2):177-188.
  2.  43
    Derivation and computation: taking the Curry-Howard correspondence seriously.Harold Simmons - 2000 - New York: Cambridge University Press.
    Mathematics is about proofs, that is the derivation of correct statements; and calculations, that is the production of results according to well-defined sets of rules. The two notions are intimately related. Proofs can involve calculations, and the algorithm underlying a calculation should be proved correct. The aim of the author is to explore this relationship. The book itself forms an introduction to simple type theory. Starting from the familiar propositional calculus the author develops the central idea of an applied lambda-calculus. (...)
    Direct download (2 more)  
    Export citation  
    Bookmark   2 citations  
  3. Large discrete parts of the e-tree.Harold Simmons - 1988 - Journal of Symbolic Logic 53 (3):980-984.
  4.  30
    Proof theory: a selection of papers from the Leeds Proof Theory Programme, 1990.Peter Aczel, Harold Simmons & Stanley S. Wainer (eds.) - 1992 - New York: Cambridge University Press.
    This work is derived from the SERC "Logic for IT" Summer School Conference on Proof Theory held at Leeds University. The contributions come from acknowledged experts and comprise expository and research articles which form an invaluable introduction to proof theory aimed at both mathematicians and computer scientists.
    Direct download  
    Export citation  
  5.  7
    A coverage construction of the reals and the irrationals.Harold Simmons - 2007 - Annals of Pure and Applied Logic 145 (2):176-203.
    I modify the standard coverage construction of the reals to obtain the irrationals. However, this causes a jump in ordinal complexity from ω+1 to Ω.
    Direct download (4 more)  
    Export citation  
  6.  27
    A comparison of two systems of ordinal notations.Harold Simmons - 2004 - Archive for Mathematical Logic 43 (1):65-83.
    The standard method of generating countable ordinals from uncountable ordinals can be replaced by a use of fixed point extractors available in the term calculus of Howard’s system. This gives a notion of the intrinsic complexity of an ordinal analogous to the intrinsic complexity of a function described in Gödel’s T.
    Direct download (3 more)  
    Export citation  
    Bookmark   1 citation  
  7.  26
    Fruitful and helpful ordinal functions.Harold Simmons - 2008 - Archive for Mathematical Logic 47 (7-8):677-709.
    In Simmons (Arch Math Logic 43:65–83, 2004), I described a method of producing ordinal notations ‘from below’ (for countable ordinals up to the Howard ordinal) and compared that method with the current popular ‘from above’ method which uses a collapsing function from uncountable ordinals. This ‘from below’ method employs a slight generalization of the normal function—the fruitful functions—and what seems to be a new class of functions—the helpful functions—which exist at all levels of the function space hierarchy over ordinals. Unfortunately, (...)
    Direct download (3 more)  
    Export citation  
  8.  76
    Tiering as a recursion technique.Harold Simmons - 2005 - Bulletin of Symbolic Logic 11 (3):321-350.
    I survey the syntactic technique of tiering which can be used to restrict the power of a recursion scheme. I show how various results can be obtained entirely proof theoretically without the use of a model of computation.
    Direct download (12 more)  
    Export citation