科研之友
微信
新浪微博
Facebook
分享链接
摘要
We present a version of arithmetic in all finite types based on a systematic use of an internally definable notion of observational equivalence for dealing with equalities at higher types. For this system both intensional and extensional models are possible, the deduction theorem holds and the soundness of the Dialectica interpretation is provable inside the system itself.
- 出版日期2017-11
