www.elsevier.com/locate/entcs Relationally Staged Computations in Calculi of Mobile Processes (2009)
Neil Ghani, Kidane Yemane, Björn Victor
We apply the recently developed techniques of higher order abstract syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with...
Representations of Stream Processors Using Nested Fixed Points (2009)
Ghani, Neil, Hancock, Peter, Pattinson, Dirk
We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions. We define also an...
21.1 GENERALIZING SHORT CUT FUSION 21.1.1 Introducing Short Cut Fusion (2009)
Abstract: Fusion is the process of improving the efficiency of modularly constructed programs by transforming them into monolithic equivalents. This paper defines a generalization of the...
Monads are commonplace programming devices that are used to uniformly structure computations; in particular, they are often used to mimic the effects of impure features such as state, error handling,...
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor Mcbride, Peter Morris
Abstract. The search for an expressive calculus of datatypes in which canonical algorithms can be easily written and proven correct has proved to be an enduring challenge to the theoretical computer...
Abstract Constructing Strictly Positive Families (2008)
Peter Morris, Thorsten Altenkirch, Neil Ghani
data types one must go beyond the traditional treatment of data types as being inductive types and, instead, consider them as inductive families. Strictly positive types (SPTs) form a grammar for...
Representing Cyclic Structures as Nested Datatypes (2008)
Neil Ghani, Makoto Hamana, Tarmo Uustalu, Varmo Vene
We show that cyclic structures, i.e., finite or possibly infinite structures with backpointers, unwindable into possibly infinite structures, can be elegantly represented as nested datatypes. This...
∂ for Data: Differentiating Data Structures (2008)
Michael Abbott, Neil Ghani, Thorsten Altenkirch, Conor Mcbride
This paper and our conference paper (Abbott, Altenkirch, Ghani, and McBride, 2003b) explain and analyse the notion of the derivative of a data structure as the type of its one-hole contexts based on...
WOOD 2004 Preliminary Version Difunctorial Semantics of Object Calculus Abstract (2008)
In this paper we give a denotational model for Abadi and Cardelli’s first order object calculus FOb1+×µ (without subtyping) in the category pCpo. The key novelty of our model is its extensive use...
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor Mcbride, Peter Morris
Abstract. The search for an expressive calculus of datatypes in which canonical algorithms can be easily written and proven correct has proved to be an enduring challenge to the theoretical computer...
ABSTRACT Build, Augment and Destroy. Universally. (2008)
We give a semantic footing to the fold/build syntax of programming with inductive types, covering shortcut deforestation, based on a universal property. Specifically, we give a semantics for...
Chapter 1 Generalizing the AUGMENT Combinator (2008)
Neil Ghani, Tarmo Uustalu, Varmo Vene
Abstract: The usual initial algebra semantics of inductive types provides a clear and uniform explanation for the FOLD combinator. In an APLAS 2004 paper [1], we described an alternative equivalent...
Representing Cyclic Structures as Nested Datatypes (2008)
Neil Ghani, Makoto Hamana, Tarmo Uustalu, Varmo Vene
We show that cyclic structures, i.e., finite or possibly infinite structures with backpointers, unwindable into possibly infinite structures, can be elegantly represented as nested datatypes. This...
Nordic Journal of Computing 10(2003), 290–312. REWRITING VIA COINSERTERS (2008)
Abstract. This paper introduces a semantics for rewriting that is independent of the data being rewritten and which, nevertheless, models key concepts such as substitution which are central to...
Nordic Journal of Computing 10(2003), 290–312. REWRITING VIA COINSERTERS (2008)
Abstract. This paper introduces a semantics for rewriting that is independent of the data being rewritten and which, nevertheless, models key concepts such as substitution which are central to...
DOI: 10.1051/ita:2003021 SOLVING ALGEBRAIC EQUATIONS USING COALGEBRA (2008)
Federico De Marchi, Neil Ghani, Christoph Lüth
Abstract. Algebraic systems of equations define functions using recursion where parameter passing is permitted. This generalizes the notion of a rational system of equations where parameter passing...
Explicit Substitutitions for Constructive Necessity (2007)
Neil Ghani, Valeria De Paiva, Eike Ritter
Machine. be applied to design an abstract machine from our modal calculus with explicit substitutions. The main application of our modal calculus is as a framework for specifying and analysing...
Coalgebraic Monads, Neil Ghani, Christoph Luth, Federico De Marchi
This paper introduces coalgebraic monads as a unified model of term algebras covering fundamental examples such as initial algebras, final coalgebras, rational terms and term graphs. We develop a...
FB 3 | Mathematik und Informatik, Universitat Bremen (2007)
Abstract. This paper argues that the core of modularity problems is an understanding of how individual components of a large system interact with each other, and that this interaction can be...
This thesis concerns rewriting in the typed-calculus. Traditional categorical models of typed-calculus use concepts such as functor, adjunction and algebra to model type constructors and their...
Abstract. Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lu96], this semantics was used to...
Composing Monads Using Coproducts (2007)
Christoph Lüth, Christoph L Uth, Neil Ghani
Monads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a...
Coproducts Of Ideal Monads (2007)
The question of how to combine monads arises naturally in many areas with much recent interest focusing on the coproduct of two monads. In general, the coproduct of arbitrary monads does not always...
Brouwerian stream processors (2007)
Neil Ghani, Peter Hancock, Dirk Pattinson
We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions. We define also an...
Continuous functions on final coalgebras (2007)
Neil Ghani, Peter Hancock, Dirk Pattinson
In a previous paper we have given a representation of continuous functions on streams, both discrete-valued functions, and functions between streams. the topology on streams is the ‘Baire ’...
Initial algebra semantics is enough (2007)
Abstract. Initial algebra semantics is a cornerstone of the theory of modern functional programming languages. For each inductive data type, it provides a fold combinator encapsulating structured...
String rewriting for Double Coset Systems (2005)
Brown, Ronald, Ghani, Neil, Heyworth, Anne, Wensley, Christopher D.
In this paper we show how string rewriting methods can be applied to give a new method of computing double cosets. Previous methods for double cosets were enumerative and thus restricted to finite...
Monadic augment and generalised short cut fusion (2005)
Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. This paper further develops the monadic programming...
Monadic augment and generalised short cut fusion (2005)
Monads are commonplace programming devices that are used to uniformly structure computations with effects such as state, exceptions, and I/O. This paper further develops the monadic programming...
Constructing polymorphic programs with quotient types (2004)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. The efficient representation and manipulation of data is one of the fundamental tasks in the construction of large software systems. Parametric polymorphism has been one of the most...
Neil Ghani, Christoph L Üth, Federico De Marchi
This paper introduces guarded and strongly guarded monads as a unified model of a variety of different term algebras covering fundamental examples such as initial algebras, final coalgebras, rational...
Build, augment and destroy. Universally (2004)
Neil Ghani, Tarmo Uustalu, Varmo Vene
Abstract. We give a semantic footing to the fold/build syntax of programming with inductive types, covering shortcut deforestation, based on a universal property. Specifically, we give a semantics...
Representing nested inductive types using W-types (2004)
Michael Abbott, Thorsten Altenkirch, Neil Ghani
Abstract. We show that strictly positive inductive types, constructed from polynomial functors, constant exponentiation and arbitrarily nested inductive types exist in any Martin-Löf category...
ISSN 1404-3203Relationally Staged Computations in Calculi of Mobile Processes (2004)
Neil Ghani, Kidane Yemane, Björn Victor, Neil Ghani, Kidane Yemane, Björn Victor
syntax and functorial operational semantics to give a compositional and fully abstract semantics for the π-calculus equipped with open bisimulation. The key novelty in our work is the realisation...
Explicit substitutions and higher-order syntax (2003)
Recently there has been a great deal of interest in higherorder syntax which seeks to extend standard initial algebra semantics to cover languages with variable binding by using functor categories....
Derivatives of containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride’s idea that the type of one-hole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
Categories of Containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani
Abstract. We introduce the notion of containers as a mathematical formalisation of the idea that many important datatypes consist of templates where data is stored. We show that containers have good...
Categories of Containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani
Abstract. We introduce the notion of containers as a mathematical formalisation of the idea that many important datatypes consist of templates where data is stored. We show that containers have good...
Explicit substitutions and higher-order syntax (2003)
Neil Ghani, Tarmo Uustalu, Makoto Hamana
Abstract. Recently there has been a great deal of interest in higher-order syntax which seeks to extend standard initial algebra semantics to cover languages with variable binding. The canonical...
Derivatives of containers (2003)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride’s idea that the type of one-hole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
Dualising initial algebras. Coalgebraic methods in computer science (Genova, 2001) (2003)
Ghani, Neil, Lüth, Christoph, De Marchi, Federico, Power, John
Derivatives of Containers (2002)
Michael Abbott, Thorsten Altenkirch, Neil Ghani, Conor Mcbride
Abstract. We are investigating McBride's idea that the type of onehole contexts are the formal derivative of a functor from a categorical perspective. Exploiting our recent work on containers we...
Abstract. This paper argues that the core of modularity problems is an understanding of how individual components of a large system interact with each other, and that this interaction can be...
DOI: 10.1017/S0960129502003912 Printed in the United Kingdom Dualising initial algebras (2001)
Neil Ghani, Christoph L Üth, Federico De Marchi
Whilst the relationship between initial algebras and monads is well understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more...
Categorical models for explicit substitutions (1999)
Neil Ghani, Valeria Paiva, Eike Ritter
This paper concerns itself with the categorical semantics of-calculi extended with explicit substitutions. For the simply-typed-calculus, indexed categories seem to provide the right categorical...
Rewriting the Conditions in Conditional Rewriting (1999)
Neil Ghani, Christoph Lüth, Stefan Kahrs
Category theory has been used to provide a semantics for term rewriting systems at an intermediate level of abstraction between the actual syntax and the relational model. Recently we have developed...
Rewriting the Conditions in Conditional Rewriting (1999)
Neil Ghani, Christoph Lüth, Stefan Kahrs
Category theory provides a semantics for term rewriting systems at an intermediate level of abstraction between the actual syntax and the relational model. Recently we have developed a semantics for...
Categorical Models of Explicit Substitutions (1999)
Neil Ghani, Valeria De Paiva, Eike Ritter
. Indexed categories provide models of cartesian calculi of explicit substitutions. However, these structures are inherently non-linear and hence cannot be used to model linear calculi of explicit...
An e cient linear abstract machine with single-pointer (1998)
Francisco Alberti, Neil Ghani, Valeria De Paiva, Eike Ritter Y
property
Linear explicit substitutions (extended abstract (1998)
Neil Ghani, Valeria Paiva, Eike Ritter
The-calculus [1] adds explicit substitutions to the-calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper...
Linear Explicit Substitutions (1998)
Neil Ghani, Valeria De Paiva, Eike Ritter
The oe-calculus adds explicit substitutions to the -calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper...
Linear Explicit Substitutions (1998)
Neil Ghani, Valeria De Paiva, Eike Ritter
The oe-calculus adds explicit substitutions to the -calculus so as to provide a theoretical framework within which the implementation of functional programming languages can be studied. This paper...
Categorical Models of Explicit Substitutions (1998)
Neil Ghani, Valeria De Paiva, Eike Ritter
This paper concerns itself with the categorical semantics of -calculi extended with explicit substitutions. For the simply-typed -calculus, indexed categories seem to provide the right categorical...
Eta-Expansions in Dependent Type Theory - The Calculus of Constructions (1997)
. Although the use of expansionary j-rewrite has become increasingly common in recent years, one area where j-contractions have until now remained the only possibility is in the more powerful type...
Monads and Modular Term Rewriting (1997)
Christoph Luth And, Christoph Luth, Neil Ghani
. Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lu96], the usefulness of this semantics...
On Modular Properties of Higher Order Extensional Lambda Calculi (1997)
Roberto Di Cosmo, Neil Ghani, Roberto Di, Cosmo Neil Ghani, Ecole Normale Superieure
. We prove that confluence and strong normalisation are both modular properties for the addition of algebraic term rewriting systems to Girard's F ! equipped with either fi-equality or...
Monads and Modular Term Rewriting (1997)
. Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lu96], the usefulness of this semantics...
Monads and modular term rewriting (1997)
Abstract. Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In [Lü96], this semantics was used...
Adjoint Rewriting and the !-type constructor (1996)
This paper provides a sound, complete and decidable equational theory for the terms of the (I;\Omega ; \Gammaffi; !)-fragment of intuitionistic linear logic with respect to the class of models known...
Eta Expansions in System F (1996)
The use of expansionary j-rewrite rules in various typed -calculi has become increasingly common in recent years as their advantages over contractive j-rewrite rules have become apparent. Not only...
Eta-Expansions III - F omega (1996)
The use of expansionary j-rewrite rules in various typed -calculi has become increasingly common in recent years as their advantages over contractive j-rewrite rules have become apparent. Not only...
Eta Expansions in System F (1996)
Neil Ghani, Neil Ghani, Neil Ghani
The use of expansionary j-rewrite rules in various typed -calculi has become increasingly common in recent years as their advantages over contractive j-rewrite rules have become apparent. Not only...
This thesis is about rewriting in the typed lambda-calculus. Traditional categorical models of typed lambda-calculus use concepts such as functor, adjunction and algebra to model type constructors...
This thesis is about rewriting in the typed lambda-calculus. Traditional categorical models of typed lambda-calculus u se concepts such as functor, adjunction and algebra to model type constructors...
Abstract: "This thesis concerns rewriting in the typed [lambda]- calculus. Traditional categorical models of typed [lambda]-calculus use concepts such as functor, adjunction and algebra to model type...
βη-equality for coproducts (1995)
The use of expansionary η-rewrite rules in various typed λ-calculi has become increasingly common in recent years as their advantages over contractive η-rewrite rules have become apparent. Not...
betaeta-Equality for Coproducts (1995)
. Recently several researchers have investigated fij-equality for the simply typed -calculus with exponentials, products and unit types. In these works, j-conversion was interpreted as an expansion...
The Virtues of Eta-expansion (1993)
Interpreting j-conversion as an expansion rule in the simply-typed -calculus maintains the confluence of reduction in a richer type structure. This use of expansions is supported by categorical...
Algebraic semantics for flow diagram programs / (1990)
Thesis (M. Sc.)--Oxford University, 1990.