Browsing Computer Science by Author "Kfoury, A.J."

OpenBU

Browsing Computer Science by Author "Kfoury, A.J."

Sort by: Order: Results:

  • Addendum to "New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi"
    Kfoury, A.J.; Wells, J.B. (Boston University Computer Science Department, 1995-03-31)
    This is an addendum to our technical report BUCS TR-94-014 of December 19, 1994. It clarifies some statements, adds information on some related research, includes a comparison with research be de Groote, and fixes two ...
  • Adding Polymorphic Abstraction to ML (Detailed Abstract)
    Kfoury, A.J.; Wells, J.B. (Boston University Computer Science Department, 1994-03-16)
    The ML programming language restricts type polymorphism to occur only in the "let-in" construct and requires every occurrence of a formal parameter of a function (a lambda abstraction) to have the same type. Milner in 1978 ...
  • Beta-Reduction As Unification
    Kfoury, A.J. (Boston University Computer Science Department, 1996-07-08)
    We define a unification problem ^UP with the property that, given a pure lambda-term M, we can derive an instance Gamma(M) of ^UP from M such that Gamma(M) has a solution if and only if M is beta-strongly normalizable. ...
  • A Characterization of First-Order Definable Subsets on Classes of Finite Total Orders
    Kfoury, A.J.; Wymann-Böni, M. (Boston University Computer Science Department, 1993-08)
    We give an explicit and easy-to-verify characterization for subsets in finite total orders (infinitely many of them in general) to be uniformly definable by a first-order formula. From this characterization we derive ...
  • Fixed Point vs. First-Order Logic on Finite Ordered Structures with Unary Relations
    Kfoury, A.J.; Wymann-Böni, M. (Boston University Computer Science Department, 1993-08-11)
    We prove that first order logic is strictly weaker than fixed point logic over every infinite classes of finite ordered structures with unary relations: Over these classes there is always an inductive unary relation which ...
  • An Infinite Pebble Game and Applications
    Kfoury, A.J.; Stolboushkin, A.P. (Boston University Computer Science Department, 1996-08-15)
    We generalize the well-known pebble game to infinite dag's, and we use this generalization to give new and shorter proofs of results in different areas of computer science (as diverse as "logic of programs" and "formal ...
  • A Linearization of the Lambda-Calculus and Consequences
    Kfoury, A.J. (Boston University Computer Science Department, 1996-08-19)
    If every lambda-abstraction in a lambda-term M binds at most one variable occurrence, then M is said to be "linear". Many questions about linear lambda-terms are relatively easy to answer, e.g. they all are beta-strongly ...
  • New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi
    Kfoury, A.J.; Wells, J.B. (Boston University Computer Science Department, 1994-12-19)
    Two new notions of reduction for terms of the λ-calculus are introduced and the question of whether a λ-term is beta-strongly normalizing is reduced to the question of whether a λ-term is merely normalizing under one of ...
  • Principality and Decidable Type Inference for Finite-Rank Intersection Types
    Kfoury, A.J.; Wells, J.B. (Boston University Computer Science Department, 1998-11-06)
    Principality of typings is the property that for each typable term, there is a typing from which all other typings are obtained via some set of operations. Type inference is the problem of finding a typing for a given term, ...
  • Programming Examples Needing Polymorphic Recursion
    Kfoury, A.J.; Hallett, J.J. (Boston University Computer Science Department, 2004-01-22)
    Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type ...

Search OpenBU


Advanced Search

Browse

Deposit Materials