Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
TCS Journal 2003 Journal Article
Interpretation of proofs of the multiplicative-additive fragment of non-commutative logic, by using bimodules on coherent spaces and bilinear functions.
I&C Journal 1989 Journal Article
Moschovakis (1984, in “Computation and Proof Theory” (Y. Richter et al. , Eds.), Lect. Notes in Math. Vol. 1104, pp. 289–362, Springer-Verlag, Berlin) raised a question: to find a “logic of recursion, ” related to “recursion structures” as denotational models of the language of recursion investigated in the same paper. We give a positive answer to this question. The “logic of recursion” presented in our paper is a first-order many-sorted β-logic (cf. Girard, (in press), “Proof Theory and Logical Complexity, ” Vol. 2, Bibliopolis, Napoli), modified in order to deal with function symbols interpreted as partial functions, and extended with the operators λ (abstraction), R (recursion), I (iteration along the ordinal numbers). The operators λ and R are already present in Moschovakis' languages of recursion. The use of the operator I together with first-order many-sorted β-logic is needed for obtaining the completeness theorem.