We investigate a new denotational model of linear logic based on the purely relational model. In this semantics, webs are equipped with a notion of ‘finitary’ subsets satisfying a closure condition and proofs are interpreted as finitary sets. In spite of a formal similarity, this model is quite different from the usual models of linear logic (coherence semantics, hypercoherence semantics, the various existing game semantics…). In particular, the standard fix-point operators used for defining the general recursive functions are not finitary, although the primitive recursion operators are. This model can be considered as a discrete analogue of the Köthe space semantics introduced in a previous paper: we show how, given a field, each finiteness space gives rise to a vector space endowed with a linear topology, a notion introduced by Lefschetz in 1942, and we study the corresponding model where morphisms are linear continuous maps (a version of Girard's quantitative semantics with coefficients in the field). In this way we obtain a new model of the recently introduced differential lambda-calculus.

The existence of semi-pullbacks for stochastic relations over analytic spaces is addressed. It is shown by means of a measure extension that the theory of measurable selectors for measurable relations may be employed for its solution. The category of stochastic relations is shown not to have (weak) pullbacks.

Constructive type theory is an expressive programming language in which both algorithms and proofs can be represented. A limitation of constructive type theory as a programming language is that only terminating programs can be defined in it. Hence, general recursive algorithms have no direct formalisation in type theory since they contain recursive calls that satisfy no syntactic condition guaranteeing termination. In this work, we present a method to formalise general recursive algorithms in type theory. Given a general recursive algorithm, our method is to define an inductive special-purpose accessibility predicate that characterises the inputs on which the algorithm terminates. The type-theoretic version of the algorithm is then defined by structural recursion on the proof that the input values satisfy this predicate. The method separates the computational and logical parts of the definitions and thus the resulting type-theoretic algorithms are clear, compact and easy to understand. They are as simple as their equivalents in a functional programming language, where there is no restriction on recursive calls. Here, we give a formal definition of the method and discuss its power and its limitations.

We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin. The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for existing category-theoretic notions of relational parametricity. We provide examples of parametric models and describe a way of constructing parametric models from given models of the second-order lambda calculus.

In this paper we introduce a new hierarchical graph model to structure large graphs into small components by distributing the nodes (and, likewise, edges) into a hierarchy of packages. In contrast to other known approaches, we do not fix the type of underlying graphs. Moreover, our model is equipped with a rule-based transformation concept such that hierarchical graphs are not restricted to being used only for the static representation of complex system states, but can also be used to describe dynamic system behaviour.