By establishing an appropriate equivalence, we observe that the theory of semi-functors can be fully embedded in the theory of (ordinary) functors. As a result, standard properties and constructions on functors extend automatically to semi-functors.

Every accessible category is proved to be sketchable by a sketch with finite colimits. In contrast, a finitely accessible category is presented that cannot be sketched by a finitary sketch, i.e., a sketch with finite limits and finite colimits. Also, a category sketchable by a finitary sketch is found that is not finitely accessible.

We consider the following two properties of a functor F from a presheaf topos to the category of sets: (a) F preserves connected limits, and (b) the Artin glueing of F is again a presheaf topos. We show that these two properties are in fact equivalent. In the process, we develop a general technique for associating categorical properties of a category obtained by Artin glueing with preservation properties of the functor along which the glueing takes place. We also give a syntactic characterization of those monads on Set whose functor parts have the above properties, and whose units and multiplications are cartesian natural transformations.

The categorical dual construction of initial abstract data types is studied. The resulting terminal co-algebras represent not only an implementation independent semantics of infinite objects such as streams, but also a suitable formal basis for object types in the sense of the object-oriented programming paradigm. Instances of object types may be interpreted as abstract automata with several state transition functions representing the methods of an object, and several output functions representing the attributes. By structuring the index set of the possibly infinite family of methods, and by structuring the output set, one can specify specific object types. For dealing simultaneously with complex data types and object types, it is not necessary to live within a cartesian closed category. In ccc's there are standard functional constructions for object types, but object types are not necessarily a higher-order construction. A world of data types and object types may be combined with the Rewriting Logic of Meseguer to obtain a formal basis for concurrent object systems.

We propose a new framework for representing logics, called LF+, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF+ entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF+, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.

Equational deduction is generalised within a category-based abstract model theory framework, and proved complete under a hypothesis of quantifier projectivity, using a semantic treatment that regards quantifiers as models rather than variables, and valuations as model morphisms rather than functions. Applications include many- and order-sorted (conditional) equational logics, Horn clause logic, equational deduction modulo a theory, constraint logics, and more, as well as any possible combination among them. In the cases of equational deduction modulo a theory and of constraint logic the completeness result is new. One important consequence is an abstract version of Herbrand's Theorem, which provides an abstract model theoretic foundation for equational and constraint logic programming.

Categorical constructions inherent to a theory of algebras with strict partial operations are presented and exploited to provide a categorical deduction calculus for conditional existence equations and an alternative definition of such algebras based on the notion of syntactic categories. A compact presentation of the structural theory of parameterized (partial) specifications is given using the categorical approach. This theory is shown to be suitable for providing initial semantics as well as the compositionality results necessary for the definition of specification languages like ACT ONE and ACT TWO

We formulate a typed version of call-by-value λ-calculus containing variants of Felleisen's control operators A and C that provide explicit access to continuations and logically extend the propositions-as-types correspondence to classical propositional logic. We give an equational theory for this calculus, which is shown to be sound and complete with respect to a class of categorical models based on continuation-passing-style semantics.

A new correctness criterion for discriminating Proof Nets among Proof Structures of Multiplicative Linear Logic with the MIX rule is provided. This criterion is inspired by an original interpretation of Proof Structures as distributed systems, and logical formulae as processes. The computation inside a system corresponds to the logical flow of information inside a proof, that is, roughly speaking, a distributed version of Girard's token trip. Proof Nets are then characterised as deadlock free Proof Structures (deadlock free distributed systems). This result follows by explicitly considering the causal dependencies among logical formulae inside proofs, and it provides a new understanding of notions such as acyclicity, chains and empires in terms of concurrent computations.

In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with the PART-construction, which interprets total based algebras as partial algebras. This construction can be viewed as a simulation of Horn Clause Theories by means of Conditional Equational Theories. Other constructions in other frameworks are extendable to simulations in a similar way. The notion of categorical retractive simulation captures some essential properties of these, which allows us to measure the equivalence and difference between institutions.

Inspired by the work of S. Kaplan on positive/negative conditional rewriting, we investigate initial semantics for algebraic specifications with Gentzen formulas. Since the standard initial approach is limited to conditional equations (i.e. positive Horn formulas), the notion of semi-initial and quasi-initial algebras is introduced, and it is shown that all specifications with (positive) Gentzen formulas admit quasi-initial models.

