tag:blogger.com,1999:blog-827419514217130218.post6032546845805008908..comments2023-12-11T04:47:19.677-05:00Comments on Request for Logic: That curious termination argumentRobhttp://www.blogger.com/profile/05106663398227635415noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-827419514217130218.post-23632947091392371032010-11-11T11:27:53.402-05:002010-11-11T11:27:53.402-05:00Simple General Recursion in Type Theory (Bove, 200...Simple General Recursion in Type Theory (Bove, 2000, Nordic Journal of Computing) is the earliest cite I can findDan Licatahttps://www.blogger.com/profile/05419342217317164459noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-55418563432657673122010-11-04T08:46:24.171-04:002010-11-04T08:46:24.171-04:00Thanks - is the right citation for that "Mode...Thanks - is the right citation for that "Modelling general recursion in type theory," MSCS 2005?Robhttps://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-827419514217130218.post-21063497874238466472010-11-02T09:53:31.143-04:002010-11-02T09:53:31.143-04:00BTW, what you're describing---defining a predi...BTW, what you're describing---defining a predicate that gives an inductive definition of the domain/recursive calls of the function, and separately proving that everything satisfies that predicate---is often called the "Bove-and-Capretta" methodDan Licatahttps://www.blogger.com/profile/05419342217317164459noreply@blogger.com