JavaScript is disabled for your browser. Some features of this site may not work without it.
The Computational Behaviour of Girard's Paradox

Author
Howe, Douglas J.
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 programing language with dependent types. Central to their argument is the claim that by following the proof of Girard's paradox it is possible to construct in their calculus $\lambda^{\tau \tau}$ 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 Girard'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.
Date Issued
1987-03Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-820
Type
technical report