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.
CSL Conference 2017 Conference Paper
The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2017 edition of the award.
CSL Conference 2013 Conference Paper
Common data-types, such as N, can be identified with term algebras. Thus each type can be construed as a global set; e. g. for N this global set is instantiated in each structure S to the denotations in S of the unary numerals. We can then consider each declarative program as an axiomatic theory, and assigns to it a semantic (Curry-style) type in each structure. This leads to the intrinsic theories of [Leivant, 2002], which provide a purely logical framework for reasoning about programs and their types. The framework is of interest because of its close fit with syntactic, semantic, and proof theoretic fundamentals of formal logic. This paper extends the framework to data given by coinductive as well as inductive declarations. We prove a Canonicity Theorem, stating that the denotational semantics of an equational program P, understood operationally, has type \tau over the canonical model iff P, understood as a formula has type \tau in every "data-correct" structure. In addition we show that every intrinsic theory is interpretable in a conservative extension of first-order arithmetic.
I&C Journal 2010 Journal Article
TCS Journal 2004 Journal Article
We continue from (Ann. Pure Appl. logic 114 (2002) 117) our study of reasoning about recursion equations in rudimentary theories for inductive data, dubbed intrinsic theories. We show that the functions that are provable using unipolar induction are precisely the primitive-recursive functions, where we call an instance of induction unipolar if data predicates do not occur in the induction formula both positively and negatively. Two special cases of this result are well known, namely induction over Σ 1 0 and Π 1 0. Here, however, induction formulas may have unrestricted quantifier alternations as long as those quantifiers that are relativized to data do not violate the prescribed restriction. The main technical challenge is in showing that the functions provable by unipolar induction, even in classical logic, are primitive-recursive. The result is generic with respect to the underlying inductive data, suggesting a potentially useful formalization of primitive-recursive mathematics.
TCS Journal 2003 Journal Article
This article has been withdrawn at the request of the author(s) and/or editor. The Publisher apologizes for any inconvenience this may cause. The full Elsevier Policy on Article Withdrawal can be found at http: //www. elsevier. com/locate/withdrawalpolicy
CSL Conference 2002 Conference Paper
Abstract In previous works we argued that second order logic with comprehension restricted to positive formulas can be viewed as the core of Feasible Mathematics. Indeed, the equational programs over strings that are provable in this logic compute precisely the poly-time computable functions. Here we investigate the provable functionals of this logic, and show that they are precisely Cook and Urquhart’s basic feasible functionals, BFF. This further confirms the stability of BFF as a notion of computational feasibility in higher type. Using a formula-as-type morphism, we also show that BFF consists precisely of the functionals that are lambda representable in F 2 restricted to positive type arguments (and trivially augmented with basic constructors and destructors).
LPAR Conference 2001 Conference Paper
Abstract Function provability in higher-order logic is a versatile and powerful framework for conceptual classification as well as verification and derivation of declarative programs. Here we show that the functions provable in second-order logic with first-order set-abstraction are precisely the elementary functions. This holds regardless of whether the logic is classical, intuitionistic, or minimal. The notion of provability here is not purely logical, as it incorporates a trivial theory of data, with axioms stating that each data object has a detectable main constructor which can be destructed. We show that this is necessary, by proving that without such rudimentary axioms the provable functions are merely the functions broadly-represented in the simply typed lambda calculus, a collection that does not even include integer subtraction.
TCS Journal 2000 Journal Article
We give a machine-independent characterization of the class of functions bitwise computable in alternating logarithmic time, with output of polynomial size. Recall that ALogTime is the same, for decision problems, as the UE∗ -uniform variant of NC 1 Ruzzo, J. Comput. System Sci. 22 (1981) 365–383. Our characterization is in terms of a weak form of ramified tree recurrence with substitutions. No initial functions other than basic tree operations are used, and no bounding conditions on the recurrence.
CSL Conference 1999 Conference Paper
Abstract We establish a tight correspondence between three major complexity classes and simple syntactic restrictions on applicative programs in the simply typed lambda calculus with a recurrence operator. The syntactic restrictions considered are: recurrence arguments cannot be passed as computed values (“input-driven terms”), abstracted higher-order variables can appear at most once (“solitary terms”), and abstracted variables cannot be eventually nested (“separated terms”). We show that the functions over word algebras represented by inputdriven terms are precisely the poly-time functions (a result akin to [8] (Chapter 24. 2)). When input-driven recurrence is permitted over all finite types, the elementary functions are obtained (a result akin to [1]). When terms are further restricted to solitary ones, even recurrence in all finite type yields only the poly-time functions. Finally, separated terms generate exactly the poly-space functions. The interest in the approach discussed here lies in its simplicity: the complexity characterizations are based on restricted use of standard applicative constructs, rather than a syntactic overlay as in ramified recurrence [ 3 ], [ 12 ], [ 15 ], [ 7 ], [ 21 ]. However, approaches based on ramified recurrence are more powerful than simple syntactic control, as well as more conceptually and methodologically coherent. Thus, the two approaches are complementary and of independent interest.
FOCS Conference 1998 Conference Paper
We show that a boolean valued function is in NC if it is defined by ramified schematic recurrence over trees. This machine-independent characterization uses no initial functions other than basic tree operations, and no bounding conditions on the recurrence. Aside from its technical interest, our result evidences the foundational nature of NC, thereby illustrating the merits of implicit (i. e. machine independent) computational complexity theory.
CSL Conference 1995 Conference Paper
Abstract We prove an applicative characterization of poly-space as the set of functions over \(\mathbb{W} = \{ 0, 1\} *\) defined by ramified \(\mathbb{W}\) -recurrence with parameter substitution. Intuitively, parameter substitution allows re-use of space in ways disallowed by ramified recurrence without substitution: it permits capturing by recurrence the flow of computation backwards from accepting configurations, thereby enabling the simulation of parallel (alternating) computing. Conversely, parameter substitution can be simulated by a computation that can repeatedly bifurcate into subcomputations, i. e. by parallelism that can be captured in poly-space.
TCS Journal 1993 Journal Article
We show that a function over a free algebra is definable in the simply typed λ-calculus (modulo the Böhm–Berarducci embedding) iff it is generated by predicative monotonic recurrence. Monotonic recurrence here is the generalization of iteration-with-parameters from n to arbitrary free algebras and our predicativity condition uses the notion of tiers introduced by Leivant (1990). In fact, we show that the same functions are generated by tiered monotonic recurrence whether 2 tiers or all finite tiers are used.
I&C Journal 1991 Journal Article
We consider predicative type-abstraction disciplines based on type quantification with finitely stratified levels. These lie in the vast middle ground between quantifier-free parametric abstraction and full impredicative abstraction. Stratified polymorphism has an unproblematic set-theoretic semantics, and may lend itself to new approaches to type inference, without sacrificing useful expressive power. Our main technical result is that the functions representable in the finitely stratified polymorphic λ-calculus are precisely the super-elementary functions, i. e. , the class ε 4 in Grzegorczyk's subrecursive hierarchy. This implies that there is no super-elementary bound on the length of optimal normalization sequences, and that the equality problem for finitely stratified polymorphic λ-expressions is not super-elementary. We also observe that finitely stratified polymorphism augmented with type recursion admits functional algorithms that are not typable in the full second order λ-calculus.
TCS Journal 1986 Journal Article
We use a perception of second-order typing in the λ-Calculus, as conveying semantic properties of expressions in models over λ-expressions, to exhibit natural and uniform proofs of theorems of Girard (1971/1972) and of Coppo, Dezani and Veneri (1981) about the relations between typing properties and computational properties of λ-expressions (solvability, normalizability, strong normalizability), and of some generalizations of these theorems.
FOCS Conference 1983 Conference Paper
We present a method of reasoning directly about functional programs in Second-Order Logic, based on the use of explicit second-order definitions for inductively defined data-types. Termination becomes a special case of correct typing. The formula-as-type analogy known from Proof Theory, when applied to this formalism, yields λ-expressions representing objects of inductively defined types, as well as λ-expressions representing functions between such types. A proof that a functional closed expression e is of type T maps into a λ-expression representing (the value of) e; and a proof that a function f is correctly typed maps into a λ-expression representing f (modulo the representations of objects of those types). When applied to integers and to numeric functions the mapping yields Church's numerals and the traditional function representations over them. The λ-expressions obtained under the isomorphism are typed (in the Second-Order Lambda Calculus). This implies that, for functions defined over inductively defined types, the property of being proved everywhere-defined in Second-Order Logic is equivalent to the property of being representable in the Second-Order Lambda Calculus. Extensions and refinements of this result lead to other characterizations of complexity classes by type disciplines. For example, log-space functions over finite structures are precisely the functions over finite-structures definable by λ-pairing-expressions in a predicative version of the Second-Order Lambda Calculus.
TCS Journal 1982 Journal Article
STOC Conference 1981 Conference Paper