Very nice paper. Thanks Umair and Freek for the correction and link. On Wed, 20 Feb 2019 21:08 Umair Siddique <umair....@gmail.com wrote:
> > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101&rep=rep1&type=pdf > > http://www.gilith.com/talks/tphols2001-subtypes.pdf > > > - Umair > > On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk <fr...@cs.ru.nl> wrote: > >> Hi Ramana, >> >> >I think this is exactly what is impossible to do in HOL: >> >it is a logic of total functions. >> >> I think that in PVS you _can_ do something like that, right? >> Using the predicate subtypes. Even though PVS _also_ >> only has total functions. >> >> And I _think_ there was a paper once about how to mimic >> predicate subtypes in HOL. Does anyone remember the >> reference? >> >> Freek >> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
