Abstract

In some bicategories, the 1-cells are `morphisms' between the 0-cells, such as functors between categories, but in others they are `objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the `morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change `nonalgebraically', using categorical ...

Abstract

Categorical proof theory is an approach to understanding the structure of proofs. We illustrate the idea first by analyzing G del's Dialectica interpretation and the Diller-Nahm variant in categorical terms. Then we consider the problematic question of the structure of classical proofs. We show how double negation translations apply in the case of the Dialectica interpretations. Finally we formulate a proposal as to how to give a more faithful analysis of proofs in the sequent calculus. ...

Abstract

Such a universal instrument for guiding the learning, development, and use of advanced mathematics does not fail to have its indications also in areas of school and college mathematics, in the most basic relationships of space and quantity and the calculations based on those relationships. In saying "take categories seriously", I advocate noticing, cultivating, ...

Abstract

Sunto  In questo articolo viene rigorosamente sviluppata l'analogia fra dist (a, b)+dist (b, c)≥dist (a, c) e hom (A, B) ⊗ hom (B, C)→ hom (A, C), giungendo a numerosi risultati generali sugli spazi metrici, come conseguenza di una «logica pura generalizzata» i cui «valori di verità» sono scelti in una arbitraria categoria chiusa. ...

Abstract

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is 𝒫-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of 𝒫-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no ...

Abstract

Genericity is the idea that the same program can work at many different data types. Longo, Milstead and Soloviev proposed to capture the inability of generic programs to probe the structure of their instances by the following equational principle: if two generic programs, viewed as terms of type XA[X], are equal at any given instance A[T], then they are equal at all instances. They proved that this rule is admissible in a certain extension of System ...

Abstract

The paper describes an abstract interpretation technique based on lazy functional programming, and applies it to the proof of Conway’s Lost Cosmological Theorem, a combinatorial proposition analogous to the four color theorem or Kepler’s conjecture, which essentially states that a certain predicate holds of all lists of integers from 1 to 4. The technique makes use of the semantics of Haskell in the following way: evaluating a predicate on a partial lazy list to True proves that the predicate would evaluate ...

Abstract

Containers are a semantic way to talk about strictly positive types. In previous work it was shown that containers are closed under various constructions including products, coproducts, initial algebras and terminal coalgebras. In the present paper we show that, surprisingly, the category of containers is cartesian closed, giving rise to a full cartesian closed subcategory of endofunctors. The result has interesting applications in generic programming and representation of higher order abstract syntax. We also show that while the category of containers ...

Abstract

Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly. We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language. ...

Abstract

This text presents topos theory as it has developed from the study of sheaves. Sheaves arose in geometry as coefficients for cohomology and as descriptions of the functions appropriate to various kinds of manifolds (algebraic, analytic, etc.). Sheaves also appear in logic as carriers for models of set theory as well as for the semantics of other types of logic. Grothendieck introduced a topos as a category of sheaves for algebraic geometry. Subsequently, Lawvere and Tierney obtained ...

Abstract

Proof theory is the result of a short and tumultuous history, developed on the periphery of mainstream mathematics. Hence, its language is often idiosyncratic: sequent calculus, cut-elimination, subformula property, etc. This survey is designed to guide the novice reader and the itinerant mathematician along a smooth and consistent path, investigating the symbolic mechanisms of cut-elimination, and their algebraic transcription as coherence diagrams in categories with structure. This spiritual journey at the meeting point of linguistic and algebra is demanding at times, ...

Note (first note only)

found by way of sigfpe, great explanation of the Yoneda lemma.

Abstract

This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type which is substitutive , allowing us to reason by replacing equal for equal in propositions; which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality -- functions are equal if they take equal ...

Abstract

We show that any monad whose unit and extension operations are expressible as purely functional terms can be embedded in a call-by-value language with “composable continuations”. As part of the development, we extend Meyer and Wand's characterization of the relationship between continuation-passing and direct style to one for continuation-passing vs. general “monadic” style. We further show that the composable-continuations construct can itself be represented using ordinary, non-composable first-class continuations and a single piece of state. Thus, in the presence of two ...

Abstract

The work reported in this thesis arises from the old idea, going back to the origins of constructive logic, that a proof is fundamentally a kind of program. If proofs can be considered as programs, then one might expect that proof theory should have much to contribute to the theory of programming. This has indeed turned out to be the case. Various technologies developed in proof theory are now widely used in computer science for formulating and investigating programming languages and logics ...

Abstract

In the 1920s, David Hilbert proposed a research program with the aim of providing mathematics with a secure foundation. This was to be accomplished by first formalizing logic and mathematics in their entirety, and then showing—using only so-called finitistic principles—that these formalizations are free of contradictions. In the area of logic, the Hilbert school accomplished major advances both in introducing new systems of logic, and in developing central metalogical notions, such as completeness and decidability. The analysis of unpublished material presented in ...

Abstract

