[Prev][Next][Index][Thread]

Re: Non-dependant PTS's




[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

> the same idea was used by Furio Honsell about the same time to prove
> SN for the Edinburgh Logical Framework.

The idea was attributed to Plotkin in the JACM paper "A Framework for
Defining Logics", if I recall correctly.

 - David.