Paper: The Computational Behaviour of Girard's Paradox (at LICS 1987)

Authors: Douglas J. Howe

Abstract

In their paper "Type" Is Not a Type, Meyer and Reinhold argued that serious pathologies can result when a type of all types is added to a programming language with dependent types. Central to their argument is the claim that by following the proof of Girad's paradox it is possible to construct in their calculus λ^ττ a term having a fixed-point property. Because of the tremendous amount of formal detail involved, they were unable to establish this claim. We have made use of the Nuprl proof development system in constructing a formal proof of Girad's paradox and analysing the resulting term. We can show that the term does not have the desired fixed-point property, but does have a weaker form of it that is sufficient to establish some of the results of Meyer and Reinhold. We believe that the method used here is in itself of some interest, representing a new kind of application of a computer to a problem in symbolic logic.

BibTeX

  @InProceedings{Howe-TheComputationalBeh,
    author = 	 {Douglas J. Howe},
    title = 	 {The Computational Behaviour of Girard's Paradox},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {205--214},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }