Skew and ω-Skew Confluence and Abstract Böhm Semantics (2008)
Abstract. Skew confluence was introduced as a characterization of nonconfluent term rewriting systems that had unique infinite normal forms or Böhm like trees. This notion however is not expressive...
There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become...
Zena M. Ariola, Jan Willem Klop
E-mail:det informatik.uni-bremen.de We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for different kinds of term graph rewriting;...
Bisimilarity in term graphs rewriting (2007)
Zena M. Ariola, Jan Willem Klop, Detlef Plump
We present a survey of con uence properties of (acyclic) term graph rewriting. Results and counterexamples are given for dierent kinds of term graph rewriting: besides plain applications of rewrite...
Computational Content of Unique Decomposition Proofs (2007)
Syntax (e.g., ELF) since one cannot represent evaluation contexts as meta-functions. Second one cannot use just one metavariable to describe the goal type E[x] as before. A crucial proof step in the...
Ling Cheung, Jesse Hughes, Zena M. Ariola
Abstract. We investigate the conditions under which least bisimulations exist with respect to set inclusion. In particular, we describe a natural way to remove redundant pairs from a given...
Zena M. Ariola, Zena M. Ariola
Compilation of Id, a higher-order non-strict functional language augmented with Istructures, is described in terms of two languages. The first language is called Kid, which is a Kernel language for...
Abstract. We precisely characterize a class of cyclic lambda-graphs, and then give a sound and complete axiomatization of the terms that represent a given graph. The equational axiom system is an...
Bisimilarity in term graphs rewriting (2007)
Z. M. Ariola, J. W. Klop, D. Plump, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Concise Graphs and Functional Bisimulations (2007)
Ling Cheung And, Ling Cheung, Jesse Hughes, Zena M. Ariola
We investigate the conditions under which least bisimulations exist with respect to set inclusion. In particular, we describe a natural way to remove redundant pairs from a given bisimulation. We...
A call-by-need lambda calculus (2007)
Ariola, Zena M., Felleisen, Matthias, Maraist, John, Odersky, Martin, Wadler, Philip
Zena M. Ariola, Hugo Herbelin, Amr Sabry, Zena M. Ariola, Hugo Herbelin, Amr Sabry
We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s law without enforcing Ex Falso Quodlibet. We show that a “natural ”...
A Typed Calculus Supporting Shallow Embeddings of Abstract Machines 1 Overview (2005)
Aaron Bohannon, Zena M. Ariola, Amr Sabry
The goal of this work is to draw a formal connection between steps taken by abstract machines and reductions in a system of proof terms for a version the sequent calculus. We believe that by doing so...
From syntactic theories to interpreters: Automating the proof of unique decomposition (2004)
Yong Xiao, Amr Sabry, Zena M. Ariola
Abstract. Developing syntactic theories for reasoning about programming languages usually involves proving a unique-decomposition lemma. The proof of such a lemma is tedious, error-prone, and is...
From Syntactic Theories to Interpreters: A Specification Language and Its Compilation (2000)
Xiao, Yong, Ariola, Zena M., Mauny, Michel
Recent years have seen an increasing need of high-level specification languages and tools generating code from specifications. In this paper, we introduce a specification language, {\splname}, which...
From syntactic theories to interpreters: A specification language and its compilation (2000)
Yong Xiao, Zena M. Ariola, Michel Mauny
Abstract. Recent years have seen an increasing need of high-level speci cation languages and tools generating code from specications. In this paper, we introduce a specication language, SL, which is...
Correctness of monadic state: an imperative call-by-need calculus (1998)
The extension of Haskell with a built-in state monad combines mathematical elegance with operational efficiency: ffl Semantically, at the source language level, constructs that act on the state are...
Bisimilarity in Term Graph Rewriting (1998)
Zena M. Ariola, Jan Willem Klop, D. Plump
We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for different kinds of term graph rewriting: besides plain applications of...
ABSTRACT Bisimilarity in Term Graph Rewriting (1998)
Z. M. Ariola, J. W. Klop, D. Plump, Issn -x, Copyright Stichting, Mathematisch Centrum, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Narrowing the Narrowing Space (1997)
We introduce a framework for managing as a whole the space of a narrowing computation. The aim of our framework is to find a finite representation of an infinite narrowing space. This, in turn,...
A call-by-need lambda calculus. (1996)
Ariola, Zena M., Felleisen, Matthias, Maraist, John, Odersky, Martin, Wadler, Philip
Lambda Calculus with Explicit Recursion (1996)
Z. M. Ariola, J. W. Klop, Issn -x, Zena M. Ariola, Jan-Willem Klop
This paper is concerned with the study of -calculus with explicit recursion, namely of cyclic -graphs. The starting point is to treat a -graph as a system of recursion equations involving -terms, and...
Z. M. Ariola, J. W. Klop, Issn -x, Zena M. Ariola, Jan Willem Klop
We present an equational framework for term graph rewriting with cycles. The usual notion of homomorphism is phrased in terms of the notion of bisimulation, which is well-known in process algebra and...
and Arvind. Properties of a first-order functional language with sharing (1995)
Zena M. Ariola, Zena M. Ariola
A calculus and a model for a first-order functional language with sharing is presented. In most implementations of functional languages, argument subexpressions in a function application are shared...
A Call-By-Need Lambda Calculus (1995)
Zena Ariola Computer, Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, Philip Wadler
The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their...
Cyclic Lambda Graph Rewriting (1994)
Zena M. Ariola, Jan Willem Klop
This paper is concerned with the study of cyclic - graphs. The starting point is to treat a -graph as a system of recursion equations involving -terms, and to manipulate such systems in an...
Relating Graph and Term Rewriting via Böhm Models (1993)
. Dealing properly with sharing is important for expressing some of the common compiler optimizations, such as common subexpressions elimination, lifting of free expressions and removal of invariants...
Relating Graph and Term Rewriting via Böhm Models (1993)
this paper we are interested in defining a term model for term graph rewriting systems, which allows us to prove total correctness of those optimizations. We introduce the notion of Bohm tree, and...
Equational Term Graph Rewriting (1993)
Zena M. Ariola, Jan Willem Klop, De Boelelaan A, Hv Amsterdam
We present an equational framework for term graph rewriting with cycles. The usual notion of homomorphism is phrased in terms of the notion of bisimulation, which is well-known in process algebra and...
Abstract: "Modern languages are too complex to be given direct operational semantics. For example, the operational semantics of functional languages has traditionally been given by translating them...
A Syntactic Approach to Program Transformations (1991)
Kid, a language for expressing compiler optimizations for functional languages is introduced. The language is λ-calculus based but treats let-blocks as first class objects. Let-blocks and...
In this paper we illustrate, using the Id language, that both the operational semantics of a language and its compilation process can be formalized together. Id is a higher-order non-strict...
Narrowing the narrowing space (1292)
Abstract. We introduce a framework for managing as a whole the space of a narrowing computation. The aim of our framework is to nd a nite representation of an innite narrowing space. This, in turn,...
Narrowing the narrowing space (1292)
Abstract. We introduce a framework for managing as a whole the space of a narrowing computation. The aim of our framework is to find a finite representation of an infinite narrowing space. This, in...