 On the other hand, once we set apart the ideological inspiration of logicism, we might believe that the development of logic and set theory in the 20th century has fully sterilized paradoxes, and that contradictions in logical systems are phenomena of the years of foundational crisis only. But this is not true: paradoxes have been discovered in logical systems related to computer science. For instance, half a century ago, Girard showed that a constructive theory of types, due to Per Martin-Löf 1971, and based on the Curry-Howard correspondence, is inconsistent with the existence of a type of all types; the contradiction follows by means of a type-theoretic reconstruction of an argument related to the Burali-Forti antinomy and the Mirimanoff paradox of grounded sets. Later, Coquand 1986 proved that certain extensions of the calculus C of constructions are inconsistent. Very roughly, C is a higher order impredicative type theory, extending Girard’s system F, a powerful second-order typed lambda calculus with abstraction on types which is suitable for representing proofs of impredicative intuitionistic second-order logic. Coquand 1994 offered a new paradox affecting type theory, which refines Reynold’s result that there is no classical set-theoretic model of polymorphism (read: Girard’s system F, see the entries  Type Theory,  set theory: constructive and intuitionistic ZF). On the other side, a general type-free development of the theory of constructions as a foundation for constructive provability in logic and mathematics was originally proposed by Kreisel and Goodman, but it turned out to be affected by an antinomy, which has been recently reconsidered by Dean and Kurokawa 2016.