虚弱 发表于 2025-3-23 11:35:37

Program Testing and the Meaning Explanations of Intuitionistic Type Theoryes. In particular we propose that testing for impredicative type theory should be based on the evaluation of open expressions. This is in contrast to our testing semantics for Martin-Löf’s predicative intuitionistic type theory which is based on the evaluation of closed expressions.

虚情假意 发表于 2025-3-23 15:47:30

http://reply.papertrans.cn/32/3134/313350/313350_12.png

attenuate 发表于 2025-3-23 18:33:59

http://reply.papertrans.cn/32/3134/313350/313350_13.png

和谐 发表于 2025-3-24 00:52:35

Wittgenstein’s Diagonal Argument: A Variation on Cantor and Turing the remark “Turings ‘machines’: these machines are humans who calculate. And one might express what he says also in the form of games”. Though most of the extant literature interprets the remark as a criticism of Turing’s philosophy of mind (that is, a criticism of forms of computationalist or func

Albinism 发表于 2025-3-24 06:10:59

http://reply.papertrans.cn/32/3134/313350/313350_15.png

物质 发表于 2025-3-24 07:37:08

The “Middle Wittgenstein” and Modern Mathematics beginning of the 1930s when he starts to emphasise the autonomy of the grammar of language and to talk about grammatical pictures and language games as objects of comparison. By examining certain crucial features in this change in Wittgenstein’s thinking, it will be shown that he received decisive

Hirsutism 发表于 2025-3-24 11:56:08

A Computational Interpretation of Forcing in Type Theoryt types. The argument was constructive, and so contains implicitly an algorithm which computes a witness that a given functional is uniformly continuous. We present here such an algorithm, which provides a possible computational interpretation of forcing.

Ebct207 发表于 2025-3-24 17:20:46

Program Testing and the Meaning Explanations of Intuitionistic Type Theorytionistic type theory are viewed as conjectures which can be tested in order to be corroborated or refuted. This point of view provides a new perspective on the meaning of hypothetical judgements, since tests for such judgements need methods for generating inputs. Among other things, we need to gene

不合 发表于 2025-3-24 23:03:10

http://reply.papertrans.cn/32/3134/313350/313350_19.png

Customary 发表于 2025-3-25 01:58:48

Machine Translation and Type Theoryrnate. Grammatical Frameword (GF) is introduced as an approach that uses type theory to provide high-quality translation between multiple languages. GF translation is fundamentally grammar-based but can be combined with statistical methods such as learning translation models from a corpus and rankin
页: 1 [2] 3 4 5 6
查看完整版本: Titlebook: Epistemology versus Ontology; Essays on the Philos P. Dybjer,Sten Lindström,G. Sundholm Book 2012 Springer Science+Business Media Dordrecht