[TYPES] Conversion elimination lemma for Pure Type Systems?

[Randy Pollack]

There has been some thinking about where conversion is necessary in
PTS derivations.  I suggest you look at:

@article{Jutting93,
  author =	 "L.S. van Benthem Jutting",
  title =	 "Typing in {P}ure {T}ype {S}ystems",
  journal =	 ic,
  year =	 1993,
  pages =	 "30--41",
  volume =	 "105",
  number =	 "1",
  month =	 jul
}
@InProceedings{JuttingMcKinnaPollack93,
  author =      "L.S. van Benthem Jutting and J. McKinna and
                 R. Pollack",
  title =       "Checking Algorithms for {P}ure {T}ype {S}ystems",
  booktitle =   "TYPES'93: Workshop on Types for Proofs and Programs,
                 Selected Papers",
  editor =      "Barendregt and Nipkow",
  pages =       "19--61",
  volume =       806,
  series =       lncs,
  publisher =    springer,
  year =         1994
}

Best,
Randy Pollack


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.