The whole approach is generalized to the parametric case where quasi-initiality generalizes to quasi-freeness. Since quasi-free objects need not be isomorphic, the persistency requirement is added to obtain a unique semantics for many interesting practical examples. Unique persistent quasi-free semantics can be described as a free construction if the homomorphisms of the parameter category are suitably restricted. Furthermore, it turns out that unique persistent quasi-free semantics applies especially to specifications where the Gentzen formulas can be interpreted as hierarchical positive/negative conditional equations. The data type constructor of finite function spaces is used as an example that does not admit a correct initial semantics, but does admit a correct unique persistent quasi-initial semantics. The example demonstrates that the concepts introduced in this paper might be of some importance in practical applications.

In this work we show how some useful reductions known from ordinary intuitionistic propositional calculus can be modified for Intuitionistic Linear Logic (without modalities). The main reductions we consider are: (1) the reduction of the depth of formulas in the sequents by addition of new variables, and (2) the elimination of linear disjunction, tensor and constant F. Both transformations preserve deducibility, that is, a transformed sequent is deducible if and only if the initial one was deducible. The size of the sequent grows linearly in case (1) and ≤ On8 in case (2).

Tries, a form of string-indexed look-up structure, are generalized, in a manner first discovered by Wadsworth, to permit indexing by terms built according to an arbitrary signature. The construction is parametric with respect to the type of data to be stored as values; this is essential, because the recursion that defines tries appeals from one value type to others. ‘Trie’ (for any fixed signature) is then a functor, and the corresponding look-up function is a natural isomorphism.

The trie functor is in principle definable by the ‘initial fixed point’ semantics of Smyth and Plotkin. We simplify the construction, however, by introducing the ‘category-cpo’, a class of category within which calculations can retain some domain-theoretic flavor. Our construction of tries extends easily to many-sorted signatures.

Lambek used categories with indeterminates to capture explicit variables in simply typed λ-calculus. He observed that such categories with indeterminates can be described as Kleisli categories for suitable comonads. They account for ‘functional completeness’ for Cartesian (closed) categories.

Here we refine this analysis, by distinguishing ‘contextual’ and ‘functional’ completeness, and extend it to polymorphic λ-calculi. Since the latter are described as certain fibrations, we are lead to consider indeterminates, not only for ordinary categories, but also for fibred categories. Following a 2-categorical generalisation of Lambek's approach, such fibrations with indeterminates are presented as 'simple slices' in suitable 2-categories of fibrations; more precisely, as Kleisli objects. It allows us to establish contextual and functional completeness results for some polymorphic calculi.

Subtyping in the presence of recursive types for the λ-calculus was studied by Amadio and Cardelli in 1991 (Amadio and Cardelli 1991). In that paper they showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time. In this paper we give an 0(n2) algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states.

It is known that equality of recursive types and the covariant Bohm order can be decided efficiently by means of finite automata, since they are just language equality and language inclusion, respectively. Our results extend the automata-theoretic approach to handle orderings based on contravariance.

The concept of algebraic high-level net transformation systems combines two important lines of research recently introduced in the literature: algebraic high-level nets (AHL-nets for short) and high-level replacement systems (HLR-systems for short). In both cases a categorical formulation of the corresponding theory has turned out to be highly important and is also a good basis for the integration of these concepts in this paper.

AHL-nets combine Petri nets with algebraic specifications and provide a powerful specification technique for distributed systems including data types and processes.

HLR-systems are transformation systems for high-level structures such as graphs, hypergraphs, algebraic specifications and different kinds of Petri nets. The theory of HLRsystems - formulated already in a categorical framework - is applied in this paper to AHLnets. Thus we obtain AHL-net transformation systems as an instantiation of HLR-systems to AHL-nets. This allows us to build up AHL-nets from basic components and to transform the net structure using rules or productions in the sense of graph grammars. This concept is illustrated by extending the well-known example of ‘dining philosophers’. We are able to show that AHL-net-transformation systems satisfy several important compatibility properties. On the one hand we obtain a local Church-Rosser and Parallelism Theorem, which is well-known for graph grammars and has recently been generalized to HLR-systems. This allows us to analyse concurrency in AHL-nets not only on the token level but also on the level of transformations of the net structure. On the other hand, we consider the ‘fusion’ and ‘union’ constructions for high-level structures, motivated by corresponding concepts for high-level Petri nets in the literature, and we show compatibility of these constructions with derivations of HLR-systems in general and AHL-nettransformations in particular. This means compatibility of vertical and horizontal structuring in terms of software development.

We study a type system with a notion of subtyping that involves a largest type ⊤, a smallest type ⊥, atomic coercions between base types, and the usual ordering of function types. We prove that any λ-term typable in this system is strongly normalizing, which solves an open problem of Thatte. We also prove that the fragment without ⊥ types has strictly fewer terms. This demonstrates that ⊥ adds power to a type system.