Non-trivial power types can't be subtypes of polymorphic types

LDR 01105nam a2200301Ia 4500
001 006251053
003 MiAaHDL
005 20090407000000.0
006 m d
007 cr bn ---auaua
008 021205s1989 enk tb 000 0 eng d
035 ‡asdr-nrlfGLAD184960796-B
035 ‡ab11733974
040 ‡aPMC ‡cPMC
090 ‡a QA9.5 ‡b.P58 1989
035 ‡a(OCoLC)20696163
100 1 ‡aPitts, A. M. ‡q(Andrew M.)
245 1 0 ‡aNon-trivial power types can't be subtypes of polymorphic types / ‡cby Andrew M. Pitts.
260 ‡aCambridge [Cambridgeshire] : ‡bUniversity of Cambridge, Computer Laboratory, ‡c1989.
300 ‡a12 p. ; ‡c21 cm.
490 0 ‡aTechnical report / University of Cambridge, Computer Laboratory ; ‡vno. 159
500 ‡a"January 1989."
504 ‡aIncludes bibliographical references.
538 ‡aMode of access: Internet.
650 0 ‡aType theory.
650 0 ‡aLambda calculus.
CID ‡a006251053
DAT 0 ‡a20080319111814.0 ‡b20090407000000.0
DAT 1 ‡a20120815184702.0 ‡b2023-05-20T18:11:19Z
DAT 2 ‡a2023-05-20T17:30:01Z
CAT ‡aSDR-NRLF ‡dLOCAL - GLADIS ‡lloader.pl-001-001
FMT ‡aBK
HOL ‡0sdr-nrlfGLAD184960796-B ‡auc1 ‡bSDR ‡cNRLF ‡puc1.b4502335 ‡sUC ‡1GLAD184960796-B
974 ‡bUC ‡cNRLF ‡d20230520 ‡sgoogle ‡uuc1.b4502335 ‡y1989 ‡ric ‡qbib ‡tnon-US bib date1 >= 1930