Zobrazeno 1 - 10
of 66
pro vyhledávání: '"Jonathan P. Seldin"'
Autor:
J. Roger Hindley, Jonathan P. Seldin
Combinatory logic and lambda-calculus, originally devised in the 1920s, have since developed into linguistic tools, especially useful in programming languages. The authors'previous book served as the main reference for introductory courses on lambda-
Publikováno v:
Annals of the Canadian Society for History and Philosophy of Mathematics/ Société canadienne d’histoire et de philosophie des mathématiques ISBN: 9783030952006
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::836b2c051c1b4bc54d95b785d796cbd3
https://doi.org/10.1007/978-3-030-95201-3_11
https://doi.org/10.1007/978-3-030-95201-3_11
Autor:
Jonathan P. Seldin
Publikováno v:
Theoretical Computer Science. 663:34-58
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::df62ffaecb6d701b26b5ff00a025168e
https://doi.org/10.1016/j.tcs.2016.12.016
https://doi.org/10.1016/j.tcs.2016.12.016
Publikováno v:
Journal of Applied Logic. 18:42-70
There are two versions of type assignment in the -calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called domain free), in which it is not. As an example, in Church-style typing, x:A.x is the identity functio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a91bf0c829b3292642afa52a7f1c0022
https://doi.org/10.1016/j.jal.2016.05.008
https://doi.org/10.1016/j.jal.2016.05.008
Autor:
Jonathan P. Seldin
Publikováno v:
Studies in Universal Logic ISBN: 9783319247540
In this paper it is shown that every intermediate logic obtained from intuitionistic logic by adding a disjunction can be normalized. However, the normalization procedure is not as complete as that for intuitionistic and minimal logic because some re
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0fecd31254dd49e2911e8ad16191f032
https://doi.org/10.1007/978-3-319-24756-4_12
https://doi.org/10.1007/978-3-319-24756-4_12
Autor:
Jonathan P. Seldin
Publikováno v:
Theoretical Computer Science. 412:4905-4918
Combinatory logic (CL) is generally regarded as equivalent to @l-calculus (@l), and in most respects, it is. However, with respect to reduction, the equivalence is not complete. In CL, there is not, as yet, a reduction relation which is generally acc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::46961c04574c3258b3a00a8635ba71d6
https://doi.org/10.1016/j.tcs.2011.02.002
https://doi.org/10.1016/j.tcs.2011.02.002
Autor:
Jonathan P. Seldin
Publikováno v:
Logica Universalis. 5:91-100
In 1939, Curry proposed a philosophy of mathematics he called formalism. He made this proposal in two works originally written then, although one of them was not published until 1951. These are the two philosophical works for which Curry is known, an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::031d5a20687bd2e9d1fa36cf3cfda68d
https://doi.org/10.1007/s11787-011-0028-3
https://doi.org/10.1007/s11787-011-0028-3
Autor:
Jonathan P. Seldin
Publikováno v:
Trends in Logic ISBN: 9789400775473
Anybody using a theorem prover or proof assistant will want to have confidence that the system involved will not permit the derivation of false results. On some occasions, there is more than the usual need for this confidence. This chapter discusses
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::29aceceb34d4bc7a2a8abf09992463c1
https://doi.org/10.1007/978-94-007-7548-0_7
https://doi.org/10.1007/978-94-007-7548-0_7
Autor:
Jonathan P. Seldin
Publikováno v:
Journal of Symbolic Logic. 65:1076-1114
Evidence is given that implication (and its special case, negation) carry the logical strength of a system of formal logic. This is done by proving normalization and cut elimination for a system based on combinatory logic or λ-calculus with logical
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::bdbed4f764a6b5e553bc0642af51aba7
https://doi.org/10.2307/2586689
https://doi.org/10.2307/2586689
Autor:
Jonathan P. Seldin
Publikováno v:
Theoretical Computer Science. 243(1-2):199-215
A Gentzen-style L-formulation of the calculus of constructions is presented and proved equivalent to a natural deduction formulation based on that of Seldin (1997). The L-rules corresponding to the conversion rules of the natural deduction system are
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7d26491574824d1c8cffef2d7bda010e