Category Theory

Toposes, Triples, and Theories Barr, Michael and Charles Wells

Category Theory for Program Construction Meertens, Lambert (gzipped ps)

Categories, Types, and Structures Asperti, Andrea and Giuseppe Longo (Out of print, available online)

List of electronically available resources


Computability and Incomputability (PDF), Robert I. Soare, Lecture Notes In Computer Science; Vol. 4497 archive Proceedings of the 3rd conference on Computability in Europe: Computation and Logic in the Real World, Siena, Italy, Pages: 705 - 715, Year of Publication: 2007, ISBN:978-3-540-73000-2, DOI: 10.1007/978-3-540-73001-9_75

The conventional wisdom presented in most computability books and historical papers is that there were several researchers in the early 1930's working on various precise definitions and demonstrations of a function specified by a finite procedure and that they should all share approximately equal credit. This is incorrect. It was Turing alone who achieved the characterization, in the opinion of Gödel. We also explore Turing's oracle machine and its analogous properties in analysis.

Computability and recursion, Robert I. Soare, Bulletin of Symbolic Logic, 1996, Vol. 2, pages 284—321

We consider the informal concept of "computability" or "effective calculability" and two of the formalisms commonly used to define it, "(Turing) computability" and "(general) recursiveness." We consider their origin, exact technical definition, concepts, history, general English meanings, how they became fixed in their present roles, how they were first and are now used, their impact on nonspecialists, how their use will affect the future content of the subject of computability theory, and its connection to other related areas. 1 After a careful historical and conceptual analysis of computability and recursion we make several recommendations in section x7 about preserving the intensional differences between the concepts of "computability" and "recursion." Specifically we recommend that: the term "recursive" should no longer carry the additional meaning of "computable" or "decidable;" functions defined using Turing machines, register machines, or their variants should be called "computable" rather than "recursive;" we should distinguish the intensional difference between Church's Thesis and Turing's Thesis, and use the latter particularly in dealing with mechanistic questions; the name of the subject should be "Computability Theory" or simply Computability rather than "Recursive Function Theory."

Lambda Calculus (and Recursion)

Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I McCarthy, John (1960)

The Impact of the Lambda Calculus in Logic and Computer Science Henk Barendregt, The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997, pp 181-215

Abstract. One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.

Computational Foundations of Basic Recursive Function Theory Constable, Robert L. and Smith, Scott Fraser

In this approach computations are viewed as mathematical objects, and the major theorems in recursion theory may be classified according to which axioms about computation are needed to prove them.

Computational lambda-calculus and monads Moggi, Eugenio

Notions of computation and monads Moggi, Eugenio

Type Theory

A Formulation of the Simple Theory of Types, Alonzo Church; Source: J. Symbolic Logic Volume 5, Issue 2 (1940), 56-68.

Completeness in the Theory of Types Leon Henkin, The Journal of Symbolic Logic, Vol. 15, No. 2 (Jun., 1950), pp. 81-91 (article consists of 11 pages)

Proofs and Types Girard, Jean-Yves

Proofs and Programs (Type Theory: an introduction, some reflections). Giuseppe Longo

Naive Computational Type Theory, by Robert L. Constable; Proof and System-Reliability, H. Schwichtenberg and R. Steinbruggen (eds.), pp. 213-259, 2002.

…Here we follow the example of the mathematician Paul Halmos, who in 1960 wrote a 104-page book called Naïve Set Theory intended to make the subject accessible to practicing mathematicians. His book served many generations well…This article follows the spirit of Halmos' book and introduces type theory without recourse to precise axioms and inference rules, and with a minimum of formalism. I start by paraphrasing the preface to Halmos' book. The sections of this article follow his chapters closely.

Type Theory and Functional Programming(PDF), Simon Thompson, ISBN 0-201-41667-0, Addison-Wesley, 1991. (Out of Print)

The book can be thought of as giving both a first and a second course in type theory. We begin with introductory material on logic and functional programming, and follow this by presenting the system of type theory itself, together with many examples. As well as this we go further, looking at the system from a mathematical perspective, thus elucidating a number of its important properties. Then we take a critical look at the profusion of suggestions in the literature about why and how type theory could be augmented. In doing this we are aiming at a moving target; it must be the case that further developments will have been made before the book reaches the press. Nonetheless, such an survey can give the reader a much more developed sense of the potential of type theory, as well as giving the background of what is to come.

Partial Objects in Constructive Type Theory Constable, Robert L. and Smith, Scott Fraser

Programming in Martin-Lof's Type Theory - An Introduction Nordstrom, Bengt, Petersson, Kent, and Smith, Jan M. Out of print, full text available online.

Denotational Semantics

Relating Operational and Denotational Semantics for Input/Output Effects Crole, Roy L. and Gordon, Andrew D

Z Specification Language

Z User pages Alas, the link is broken.

The Z Notation: A Reference Manual Text online! Outdated, but still a useful introduction

Using Z: Specification, Refinement, and Proof Text online!

The Way of Z: Practical Programming with Formal Methods Excellent book, but paper only.

CZT Community Z Tools. "…a set of tools for editing, typechecking and animating formal specifications written in the Z specification language, with some support for Z extensions such as Object-Z, Circus, and TCOZ."


The Implementation of Functional Programming Languages Peyton Jones, Simon. Out of print, full text online.

Representing monads Filinski, Andrzej

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 composablecontinuations construct can itself be represented using ordinary, non-composable first-class continuations and a single piece of state. Thus, in the presence of two specific computational effects— storage and escapes—any expressible monadic structure (e.g., nondeterminism as represented by the list monad) can be added as a purely definitional extension, without requiring a reinterpretation of the whole language. The paper includes an implementation of the construction (in Standard ML with some New Jersey extensions) and several examples.

Computability Logic

Introduction to computability logic Japaridze, Giorgi

In the beginning was game semantics Japaridze, Giorgi


Practical Foundations for Programming Languages Harper Robert


Giuseppe Longo has lots of interesting pubs online

Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-NonCommercial-NoDerivs 3.0 License