Arrow Research search

Author name cluster

G. Longo

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.

2 papers
1 author row

Possible papers

2

I&C Journal 1995 Journal Article

A Calculus for Overloaded Functions with Subtyping

  • G. Castagna
  • G. Ghelli
  • G. Longo

We present a simple extension of typed λ-calculus where functions can be overloaded by putting different "branches of code" together. When the function is applied, the branch to execute is chosen according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that the branch selection depends on the "run-time type" of the argument, which may differ from its compile-time type, because of the existence of a subtyping relation among types. Hence overloading cannot be eliminated by a static analysis of code, but it is an essential feature to be dealt with during computation. We obtain in this way a type-dependent calculus, which differs from the various λ-calculi where types to not play any role during computation. We prove confluence and a generalized subject-reduction theorem for this calculus. We prove strong normalization for a "stratified" subcalculus. The definition of this calculus is guided by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensive stressed. We show that this calculus provides a foundation for types object-oriented languages which solves some of the problems of the standard record-based approach.

Details DOI

TCS Journal 1986 Journal Article

Computability in higher types, Pω and the completeness of type assignment

  • G. Longo
  • S. Martini

Pω, the powerset of the natural numbers, may be turned into an applicative structure by Myhill and Shepherdson, “·”. Then, for A, B ⊆ Pω, set A → B = {d ϵ Pω | ∀a ϵ A, da ϵ B}. Any effectively given domain (in the sense of Scott (1982)) can be embedded into Pω by a continuous and computable retraction (notation: X 〈c A X, for some A X ⊆ Pω, which is also an effectively given domain). We first prove that if X 〈c A X and Y 〈c A Y, then also A X → A Y is an effectively given domain and (☆): Cont(X, Y) 〈c A X → A Y, i. e. , the continuous functions can be embedded into A X → A Y. Let now P ⊆ Pω be the collection of single-valued sets, i. e. , P is isomorphic to the effectively given domain of the partial functions on ω, and let T be the function-type symbols, with (1) ϵ T. Then, for P 1 = P, P σ→τ = P σ → P τ extends the classical recursive operators at higher types. By (☆), Ershov's model of the Kleene-Kreisel countable functionals can effectively be embedded, by some G σ 's, into the type structure {P σ } σϵT in Pω. Thus, the recursive functionals correspond to the r. e. sets in the due types, for example, f has type σ → τ iff G σ→τ (f) is an r. e. set in P σ → P τ. {P σ } σϵT clearly yields a model for formal type assingnment to terms of λ-calculus, i. e. , for any assignment B of types to variables and any σ ϵ T one has B ⊢ σM⇒[M] ξB ϵ P σ, where ξ B: Var → Pω, according to B. We prove that also the reverse implication holds for typable terms. Thus, a completeness theorem for type checking is established over a model defined by an independent recursion-theoretical motivation.

Details DOI
v2026.09.13