Hilbert's finitist program was not created at the beginning of the twenties solely to counteract Brouwer's intuitionism, but rather emerged out of broad philosophical reflections on the foundations of mathematics and out of detailed logical work; that is evident from notes of lecture courses that were given by Hilbert and prepared in collaboration with Bernays during the period from 1917 to 1922. These notes reveal a dialectic progression from a critical logicism through a radical constructivism toward finitism; the progression has ...

Abstract

We model notions of computation using algebraic operations and equations. We show that these generate several of the monads of primary interest that have been used to model computational e#ects, with the striking omission of the continuations monad. We focus on semantics for global and local state, showing that taking operations and equations as primitive yields a mathematical relationship that reflects their computational relationship. ...

Abstract

We reformulate the theory of ludics introduced by Girard, aiming at giving a foundation to computability and complexity theories in future. We introduce a handy syntax for designs, the main objects of ludics, that simplifies Curien's concrete syntax. Our syntax also incorporates explicit cuts for the sake of computational expressivity. We also consider design generators that allow for finite representation of some infinite designs. A normalization procedure in the style of Krivine's abstract machine directly works on generators, giving rise to ...

Abstract

Abstract.  In logic, diagrams have been used for a very long time. Nevertheless philosophers and logicians are not quite clear about the logical status of diagrammatical representations. Fact is that there is a close relationship between particular visual (resp. graphical) properties of diagrams and logical properties. This is why the representation of the four categorical propositions by different diagram systems allows a deeper insight into the relations of the logical square. In this paper I want to give some examples. ...

Abstract

ABSTRACT. A topological space is sober if it has exactly the points that are dictated by its open sets. We explain the analogy with the way in which computational values are determined by the observations that can be made of them. A new definition of sobriety is formulated in terms of lambda calculus and elementary category theory, with no reference to lattice structure, but, for topological spaces, this coincides with the standard lattice-theoretic definition. The primitive symbolic and categorical structures are ...

Abstract

Over the last 45 years, Boolean theorem has been generalized and extended in several different directions and its applications have reached into almost every area of modern mathematics; but since it lies on the frontiers of algebra, geometry, general topology and functional analysis, the corpus of mathematics which has arisen in this way is seldom seen as a whole. In order to give a unified treatment of this rather diverse body of material, Dr Johnstone begins by developing the theory of ...

Abstract

STONE DUALITY PAUL TAYLOR Transmitted by Robert Rosebrugh ABSTRACT. The contravariant powerset, and its generalisations X to the lattices of open subsets of a locally compact topological space and of recursively enumerable subsets of numbers, satisfy the Euclidean principle that ^ F () = ^ F (>). Conversely, when the adjunction ( ) a ( ) is monadic, this equation implies that classies some class of monos, and the Frobenius law 9x:((x) ^ ) = (9x:(x)) ^ ) for the... ...

Abstract

Game semantics aim at describing the interactive behaviour of proofs by interpreting formulas as games on which proofs induce strategies. In this article, we introduce a game semantics for a fragment of first order propositional logic. One of the main difficulties that has to be faced when constructing such semantics is to make them precise by characterizing definable strategies - that is strategies which actually behave like a proof. This characterization is usually done by restricting to the model to strategies satisfying subtle combinatory conditions such as innocence, ...

Abstract

I argue for the following four theses. (1) Denial is not to be analysed as the assertion of a negation. (2) Given the concepts of assertion and denial, we have the resources to analyse logical consequence as relating arguments with multiple premises and multiple conclusions. Gentzen’s multiple conclusion calculus can be understood in a straightforward, motivated, non-question-begging way. (3) If a broadly anti-realist or inferentialist justification of a logical system works, it works just as well for classical logic as it ...

Abstract

This paper compares two different styles of reasoning with inductively defined predicates, each style being encapsulated by a corresponding sequent calculus proof system. The first system supports traditional proof by induction, with induction rules formulated as sequent rules for introducing inductively defined predicates on the left of sequents. We show this system to be cut-free complete with respect to a natural class of Henkin models; the eliminability of cut follows as a corollary. The second system uses infinite (non-well-founded) proofs to represent arguments by ...

Abstract

Functional programming languages often feature mechanisms that involve complex computations at the level of types. These mechanisms can be analyzed uniformly in the framework of dependent types, in which types may depend on values. The purpose of this chapter is to give some background for such an analysis. We present here precise theorems, that should hopefully help the reader to understand to which extent statements like "introducing dependent types in a programming language implies that type checking is ...

Note (first note only)

A great explanation of pure type systems.

Abstract

This note analyzes in terms of categorial proof theory some standard assumptions about negation in the absence of any other connective. It is shown that the assumptions for an involutive negation, like classical negation, make a kind of adjoint situation, which is named involutive adjunction. The notion of involutive adjunction amounts in a precise sense to adjunction where an endofunctor is adjoint to itself. ...

Abstract

The question "What is category theory" is approached by focusing on universal mapping properties and adjoint functors. Category theory organizes mathematics using morphisms that transmit structure and determination. Structures of mathematical interest are usually characterized by some universal mapping property so the general thesis is that category theory is about determination through universals. In recent decades, the notion of adjoint functors has moved to center-stage as category theory's primary tool to characterize what is important and universal in mathematics. Hence our focus here is to present a theory of ...