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

**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} }